NAME
probabilities - for distinguishing between high and low probability events.

DESCRIPTION
There is no mechanism in Promela for indicating the probability of an event. It is possible to build a verification system that supports event probabilities, but this comes at a price in performance, and can have unintended side-effects. In Spin the attempt is to build a stronger verification system by abstracting from the probability of event sequences.

Spin is designed to check the unconditional correctness of a system. A design error in principle always has a low probability of occurrence. After all, the high probability event scenarios are easily intercepted with standard testing and debugging techniques, but only model checking techniques are able to reproducible detect the remaining classes of errors. Phrased differently: verification in Spin is concerned with possible behaviors, not with probably behaviors.

In some cases it can, nonetheless, be useful to exclude known low probability event scenarios from further consideration in a verification. Progress labels can be used to accomplish this with precise control, as explained in progress(2).

NOTES
It is possible to influence the probability that an option in a non-deterministic selection is chosen during random simulations, by replicating the option.

SEE ALSO
progress(2), if(2), do(2).