Go to the first, previous, next, last section, table of contents.
TRANS declarations
The transition relation R of the model is a set of current state/next
state pairs. Whether or not a given pair is in this set is determined by
a boolean valued expression T, introduced by the `TRANS' keyword. The
syntax of a TRANS declaration is:
trans_declaration :: "TRANS" trans_expr
trans_expr :: next_expr
It is an error for the expression to yield any value other than 0
or 1. If there is more than one TRANS declaration, the
transition relation is the conjunction of all of TRANS
declarations.