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`
`\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 ) );`