It is easy to fix this example by placing the body of the incrementer
processes in an atomic blocks as shown in
Figure .
One could also have simply replaced the pair of statements with
counter = counter + 1, because Promela statements are
atomic.
Either way, running this modified model gives us an error-free traversal
of the state space, as shown in
Figure
.