The promela language used to construct spin models is relatively easy to pick up. However, composing a model, which doesn’t introduce unnecessary states, is still black magic. Here is a list of seemingly pointless changes, that cuts down the exploration space significantly.

§Favor disable actions over enable actions

The following is a model of Peterson’s mutex algorithm; the commented code in monitor is enabled all the time, then spin needs to explore its interleaving with all other statements, while the alternative way has the guard, which become true only when the assertion is doomed to fail.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
#define turn1 0
#define turn2 1

bool x1, x2, t

byte mutex

active proctype p1() {
start1:
  x1 = true
  t = turn2

  x2 == false || t == turn1

  mutex++

  mutex--

  x1 = false

  goto start1
}

active proctype p2() {
start2:
  x2 = true
  t = turn1

  x1 == false || t == turn2

  mutex++

  mutex--
  x2 = false
  goto start2
}

active proctype monitor() {
  /* assert(mutex <= 1) */
  mutex > 1 -> assert(mutex <= 1)
}

§Reduce the number of live processes

In theory, I can put the content of checker right after done++. However, then all N processes are alive while performing d_step. Alternatively, having a separate process to do final checking reduces the size of the state space.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
#define N 5
chan channel[N] = [1] of { byte }

int candidates[N] = -1
byte done

active [N] proctype actor() {

  byte prev;
  byte x;
  if
  :: _pid == 0 -> prev = N - 1
  :: else -> prev = _pid - 1
  fi

  if
  :: goto initiator
  :: goto forwarder
  fi

initiator:
  channel[_pid] ! _pid
  byte min = _pid
  loop:
    channel[prev] ? x
    if
    :: x < min -> min = x
    :: x == _pid ->
      candidates[_pid] = min
      goto exit
    :: else -> skip
    fi
    channel[_pid] ! x
    goto loop

forwarder:
  do
  :: channel[prev] ? x ; channel[_pid] ! x
  :: timeout -> goto exit
  od

exit:
  done++
}

active proctype checker() {
  done == N
  d_step {
    byte leader
    int i
    /* check single leader */
    for (i in candidates) {
      if
      :: candidates[i] != -1 && leader == 0 -> leader = candidates[i]
      :: candidates[i] != -1 && leader != 0 -> assert(leader == candidates[i])
      :: else
      fi
    }
  }
}