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.
if :: (a != b) -> ... :: (a == b) -> ... fiThis selection structure contains two optional sequences, each preceded by a double colon. Only one sequence from the list will be executed. A sequence can be selected if its guard statement is executable (the first statement). In the example above the two guards are mutually exclusive.
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;But note that this modification also alters the meaning of the selection from a choice between (a != b) and (a == b) , to a choice between skip and (a == b) .