NAME
sequence - brackets to enclose an arbitrary 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\n") }; assert(0)

fi

NOTES
Semi-colons are used as statement separators, not as statement terminators, in Promela (although the parser is forgiving on mild deviations from this requirement). This means that the last statement in a sequence need not be followed by a semi-colon, but the closing curly brace of the sequence should be followed by a semi-colon if another statement follows it.

SEE ALSO
unless(3).