This Spectra Tutorial has been developedCode as a technical briefing for ICSE 2021.
This repository contains examples of specification used in a series of videos available in a YouTube playlist: Reactive Synthesis with Spectra. Each module contains an introduction (linked video), a task (explained in the video), example code (in this repository to be imported as Eclipse projects), and a solution (second linked video).
We suggest going through the modules in the following order (order of the playlist above):
-
[0a] Reactive synthesis with Spectra video
-
[0b] Installation and Import video
-
[L1] Write your first specification folder
-
[A1] Synthesize your first controller folder
-
[E1] Basic step-by-step simulation folder
-
[L2] Advanced language constructs folder
-
[A2] Unrealizability folder
-
[E2] Execute your reactive system folder
-
[L3] Advanced language constructs folder
-
[A3] Non-well-separation folder
-
[E3] Advanced step-by-step simulation folder
-
[D1] Working with Spectra abstract syntax folder
-
[D2] Working with counter-strategies API folder
-
[L4] Triggers folder