The S operator is used to reason about the 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 CTMCs.
The definition of steady-state (long-run) probabilities for finite CTMCs is well defined (see e.g. [Ste94]).
Informally, the property:
is true in a state s of a CTMC if
"starting from s, the steady-state (long-run) probability of being in a state which satisfies prop,
meets the bound bound".
A typical example of this type of property would be:
which means: "the long-run probability of the queue being more than 75% full is less than 0.05".
