All of the properties described in the previous sections evaluate to a Boolean value. Although the satisfaction of a property is defined in terms of a single state, when analysing a property of a model, PRISM considers the property to be true if it is satisfied in all states of the model, and false otherwise.
To check if a property is satisfied in some subset of states, for example just the initial states, properties can be prefixed with an implication, e.g.:
See the section "Properties Files" for details of the "init" expression.
