Macro Define

Macros can be defined and used in CTL formulae for valid sub-formulae. You cannot use a macro such as "\define MSB 7" since "7" is not a valid CTL formula. Before you use macro string, you have to define it first.

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

\define Red t_sig = RED
\define Blue t_sig = BLUE
....
AG ( \Red -> AX ( \Blue ) );