Promela |
BasicStatements |
condition(4) |
NAME
condition statement
-
for conditional execution and process synchronization.
SYNTAX
expr
EXECUTABILITY
expr != 0
EFFECT
None
DESCRIPTION
In Promela any expression used by itself forms a valid statement,
called a condition statement.
Execution of a condition statement is blocked until the
expression evaluates to a non-zero value.
EXAMPLES
1 /* the equivalent of skip and true */ 0 /* the equivalent of stop and false */ a == bA condition statement can only be passed if it holds, this means that the statement from the first example can always be passed without delay, the second can never be passed, and the third 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 a skip or a stop . If at least one of the variables is global, the statement can act as a synchronizer between processes.
NOTES
The condition statement is most frequently used as a
guard (i.e., the initial statement) of an option sequence
in a selection or repetition structure.
It can, however, be used in any context, and serve to
enforce synchronization between asynchronous processes.
SEE ALSO
skip(1), if(3), do(3), else(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |