Concurrent increments to a shared variable

[Cjen1]

I've been using the example of concurrently incrementing a shared variable for demonstrating TLA+.

Since this can be split up into t = i, and i = t + 1 actions, it demonstrates many of the interesting facets of TLA+ model checking while being a tiny example:

• Basic TLA+ syntax and TLC usage
• Non-determinism
• Counter-examples
• Liveness and fairness
• State space explosion and symmetry reduction

[lemmy]

Thanks @Cjen1, can you open a PullRequest that adds your example to https://github.com/tlaplus/Examples/blob/master/README.md ?