Promela Reference -- do(3)




do - repetition construct.

do :: sequence [ :: sequence ]* od


The repetition construct, like all other control-flow constructs, is strictly seen not a statement, but a convenient method to define the structure of the underlying automaton.

A repetition construct has a single start and stop state. Each option sequence within the construct defines outgoing transitions for the start state. The end of each option sequence transfers control back to the start state of the construct, allowing for repeated execution. The stop state of the construct is only reachable via a break statement from within one of its option sequences.

There must be at least one option sequence in each repetition construct. Each option sequence starts with a double-colon. The first statement in each sequence is called its guard . An option can be selected for execution only when its guard statement is executable. If more than one guard statement is executable, one of them will be selected non-deterministically. If none of the guards are executable, the repetition construct as a whole blocks.

A repetition construct as a whole is executable if and only if at least one of its guards is executable.


The following example defines a cyclic process that non-deterministically increments or decrements a variable named count :

In this example the loop can be broken only when count reaches zero. It need not terminate, though, because the other two options always remain unconditionally executable. To force termination, we can modify the program as follows:

The semantics of a Promela repetition construct differ from a similar control flow construct tha was included in Dijkstra's seminal proposal for a non-deterministic guarded command language. In Dijkstra's language, the repetition construct is aborted when none of the guards are executable; in Promela, execution is merely blocked in this case. In Promela, executability is used as the basic mechanism for enforcing process synchronization, and it is not considered to be an error if statements occasionally block. The Promela repetition construct also differs from a similar control flow construct in Hoare's classic language CSP. In CSP, send and receive statements cannot appear as guards of an option sequence. In Promela, there is no such restriction.

The guard statements in option sequences cannot individually be prefixed by a label, since all option sequences start from the same state (the start state of the construct). If a label is required, it should be placed before the keyword do .


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