L3_patterns

[L3] Advanced language constructs

In this module we introduce advanced language constructs for Spectra specifications, e.g., patterns and past operators.

Task at end of video

Extend specification TrafficL3.spectra

• Add an assumption that carA is always eventually followed by carB (use the pattern pRespondsToS).

Task solution

The solution for this task may be found in the project L3_patterns_solution.

More

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.