Skip to content

Cjen1/tla_increment

Repository files navigation

Specifications modelling multiple processes concurrently incrementing a shared variable

This set of specifications is useful for demonstrating many of the interesting properties of TLA+, TLC and model checking.

  • Single process increment_1.tla
    • Introduce TLA+ syntax and actions
    • Basic invariants and properties
    • Liveness properties, stuttering and fairness
  • Two processes increment_2.tla and the corrected increment_2_lock.tla
    • How to model non-determinism in the Next formula
    • Counter-examples for properties and how we can fix it in this case
  • Arbitrary processes increment_g.tla and increment_g_lock.tla
    • Complete (ish) TLA+ syntax
    • State space explosion (increase the number of processes in increment_g.cfg and increment_g_lock.cfg)
    • Symmetry reduction solving the state space explosion

To run: tlc2 increment_{variant}.tla.

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published