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) } fiThe 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) |