Promela |
Predefined |
else(5) |
NAME
else
-
a system defined condition statement.
SYNTAX
else
DESCRIPTION
The predefined condition statement
else
is intended to be used as a guard (i.e., the first
statement) of an option sequence inside selection
or repetition constructs.
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).
EXAMPLES
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.)
NOTES
The executability of the
else
depends only on local context within a process.
The Promela semantics for
timeout
can be seen as a system version of the
else .
A
timeout
is executable only when no alternative statement within the
system is executable.
SEE ALSO
skip(1), condition(4), timeout(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |