Promela Reference -- Unless(3)





unless - to define exception handling routines.

stmnt unless stmnt

Like repetition and selection, the unless construct is not really a statement, but a method to define the structure of the underlying automaton, and to distinguish between higher and lower priority of transitions within a single process.

The first statement, generally defined as a sequence of basic statements, is called the normal sequence , or the main sequence . The second statement, also generally defined as a sequence of basic statements, is called the escape sequence . The executability of all basic statements in the normal sequence is constrained to the non-executability of the guard statement of the escape sequence. If and when the guard statement of the escape sequence becomes executable, execution proceeds with the escape sequence and never returns to the normal sequence. If the guard of the escape sequence remains unexecutable throughout the execution of the normal sequence, it is skipped.

The effect of the escape sequence is distributed to all the basic statements in the normal sequence, including those that are contained inside atomic sequences. For a d_step , however, the escape will affect only the guard statement of the d_step sequence, but not the remaining basic statements inside the sequence (i.e., a d_step is equivalent to a single statement that can only be executed in its entirety from start to finish).

The guard statement of an unless can itself be a selection or a repetition construct, allowing for a non-deterministic selection of a specific executable escape.

Within the semantics model (see Intro(0)), this means that the basic statement(s) that make up the guard of the escape sequence is (are) assigned a higher priority than all basic statements in the normal sequence. Unless constructs may be nested. In that case these rules imply that, moving outward, the guard statement from each new layer of nesting is assigned a higher priority than all statements enclosed.

Consider the following unless statement:

{ B1; B2; B3 } unless { C1; C2 }

where the parts inside the curly braces are arbitrary Promela fragments. Execution of this unless statement begins with the execution of B1 . Before each statement execution of B1;B2;B3 , the executability of the first statement, or guard , of fragment C1 is checked, using the normal Promela semantics of executability. Execution of statements from B1;B2;B3 proceeds only while the guard statement of C1 remains unexecutable. The first instant that this guard of the escape sequence is found to be executable, control changes to it, and execution continues as defined for C1;C2 . Individual statement executions remain indivisible, so control can only change from inside B1;B2;B3 to the start of C1 in between individual statement executions. If the guard of the escape sequence does not become executable during the execution of B1;B2;B3 , it is skipped when B3 terminates.

Another example of the use of the unless to define an escape sequence is:



:: b1 -> B1

:: b2 -> B2


od unless { c -> C };


The curly braces around the normal or the escape sequence may be deleted if there can be no confusion about which statements belong to those sequences. In the example, condition c acts as a watchdog on the repetition construct from the normal sequence. Note that this is not necessarily equivalent to the construct:


:: b1 -> B1

:: b2 -> B2


:: c -> break


C; D

if B1 or B2 are non-empty. In the first version of the example, execution of the iteration can be interrupted at any point inside each option sequence. In the second version, execution can only be interrupted at the start of the option sequences.

In the presence of rendezvous operations, the precise effect of an unless construct can be hard to assess. See the discussion in Intro(0) for details on resolving apparent semantic conflicts.


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