An else condition statement is executable if and only if no other statement within the same process is executable at the control state where the else appears (see intro(0)).
It is an error to define control flow constructs in which more than one else applies to the same control state (e.g., by defining more than one else statement within a single selection or repetition construct).
if :: a > b -> ... :: a == b -> ... :: else -> ... /* evaluates to: a <= b */ fiThe semantics above would allow for an else to occur outside selection or repetition constructs, in a non-branching sequence of statements. The rules then say that the else is equivalent to a skip because it has no alternatives within the local context. The Spin parser, however, will flag such use as an error.
In the following example
A: do :: if :: x > 0 -> x-- :: else -> break fi :: else -> x = 10 odboth else constructs apply to the same control state, labeled A . (The current simulator is often forgiving of small non-fatal errors like this one. The verifier is meant to reliably traps all errors.)