if - selection construct.
if :: sequence [ :: sequence ]* fi
The selection 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. Each selection construct has a unique start and stop state. Each option sequence within the construct defines outgoing transitions for the start state, leading to the stop state. There can be one or more option sequences. By default, the end of each option sequence leads to the control state that follows the construct.
There must be at least one option sequence in each selection 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 selection construct as a whole blocks.
The selection construct as a whole is executable if and only if at least one of its guards is executable.
Using the relative values of two variables a and b to choose between two options, we can write
if :: (a != b) -> ... :: (a == b) -> ... fiThis selection structure contains two option sequences, each preceded by a double colon. Only one sequence from the list will be executed. A sequence can be selected only if its guard statement is executable (the first statement). In the example the two guards are mutually exclusive, but this is not required.
The guards from a selection structure cannot be prefixed by labels individually. These guards really define the outgoing transitions of a single control state, and therefore any label on one guard is really a label on the source state for all guards belonging on the selection construct itself (cf. label L0 in the next example). It is tempting to circumvent this rule and try to label a guard by inserting a skip in front of it, for instance, as follows:
L0: if :: skip; L1: (a != b) -> ... :: (a == b) -> ... fi;But note that this modification alters the meaning of the selection from a choice between (a != b) and (a == b) , to a choice between skip (which is the same as (1) or true ) and (a == b) . The addition of the skip statement also adds an extra intermediate state, immediately followin the skip statement itself.
The semantics of a Promela selection construct differ from similar control flow constructs in Hoare's language CSP, and in Dijkstra's earlier definition of a non-deterministic guarded command language. In Dijkstra's definition, the selection construct is aborted when none of the guards is executable. In Promela, execution blocks in this case. In Promela, executability is used as the basic means to enforce process synchronization, and it is not considered to be an error if statements block temporarily. Another 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. Any type of statement can be used as a guard, including assignments, and send or receive operations.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|