NAME
if - selection construct.

SYNTAX
if :: sequence [ :: sequence ]* fi

DESCRIPTION
The selection construct 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 selection construct, and another one just after it, where the next statement in the program appears (or the end-state of the proctype body. The selection 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 to the control state that follows the construct.

There can be one or more option sequences in a selection construct. The beginning of each 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 if , when considered as a high-level statement, is executable if and only if at least one of its guards is executable.

EXAMPLES
Using the relative values of two variables a and b to choose between two options, we can write

if

:: (a != b) -> ...

:: (a == b) -> ...

fi

The guards from a selection structure cannot be prefixed by labels individually. These statements 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 below). It is tempting to circumvent this rule by inserting a skip as follows:

L0:	if

	:: skip;

L0a:		(a != b) -> goto L1

	:: (a == b) -> L2

	fi;

NOTES
The semantics of a Promela selection 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 selection 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
do(3), goto(3), else(5).