TLA+ Specs

My TLA+ specifications, mostly written in Pluscal.

• 2-phase commit: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/2-phase-commit
• 3-phase commit: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/3-phase-commit
• An incorrect way to model a lease algorithm: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/lease-buggy-code
• Lamport Clock used to solve mutual exclusion problem: logical-clocks-and-mutual-exclusion
• Modeling of the solution for the problem of Missionaries and Cannibals: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/missionaries_and_cannibals_problem
• I've started watching this talk "Weeks of debugging can save you hours of TLA+", and thought it would be fun to stop it and try to find the bug myself in tla+: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/weeks_of_debugging
• Wolf, Goat and Cabbage is similar to the Missionaries and cannibals problem. A fun exercise to improve my tla+: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/wolf_goat_cabbage
• Chandy-lamport distributed snapshots algorithm: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/chandy-lamport-distributed-snapshots

Posts:

I've also written some blog posts on TLA+:

• TLA+ is easy if you know how to abstract
• Wolf, goat and cabbage problem
• Lamport clocks
• Distributed Snapshots: Chandy-Lamport protocol