One of the most fundamental tasks when specifying properties of a model is to identify particular sets or classes of states of the model. For example, to verify a property such as "the algorithm eventually terminates successfully with probability 1", it is first necessary to identify the states of the model which correspond to situations where "the algorithm has terminated successfully". In terms of the way temporal logics are usually presented, these correspond to atomic propositions.
In PRISM, this is achieved simply by writing an expression in the PRISM language which evaluates to a Boolean value. This expression will typically contain references to variables (and constants) from the model to which it relates. The set of states corresponding to this expression is those for which it evaluates to true. We say that the expression is "satisfied" in these states.
For example, in the property given above:
the expression num_errors > 5 is used to identify states of the model where more than 5 errors have occurred.
It is also common to use labels to identify states in this way, like "terminate" in the example:
Properties can refer to labels either from the model to which the property relates, or included in the same properties file.
Site hosted at the Department of Computer Science, University of Oxford