- 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
Process execution is normally only guided by the rules of synchronization captured in the statement semantics of proctype specifications. It is possible, though, to define additional global constraints on process executions. This can be done with the help of the keyword provided which can follow the parameter list of a proctype declaration, as illustrated in the following example:
bool toggle = true; /* global variables */
short cnt; /* visible to A and B */
active proctype A() provided (toggle == true)
{
L: cnt++; /* means: cnt = cnt+1 */
printf("A: cnt=%d\n", cnt);
toggle = false; /* yield control to B */
goto L /* do it again */
}
active proctype B() provided (toggle == false)
{
L: cnt--; /* means: cnt = cnt-1 */
printf("B: cnt=%d\n", cnt);
toggle = true; /* yield control to A */
goto L
}
The provided clauses used in this example force the process executions to alternate, producing an infinite stream of output:
$ spin toggle.pml | more
A: cnt=1
B: cnt=0
A: cnt=1
B: cnt=0
A: cnt=1
B: cnt=0
A: cnt=1
...
A process cannot take any step unless its provided clause evaluates to true. An absent provided clause defaults to the expression true, imposing no additional constraints on process execution.
Provided clauses can be used to implement non-standard process scheduling algorithms. This feature can carry a price-tag in system verification, though. The use of provided clauses can disable some of SPIN’s most powerful search optimization algorithms (cf. Chapter 9).