Promela Reference -- break(3)

Google

Promela

Control-Flow

break(3)

NAME
break - jump to the end of the innermost repetition structure.

SYNTAX
break

DESCRIPTION
The break is normally not executed, but is used to determine the target control state for the immediately preceding statement. The target control state is the state that immediately follows the innermost repetition structure.

In cases where there is no immediately preceding statement, for instance when the break appears as a guard in an option of a selection or repetition structure, the break is executed as if it were a skip , taking one execution step to reach the target state.

If the repetition structure is the last statement in a proctype body, the target state for the break is the process's end-state, where the process remains until it is removed from the system.

EXAMPLES

L1:	do

	:: t1 -> t2    /* reaches L1 immediately after executing t2 */

	:: t3 -> break /* reaches L2 immediately after executing t3 */

	:: break       /* optionally jumps to L2 in one step */

	od;

L2:	...

NOTES
It is an error to place a break statement where there is no surrounding repetition structure. The effect of a break statement can be replicated with the use of a goto statement and a label.

SEE ALSO
skip(1), do(3), goto(3), labels(3).


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