Promela |
Control-Flow |
goto |
NAME
goto -
unconditional jump to a labeled statement.
SYNTAX
goto name
DESCRIPTION
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.
EXAMPLES
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.
NOTES
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 Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |