Promela Reference -- d_step(3)





d_step - introduces a deterministic sequence of code that is executed indivisibly.

d_step { sequence }

The differences between a d_step sequence and an atomic sequence are:

  • A d_step sequence is required to be deterministic. If non-determinism is nonetheless present, it is resolved in a fixed and deterministic way: i.e., the first true guard in selection or repetition structures may systematically be selected.
  • No goto jumps into or out of a d_step sequence are permitted.
  • The execution of a d_step sequence may not be blocked by an unexecutable statement. This means, for instance, that rendezvous statements cannot be used inside a d_step sequence.
  • A d_step sequence is executed as if it were one single statement, and is therefore more efficient to use during verifications than an atomic sequence. It provides a mechanism for adding new types of statements to the language, or new types of transitions in the underlying automata.


d_step {	/* swap the values of a and b */

	tmp = b;

	b = a;

	a = tmp


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 {



	:: ....; break

	:: ...


	; skip	/* add this to keep parser happy */


atomic(3), goto(3), sequence(3).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)