Promela |
Control-Flow |
goto(3) |
SYNTAX
goto
name
DESCRIPTION
The
goto
is normally not executed, but is used to determine the target
control state for the immediately preceding statement.
The target state is identified by the label
name
that must be unique within the surrounding
proctype
declaration.
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
First example:
L1: if :: a != b -> goto L1 :: a == b -> goto L2 fi; L2: ...The above program fragment defines two control states, labeled by L1 and 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 above sequence is therefore equivalent to both
L1: do :: a != b :: a == b -> break od; L2:and could be written more efficiently as simply:
L1: a == b; L2:Note that the last version makes use of the capability of Promela to synchronize on a condition statement.
Second example:
L1: do :: t1 -> t2 /* reaches L1 immediately after executing t2 */ :: t3 -> goto L1 /* reaches L1 immediately after executing t3 */ :: goto L2 /* optionally jumps to L2 in one step */ od; L2: ...
NOTES
It is an error if no target for the
goto
is defined within the surrounding
proctype
declaration.
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |