In this module we review how to check realizability, i.e., check whether there exists an implementation that realizes a Spectra specification, and synthesizing a controller, i.e., obtaining such an implementation, if one exists.
Specifications TrafficA1a.spectra and TrafficA1b.spectra combine separate liveness assumptions/guarantees into a single one
- check for each specification whether it is realizable
- if it is, synthesize a controller
Try to explain why each specification is either unrealizable or how the resulting controller realizes the specification.
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.