Typically, a variable declaration
specifies the initial value for that variable.
The initial state for the model is then defined by the initial value for all variables.
It is possible, however, to specify that a model has multiple initial states.
This is done using the
which can be placed anywhere in the file except within a module definition,
and removing any initial values from variable declarations.
endinit keywords, there should be a
predicate over all the variables of the model.
Any state which satisfies this predicate is an initial state.
Consider again Example 1.
As it stands, there is a single initial state
If we remove the
init 0 part of both variable declarations
and add the following to the end of the file:
there will be three initial states:
Similarly, we could instead add:
in which case there would be two initial states: