Promela Reference -- goto(3)

`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.

SEE ALSO
break(3), labels(3).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage (Page Updated: 16 December 1997)

`Promela`

`Control-Flow`

`goto(3)`