Macro Definition

Macros can be defined and used in CTL and LTL formulae for valid sub-formulae. You cannot use a macro such as "\define MSB 7" since "7" is not a valid CTL or LTL formula. The macro definition must precede its use.

{\DEFINE | \Define | \define} MACRO formula

For instance,

\define Red t_sig = RED
\define Blue t_sig = BLUE

defines \Red as a shorthand for t_sig = RED . Similarly for \Blue. One can then write:

AG ( \Red -> AX ( \Blue ) );