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