goto - unconditional jump to a labeled statement.
The goto is normally not executed, but is used by the parser to determine the target control state for the immediately preceding statement; see also the manual page for break . The target state is identified by the label name and must be unique within the surrounding proctype declaration or never claim.
In cases where there is no immediately preceding statement, for instance, when the goto appears as a guard in an option of a selection or repetition structure, the goto is executed as if it were a skip , taking one execution step to reach the labeled state.
The following program fragment defines two control states, labeled by L1 and L2 :
L1: if :: a != b -> goto L1 :: a == b -> goto L2 fi; L2: ...If the values of variables a and b are equal, control moves from L1 to L2 immediately following the execution of condition statement a == b . If the values are unequal, control returns to L1 immediately following the execution (evaluation) of a != b . The statement is therefore equivalent to
L1: do :: a != b :: a == b -> break od; L2:and could also be written more efficiently in Promela as simply:
L1: a == b; L2:Note that the last version makes use of the capability of Promela to synchronize on a standalone condition statement.
It is an error if no target for the goto is defined within the surrounding proctype or never claim declaration.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|