break - jump to the end of the innermostn do loop.
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.
L1: do :: t1 -> t2 :: t3 -> break :: break od; L2: ...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 .
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.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|