Promela Reference -- unless(3)




unless - to define exception handling routines.

stmnt unless stmnt

Similar to the repetition and selection constructs, 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 construct can appear anywhere a basic Promela statement can appear.

The first statement, generally defined as a block or sequence of basic statements, is called the main sequence. The second statement is called the escape sequence. The guard of either sequence can be either a single statement, or it can be an if , do , or lower level unless construct with multiple guards and options for execution.

The executability of all basic statements in the main sequence is constrained to the non-executability of all guard statements of the escape sequence. If and when one of the guard statements of the escape sequence becomes executable, execution proceeds with the remainder of the escape sequence and does not return to the main sequence. If all guards of the escape sequence remain unexecutable throughout the execution of the main sequence, the escape sequence as a whole is skipped.

The effect of the escape sequence is distributed to all the basic statements inside the main sequence, including those that are contained inside atomic sequences. If a d_step sequence is included, though, the escape affects only its guard statement (that is, the first statement) of the sequence, and not the remaining statements inside the d_step . A d_step is always equivalent to a single statement that can only be executed in its entirety from start to finish.

As noted, the guard statement of an unless construct can itself be a selection or a repetition construct, allowing for a non-deterministic selection of a specific executable escape. Following the semantics model, the guard statements of an escape sequence are assigned a higher priority than the basic statements from the main sequence.

Unless constructs may be nested. In that case, the guard statements from each unless statement take higher priority than those from the statements that are enclosed. This priority rule can be reversed, giving the highest priority to the most deeply nested unless escapes, by using Spin run-time option -J . This option is called -J because it enforces a priority rule that matches the evaluation order of nested catch statements in Java programs.

Promela unless statements are meant to facilitate the modeling of error handling methods in implementation level languages.

Consider the following unless statement:

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 in the sequence 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 unless is:

The curly braces around the main 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 main sequence. Note that this is not necessarily equivalent to the construct: 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 semantics definition for details on resolving apparent semantic conflicts.


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