Skip to content

Latest commit

 

History

History
21 lines (11 loc) · 1.08 KB

File metadata and controls

21 lines (11 loc) · 1.08 KB

[L2] Advanced language constructs

In this module we introduce advanced language constructs for Spectra specifications, e.g., type definitions, defines, predicates, arrays.

Watch the video

Task at end of video

Extend specification GridL2.spectra with the predicate invMove(Move a, Move b) to assert that two parameters of type Move are inverse to each other, e.g., UP and DOWN or LEFT and RIGHT.

Task solution

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

Watch the video

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.