Home > Articles > Programming > General Programming/Other Languages

  • Print
  • + Share This
This chapter is from the book

Deterministic Steps

Another way to define an indivisible sequence of actions is to use the d_step statement. In the above case, for instance, we could also have written:

d_step { /* swap the values of a and b */
       tmp = b;
       b = a;
       a = tmp

Unlike an atomic sequence, a d_step sequence is always executed as if it were a single statement: it is intended to provide a means for defining new types of primitive statements in PROMELA. This restricts the use of d_step sequences in several ways, compared to atomic sequences:

  • The execution of a d_step sequence is always deterministic. If non-determinism is encountered in a d_step sequence, it is resolved in a fixed way, for example, by executing the first true guard in each non-deterministic selection or repetition structure. The precise way in which the non-determinism inside d_step sequences is resolved is undefined.

  • No goto jumps into or out of d_step sequences are permitted: they will be flagged as errors by the SPIN parser.

  • The execution of a d_step sequence may not be interrupted by blocking statements. It is an error if any statement other than the first one (the guard statement) in a d_step sequence is found to be unexecutable.

None of the above three restrictions apply to atomic sequences. This means that the keyword d_step can always be replaced with the keyword atomic, but not vice versa. It is safe to embed d_step sequences inside atomic sequences, but the reverse is not allowed.

  • + Share This
  • 🔖 Save To Your Account