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) |