Promela Reference -- sequence(3)

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

The more common use is for structuring unless statements, as in: 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.

SEE ALSO
atomic
d_step
unless


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)