NAME
separators - for sequential composition of statements and declarations.

SYNTAX
step ; step
step -> step

DESCRIPTION
The semicolon and the arrow are equivalent statement separators in Promela; they are not statement terminators , although the parser has been taught to be forgiving for occasional lapses. The last statement in a sequence need not be followed by a statement separator, unlike, for instance, in the C programming language.

EXAMPLES

x = 3;
atomic {
	x = y;
	y = x	/* no separator is required here */
};		/* but it is required here...    */
y = 3

NOTES
The convention is to reserve the use of the arrow separator to follow condition statements, such as guards in selection or repetition structures. The arrow symbol can thus be used to visually identify those points in the code where execution could block.

SEE ALSO
break
labels
goto