NAME
do - repetition construct.

SYNTAX
do :: sequence [ :: sequence ]* od

DESCRIPTION
The repetition construct, like all other language elements described in this section, is strictly seen not a statement, but a method to define the structure of the underlying automaton. There is a unique local control state at the start of the repetition construct, and another one just after it, where the next statement in the program appears (or the end-state of the proctype body. The repetition construct defines the outgoing transitions for the first control state. There are as many outgoing transitions as there are option sequences defined. By default, the end of each option sequence leads back to the first control state, allowing for repeated execution. A transition to the control state that follows the repetition construct can be defined with a break .

There can be one or more option sequences in a repetition construct. The beginning of an option sequence is indicated by a double-colon. The first statement in each sequence is traditionally called its guard . An option can be selected for execution provided that its guard statement is executable. More than one guard statement may be executable at the same time, in which case the selection of an option is non-deterministic. If none of the guards is executable, the construct as a whole will block.

The do , when considered as a high-level statement, is executable if and only if at least one of its guards is executable.

EXAMPLES
A cyclic program that randomly increments or decrements the variable.

byte count;



proctype counter()

{	do

	:: count = count + 1

	:: count = count - 1

	:: (count == 0) -> break

	od

}

proctype counter()

{	do

	:: count != 0 ->

		if

		:: count = count + 1

		:: count = count - 1

		fi

	:: else -> break

	od

}

NOTES
The semantics of a Promela repetition construct differs from similar control flow constructs in Hoare's language CSP, and Dijkstra's earlier definition of a non-deterministic guarded command language. In Dijkstra's definition, the repetition construct is aborted when none of the guards is executable. In Promela executability is used as the basic means to enforce process synchronization, and it is not considered an error if statements block temporarily. A further difference with CSP is that in Promela there is no restriction on the type of statement that can be used as a guard of an option sequence.

SEE ALSO
break(3), if(3), goto(3).