Promela Reference -- break(3)

Promela

Control-Flow

break


NAME
break - jump to the end of the innermostn do loop.

SYNTAX
break

DESCRIPTION
The keyword break does not indicate an executable statement, but it instead acts like a special type of semicolon: merely indicating the next statement to be executed. The search for the next statement to execute continues at the point that immediately follows the innermost do loop.

When the keyword break does not follow a statement, but appears as a guard in an option of a selection structure or do loop, then the execution of this statement takes one execution step to reach the target state, as if it were a skip . In all other cases, the execution of a break statement requires no separate step; the move to the target state then occurs after the execution of the preceding statement is completed.

If the repetition structure in which the break statement occurs is the last statement in a proctype body or never claim, then the target state for the break is the process's or claim's normal termination state, where the process or claim remains until it dies and is removed from the system.

EXAMPLES

In this example, control reaches the label L1 immediately after statement t2 is executed. Control can also reach label L2 immediately after statement t3 is executed, and optionally, in one execution step, control can also move from label L1 to label 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 always be replicated with the use of a goto statement and a label.

SEE ALSO
do
goto
if
labels
skip


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