The Spin Model-Checking Tool
by Gerard J. Holzmann


Listing One
  1 Boolean array b(0;1) integer k, i, j,
  2 comment process i, with i either 0 or 1;
  3 C0: b(i) := false;
  4 C1: ifk != i then begin
  5 C2: if not (b(j) then go to C2;
  6     else k := i; go to C1 end;
  7     else critical section;
  8     b(i) := true;
  9     remainder of program;
 10     go to C0;
 11    end

Listing Two 
  1 int cnt, k, b[2];   /* all variables are initially 0 */
  2 
  3 active [2] proctype P()
  4 {
  5     assert(_pid == 0 || _pid == 1);
  6 
  7 C0: b[_pid] = 0;
  8 C1: if
  9     :: (k != _pid) ->
 10 C2:     (b[1 - _pid]);  /* wait for this to be nonzero */
 11         k = _pid;
 12         goto C1
 13 
 14     :: else ->
 15         cnt = cnt+1;
 16         assert(cnt == 1); /* the critical section */
 17         cnt = cnt-1;
 18 
 19         b[_pid] = 1;
 20     fi;
 21     goto C0
 22 }

Listing Three
  1:  proc  1 (P) line   5 "hy66" (state 1)  [assert(((_pid==0)||(_pid==1)))]
  2:  proc  1 (P) line   7 "hy66" (state 2)  [b[_pid] = 0]
  3:  proc  1 (P) line   9 "hy66" (state 3)  [((k!=_pid))]
  4:  proc  0 (P) line   5 "hy66" (state 1)  [assert(((_pid==0)||(_pid==1)))]
  5:  proc  0 (P) line   7 "hy66" (state 2)  [b[_pid] = 0]
  6:  proc  0 (P) line  14 "hy66" (state 7)  [else]
  7:  proc  0 (P) line  15 "hy66" (state 8)  [cnt = (cnt+1)]
  8:  proc  0 (P) line  16 "hy66" (state 9)  [assert((cnt==1))]
  9:  proc  0 (P) line  17 "hy66" (state 10) [cnt = (cnt-1)]
 10:  proc  0 (P) line  19 "hy66" (state 11) [b[_pid] = 1]
 11:  proc  1 (P) line  10 "hy66" (state 4)  [(b[(1-_pid)])]
 12:  proc  0 (P) line   7 "hy66" (state 2)  [b[_pid] = 0]
 13:  proc  0 (P) line  14 "hy66" (state 7)  [else]
 14:  proc  1 (P) line  11 "hy66" (state 5)  [k = _pid]
 15:  proc  1 (P) line  14 "hy66" (state 7)  [else]
 16:  proc  1 (P) line  15 "hy66" (state 8)  [cnt = (cnt+1)]
 17:  proc  1 (P) line  16 "hy66" (state 9)  [assert((cnt==1))]
 18:  proc  0 (P) line  15 "hy66" (state 8)  [cnt = (cnt+1)]
spin: line  16 "hy66", Error: assertion violated
 19:  proc  0 (P) line  16 "hy66" (state 9)  [assert((cnt==1))]
spin: trail ends after 19 steps
#processes: 2
                cnt = 2
                k = 1
                b[0] = 0
                b[1] = 0
 19:  proc  1 (P) line  17 "hy66" (state 10)
 19:  proc  0 (P) line  17 "hy66" (state 10)
2 processes created

Listing Four
_pid:   0   1
        |   |>assert(((_pid==0)||(_pid==1)))
        |   |>b[_pid] = 0
        |   |>((k!=_pid))
        |>assert(((_pid==0)||(_pid==1)))
        |>b[_pid] = 0
        |>else
        |>cnt = (cnt+1)
        |>assert((cnt==1))
        |>cnt = (cnt-1)
        |>b[_pid] = 1
        |   |>(b[(1-_pid)])
        |>b[_pid] = 0
        |>else
        |   |>k = _pid
        |   |>else
        |   |>cnt = (cnt+1)
        |   |>assert((cnt==1))
        |>cnt = (cnt+1)
        |>assert((cnt==1))  # assertion violated




