The

operator is used to reason about the **S***steady-state* behaviour of a model,
i.e. its behaviour in the *long-run* or *equilibrium*.
Although this could in principle relate to all three model types,
PRISM currently only provides support for DTMCs and CTMCs.
The definition of steady-state (long-run) probabilities for finite DTMCS and CTMCs is well defined (see e.g. [Ste94]).
Informally, the property:

S bound [ prop ]

is true in a state *s* of a DTMC or CTMC if
"starting from *s*, the steady-state (long-run) probability of being in a state which satisfies the (Boolean-valued) PRISM property `prop`

, meets the bound `bound`

".
A typical example of this type of property would be:

S<0.05 [ queue_size / max_size > 0.75 ]

which means: "the long-run probability of the queue being more than 75% full is less than 0.05".

Like the

operator, the **P**

operator can be used in a **S***quantitative* form, which returns the actual probability value, e.g.:

S=? [ queue_size / max_size > 0.75 ]

and can be further customised with the use of filters.