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

DESCRIPTION
There is no mechanism in Promela for indicating the probability of a statement execution, other than during random simulations with priority tags.

Spin is designed to check the unconditional correctness of a system. High probability executions are easily intercepted with standard testing and debugging techniques, but only model checking techniques are able to reproducibly detect the remaining classes of errors.

Disastrous error scenarios often have a low probability of occurrence that only model checkers can catch reliably. The use of probability tags on statement executions would remove the independence of probability, which seems counter to the premise of logic model checking. Phrased differently, verification in Spin is concerned with possible behavior, not with probable behavior. In a well-designed system, erroneous behavior should be impossible, not just improbable.

To exclude known low probability event scenarios from consideration during model checking, a variety of other techniques may be used, including the use of model restriction, LTL properties, and the use of progress-state, end-state, and accept-state labels.

SEE ALSO
if
do
priority
progress
unless