Promela |
Basic Statement |
condition |
NAME
condition statement
-
for conditional execution and synchronization.
SYNTAX
expr
EXECUTABILITY
( expr != 0)
EFFECT
none
DESCRIPTION
In Promela, a standalone expression is a valid statement.
A condition statement is often used as a guard at
the start of an option sequence in a selection or repetition structure.
Execution of a condition statement is blocked until the
expression evaluates to a non-zero value (or, equivalently, to
the boolean value true).
All Promela expressions are required to be side effect free.
EXAMPLES
(1) /* always executable */ (0) /* never executable */ skip /* always executable, same as (1) */ true /* always executable, same as skip */ false /* always blocks, same as (0) */ a == b /* executable only when a equals b */A condition statement can only be executed (passed) if it holds. This means that the statement from the first example can always be passed, the second can never be passed, and the last cannot be passed as long as the values of variables a and b differ. If the variables a and b are local, the result of the evaluation cannot be influenced by other processes, and this statement will work as either true or false , depending on the values of the variables. If at least one of the variables is global, the statement can act as a synchronizer between processes.
SEE ALSO
do
else
false
if
skip
true
timeout
unless
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |