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:

• No goto jumps into or out of a d_step sequence are allowed.
• The sequence is executed deterministically. If non-determinism is present, it is resolved in a fixed and deterministic way, for instance, by always selecting the first true guard in every selection and repetition structure.
• It is an error if the execution of any statement inside the sequence can block. This means, for instance, that in most cases send and receive statements cannot be used inside d_step sequences.

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 */
	}
	...
}

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