console.txt

$ spin -a lock.spin
$ gcc -o pan pan.c
$ ./pan

(Spin Version 6.4.6 -- 2 December 2016)
        + Partial Order Reduction

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        acceptance   cycles     - (not selected)
        invalid end states      +

State-vector 36 byte, depth reached 43, errors: 0
       51 states, stored
       94 states, matched
      145 transitions (= stored+matched)
       17 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.003       equivalent memory usage for states (stored*(State-vector + overhead))
    0.290       actual memory usage for states
  128.000       memory used for hash table (-w24)
    0.534       memory used for DFS stack (-m10000)
  128.730       total actual memory usage


unreached in proctype locker
        lock.spin:29, state 21, "-end-"
        (1 of 21 states)

pan: elapsed time 0 seconds

lock.spin

bit mutex = 0;
int sum;

inline lock() {
  do
    :: 1 -> atomic {
      if
      :: mutex == 0
        sum++
        mutex = 1
        sum--
        break
      :: else
      fi
    }
  od
}

inline unlock() {
  mutex = 0
}

active [3] proctype locker() {
  do
    :: lock()
       unlock()
  od
}

proctype側のelseは到達しないと指摘。たしかにinline lockの 1 があるのでここにはこないなあ。