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

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.

The solution for this task may be found in the project L2_defsArrays_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.