The basic syntax of the language for expressing a PRISM property prop is given by the following grammar:
where:
expr is a PRISM language expression which evaluates to a Boolean (as described in the previous section),
p is a PRISM language expression evaluating to a double in the range [0,1],
t is a PRISM language expression evaluating to a non-negative double or integer.
A property is evaluated with respect to a single state of a model.
For the syntax given above, all properties evaluate to Boolean values,
i.e. for any state $s$ of a model, a property is either "true" or "false" in that state.
Equivalently, we also say that a property is "satisfied" or "not satisfied" in a state.
For the basic operators of the logic
(i.e. true, false, expr, !, &, | and =>)
the semantics are as for classical propositional logic:
true is true in all states,
false is not true in any state,
expr is true if the PRISM expression expr evaluates to true,
!prop is true if prop is not true,
prop1 & prop2 is true if both prop1 and prop2 are true,
prop1 | prop2 is true if either prop1 or prop2 is true,
prop1 => prop2 is true if prop1 implies prop2.
