In this module we will again (as in [E1]) use an interactive simulation of a reactive system implementation using the Spectra Controller walker. We will see how to use advanced features like breakpoints and exploring reachability.
Synthesize a controller for specification TrafficA1.spectra and check whether a state with carA & carB & greenB is reachable for the synthesized controller.
This module is part of a tutorial on the Spectra language and tools for reactive synthesis. More information and materials are available from the SYNTECH project website.