Home > Articles > Programming > General Programming/Other Languages

  • Print
  • + Share This
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).

  • + Share This
  • 🔖 Save To Your Account