Follow the Spectra tutorial available from http://smlab.cs.tau.ac.il/syntech/tutorial/.
-
This includes the installation of the Spectra plug-ins from this Eclipse update site: http://smlab.cs.tau.ac.il/syntech/spectra/tools/update/
-
You may start watching the tutorial videos from here: https://www.youtube.com/watch?v=smDcuR3NP44&list=PLGyeoukah9Nbx1QquUmZGdLulFZIsiRlZ&index=3
-
The code for all tasks is available from GitHub: https://github.com/jringert/spectra-tutorial
The tutorial consists of explanation videos with simple tasks. Please try these yourself. Solution videos are provided, but just watching these without trying the activities will likely not have the desired learning effect.
Clone this repository and import it into your Eclipse. Make sure to install the required Spectra plug-ins.
To pass this part you need to:
-
Create a meaningful Spectra specification Spec.spectra of some reactive system (see [L1]-[L3]) with at least
-
3 environment and 3 system variables
-
2 initial (ini), 4 safety (alw), and 2 justice (alwEv) assumptions or guarantees (at least 2 x asm and 2 x gar)
-
-
Write a short comment about the meaning of each variable, each assumption, and each guarantee.
-
Ensure that the specification is realizable (see [A1] & [A2]) and well-separated (see [A3]).
-
Create a variant of your specification that is unrealizable due to a missing justice assumption. Provide the assumption commented out in the specification Spec_Unreal.spectra and mark it with the comment “//FIX” preceding it.
-
Synthesize a Just-in-time symbolic controller for the realizable specification in file Spec.spectra and write code to execute it (see [E2]) in class de.buw.se.gendev.lab2.SpecSimulatorCmd.
You may use the provided test cases to see your progress. All test cases should pass for your submission. The test cases are not able to test the simulation of the controller!
See this video: https://youtu.be/SIDXccugsyY
Commit your solution into GitHub and submit the repository link in Moodle.