E.3 Promela Example: Atomic Increment
Keywords: perfbook_html

#
E.3 Promela Example: Atomic Increment

Figure: Promela Code for Atomic Increment

Figure: Atomic Increment spin Output

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 .

Subsections

- E.3.1 Combinatorial Explosion