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:

• 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.

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).