In this module we review how to
- check realizability, i.e., check whether there exists an implementation that realizes a Spectra specification,
- compute an unrealizable core, i.e., compute a minimal subset of guarantees that is already unrealizable, and
- compute counter-strategies, i.e., strategies for the environment that force any potential system implementation to violate guarantees.
Analyze specifications TrafficL2b.spectra to TrafficL2d.spectra
- Investigate reasons for unrealizability using a core or counter-strategy.
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.