Promela Reference -- d_step(3)

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:

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)