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
}
}
}