In this module we introduce triggers for Spectra specifications.
Extend specification GridL4.spectra
- Add a guarantee that the robot should never be away from position
p1for more than 20 steps.
The solution for this task may be found in the project L4_triggers_solution.
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.