Promela |
Control-Flow |
Unless(3) |
NAME
unless
-
to define exception handling routines.
DESCRIPTION
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.
EXAMPLES
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:
A;
do
:: b1 -> B1
:: b2 -> B2
\&...
od unless { c -> C };
D
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:
A; do :: b1 -> B1 :: b2 -> B2 \&... :: c -> break od; C; Dif 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.
NOTES
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.
SEE ALSO
sequence(3).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |