Promela Reference -- goto(3)

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 :

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 and could also be written more efficiently in Promela as simply: 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.

SEE ALSO
break
condition
labels


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)