Promela |
Control-Flow |
d_step |
NAME
d_step -
introduces a deterministic code fragment that is executed indivisibly.
SYNTAX
d_step { sequence }
DESCRIPTION
A
d_step sequence is executed as if it were one single indivisible statement.
It is comparable to an
atomic sequence, but it differs from such sequences on the
following three points:
EXAMPLES
The following example uses a
d_step sequence to swap the value of all elements in two arrays:
#define N 16 byte a[N], B[N]; init { d_step { /* swap elements */ byte i, tmp; i = 0; do :: i < N -> tmp = b[i]; b[i] = a[i]; a[i] = tmp; i++ :: else -> break od; skip /* add target for break */ } ... }A number of points should be noted in this example. First, the scope of variables i and tmp is independent of the precise point of declaration within the init body. In particular, by placing the declaration inside the d_step sequence we do not limit the scope of these variables to the d_step sequence: they remain visible also after the sequence.
Second, we have to be careful that the loop that is contained within this d_step sequence terminates. No system states are saved, restored, or checked during the execution of a d_step sequence. If an infinite loop is accidentily included in such a sequence, it can cause the verifier to hang.
Third and last, because one cannot jump into or out of a d_step sequence, a break from a do loop which appears as the last construct in a d_step sequence will trigger a parse error from Spin. Note that this type of break statement creates an hidden jump out of the d_step , to the statement that immediately follows the do loop, which is outside the d_step itself in this case. The problem can be avoided by inserting a dummy skip after the loop, as shown in the example. There is no run-time penalty for this skip statement.
NOTES
A
d_step sequence can be executed much more efficiently
during verifications than an
atomic sequence.
The difference in performance can be significant,
especially in large-scale verifications.
The d_step sequence also provides a mechanism in Promela to add new types of statements to the language, translating into new types of transitions in the underlying automata. A c_code statement has similar properties.
SEE ALSO
atomic
c_code
goto
sequence
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |