- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
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.