Promela |
Control-Flow |
d_step(3) |
NAME
d_step
-
introduces a
deterministic
sequence of code that is executed indivisibly.
SYNTAX
d_step {
sequence }
DESCRIPTION
The differences between a
d_step
sequence
and an
atomic
sequence are:
EXAMPLES
d_step { /* swap the values of a and b */ tmp = b; b = a; a = tmp }
NOTES
None of the restrictions listed apply to
atomic
sequences.
This means that the keyword
d_step
can always be replaced with the keyword
atomic ,
but the reverse is not true.
The main, reason for using d_step sequences is to improve the efficiency of verifications. Because no states are saved, restored, or checked within a d_step sequence, there can be no check on infinite executions within a d_step sequence. There can also be no check on the presence or absence of non-determinism within a d_step sequence. Use with caution.
Because one cannot jump into or out of a d_step sequence, the use of a do -loop as the last construct inside a d_step can produce unexpected effects. A break statement would cause an unintended exit from the d_step (because the state that follows the do construct lies outside the d_step in this case. The problem can be avoided by inserting a dummy skip after the loop, as follows.
d_step { .... do :: ....; break :: ... od ; skip /* add this to keep parser happy */ }
SEE ALSO
atomic(3), goto(3), sequence(3).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |