Promela |
Control-Flow |
sequence |
NAME
sequence -
curly braces, used to enclose a block of code.
SYNTAX
{ sequence }
DESCRIPTION
Any sequence of Promela statements may be enclosed in
curly braces and treated syntactically as if it
were a statement. This facility is most useful
for defining
unless constructs, but can also generally be used to
structure a model.
EXAMPLES
if
:: a < b -> { tmp = a; a = b; b = a }
:: else ->
{ printf("unexpected case\n");
assert(false)
}
fi
The more common use is for structuring
unless statements, as in:
{ tmp = a; a = b; b = a; }
unless
{ a >= b }
Note the differences between these two examples.
In the first example, the value of the expression
a < b is checked once, just before the bracketed sequence
is executed.
In the second example, the value of the negated expression is
checked before each statement execution in the main
sequence, and execution is interrupted when that expression
becomes true.
NOTES
The last statement in a sequence need not be followed
by a statement separator, but if the sequence is followed by another
statement, the sequence as a whole should be separated from
that next statement with a statement separator.
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |