Go to the first, previous, next, last section, table of contents.
INIT declarations
The set of initial states of the model is determined by a boolean expression
under the `INIT' keyword. The syntax of a INIT declaration is:
init_declaration :: "INIT" init_expr
init_expr :: simple_expr
It is an error for the expression to contain the next() operator,
or to yield any value other than 0 or 1. If there is more
than one INIT declaration, the initial set is the conjunction of
all of the INIT declarations.