/TLA-Examples

A collection of TLA+ specifications of varying complexities

Primary LanguageTLAOtherNOASSERTION

Welcome to TLA+ Examples Gitpod ready-to-code

The page TLA+ Examples is a library of TLA+ specifications for distributed algorithms. The webpage supplies the TLA+ community with:

  • A comprehensive library of the TLA+ specifications that are available today, in order to provide an overview of how to specify an algorithm in TLA+.
  • A comprehensive list of references and other interesting information for each problem.

Do you have your own case study that you like to share with the community? Send a pointer to us and we will include it in the repository. Your specifications will help the community in improving the tools for TLA+ analysis.

List of Examples

No Name Short description Spec's authors TLAPS Proof TLC Check Used modules PlusCal Apalache
1 2PCwithBTM A modified version of P2TCommit (Gray & Lamport, 2006) Murat Demirbas ✔ FinSet, Int, Seq ✔
2 802.16 IEEE 802.16 WiMAX Protocols Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou ✔ Int, Seq, FinSet
3 aba-asyn-byz Asynchronous Byzantine agreement (Bracha & Toueg, 1985) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat
4 acp-nb Non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) Stephan Merz ✔ default theories
5 acp-nb-wrong Wrong version of the non-blocking atomic commitment with a reliable broadcast (Babaoğlu & Toueg, 1993) Stephan Merz ✔ default theories
6 acp-sb Non-blocking atomic commitment with a simple broadcast (Babaoğlu & Toueg, 1993) Stephan Merz ✔ default theories
7 allocator Specification of a resource allocator Stephan Merz ✔ FinSet
8 async-comm The diversity of asynchronous communication (Chevrou et al., 2016) Florent Chevrou, Aurélie Hurault, Philippe Quéinnec ✔ Nat
9 bcastByz Asynchronous reliable broadcast - Figure 7 (Srikanth & Toeug, 1987) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ ✔ Nat, FinSet
10 bcastFolklore Folklore reliable broadcast - Figure 4 (Chandra and Toueg, 1996) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ ✔ Nat
11 bosco One-Step Byzantine asynchronous consensus (Song & Renesse, 2008) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat, FinSet
12 Boulangerie A variant of the bakery algorithm (Yoram & Patkin, 2015) Leslie Lamport, Stephan Merz ✔ ✔ Int ✔
13 byihive Based on RFC3506 - Requirements and Design for Voucher Trading System (Fujimura & Eastlake) Santhosh Raju ✔ default theories
14 byzpaxos Byzantizing Paxos by Refinement (Lamport, 2011) Leslie Lamport ✔ Int, FinSet
15 c1cs Consensus in one communication step (Brasileiro et al., 2001) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int, FinSet
16 Caesar Multi-leader generalized consensus protocol (Arun et al., 2017) Giuliano Losa ✔ FinSet, Seq, Int ✔
17 CarTalkPuzzle A TLA+ specification of the solution to a nice puzzle. ✔ Int
18 CASPaxos An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov) Tobias Schottdorf ✔ Int, FinSet
19 cbc_max Condition-based consensus (Mostefaoui et al., 2003) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int, FinSet
20 cf1s-folklore One-step consensus with zero-degradation (Dobre & Suri, 2006) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat
21 ChangRoberts Leader election in a ring (Chang & Roberts, 1979) Stephan Merz ✔ Nat, Seq ✔
22 DataPort Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016) Geoffrey Biggs, Noriaki Ando Int, Seq
23 detector_chan96 Chandra and Toueg’s eventually perfect failure detector Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int, FinSet
24 DieHard A very elementary example based on a puzzle from a movie ✔ Nat
25 dijkstra-mutex Mutual exclusion algorithm (Dijkstra, 1965) ✔ Int ✔
26 diskpaxos Disk Paxos (Gafni & Lamport, 2003) Leslie Lamport, Giuliano Losa ✔ Int
27 egalitarian-paxos Leaderless replication protocol based on Paxos (Moraru et al., 2013) Iulian Moraru ✔ Nat, FinSet
28 ewd840 Termination detection in a ring (Dijkstra et al., 1986) Stephan Merz ✔ ✔ Nat
70 ewd998 Shmuel safra's version of termination detection Stephan Merz, Markus Kuppe ✔ Int, FinSet
29 fastpaxos An extension of the classic Paxos algorithm, only PDF files (Lamport, 2006) Leslie Lamport Nat, FinSet
30 fpaxos A variant of Paxos with flexible quorums (Howard et al., 2017) Heidi Howard ✔ Int
31 HLC Hybrid logical clocks and hybrid vector clocks (Demirbas et al., 2014) Murat Demirbas ✔ Int ✔
32 L1 Data center network L1 switch protocol, only PDF files (Thacker) Tom Rodeheffer FinSet, Nat, Seq
33 lamport_mutex Mutual exclusion (Lamport, 1978) Stephan Merz ✔ ✔ Nat, Seq
34 leaderless Leaderless generalized-consensus algorithms (Losa, 2016) Giuliano Losa ✔ FinSet, Int, Seq ✔
35 losa_ap The assignment problem, a variant of the allocation problem (Delporte-Gallet, 2018) Giuliano Losa ✔ FinSet, Nat, Seq ✔
36 losa_rda Applying peculative linearizability to fault-tolerant message-passing algorithms and shared-memory consensus, only PDF files (Losa, 2014) Giuliano Losa FinSet, Nat, Seq
37 m2paxos Multi-leader consensus protocols (Peluso et al., 2016) Giuliano Losa ✔ Int, Seq, FinSet
38 mongo-repl-tla A simplified part of Raft in MongoDB (Ongaro, 2014) Siyuan Zhou ✔ FinSet, Nat, Seq
39 MultiPaxos The abstract specification of Generalized Paxos (Lamport, 2004) Giuliano Losa ✔ Int, FinSet
40 N-Queens The N queens problem Stephan Merz ✔ Nat, Seq ✔
41 naiad Naiad clock protocol, only PDF files (Murray et al., 2013) Tom Rodeheffer ✔ Int, Seq, FinSet
42 nbacc_ray97 Asynchronous non-blocking atomic commit (Raynal, 1997) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat, FinSet
43 nbacg_guer01 On the hardness of failure-sensitive agreement problems (Guerraoui, 2001) Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Nat, FinSet
44 nfc04 Non-functional properties of component-based software systems (Zschaler, 2010) Steffen Zschaler ✔ Real, Nat
45 Paxos Paxos consensus algorithm (Lamport, 1998) Leslie Lamport ✔ Int, FinSet
46 Prisoners A puzzle that was presented on an American radio program. ✔ Nat, FinSet
47 raft Raft consensus algorithm (Ongaro, 2014) Diego Ongaro ✔ FinSet, Nat, Seq
48 SnapshotIsolation Serializable snapshot isolation (Cahill et al., 2010) Michael J. Cahill, Uwe Röhm, Alan D. Fekete ✔ FinSet, Int, Seq
49 spanning Spanning tree broadcast algorithm in Attiya and Welch’s book Thanh Hai Tran, Igor Konnov, Josef Widder ✔ Int
50 SpecifyingSystems Examples to accompany the book Specifying Systems (Lamport, 2002) ✔ all modules
51 Stones The same problem as CarTalkPuzzle ✔ FinSet, Int, Seq
52 sums_even Two proofs for showing that x+x is even, for any natural number x. ✔ ✔ Int
53 SyncConsensus Synchronized round consensus algorithm (Demirbas) Murat Demirbas ✔ FinSet, Int, Seq ✔
54 Termination Channel-counting algorithm (Kumar, 1985) Giuliano Losa ✔ Integers, FiniteSets, Apalache, Sequences ✔ ✔
55 Tla-tortoise-hare Robert Floyd's cycle detection algorithm Lorin Hochstein ✔ Nat ✔
56 tower_of_hanoi The well-known Towers of Hanoi puzzle. Markus Kuppe, Alexander Niederbühl ✔ Bit, FinSet, Int, Nat, Seq
57 transaction_commit Consensus on transaction commit (Gray & Lamport, 2006) Leslie Lamport ✔ Int
58 TransitiveClosure The transitive closure of a relation ✔ FinSet, Int, Seq
59 TwoPhase Two-phase handshaking Leslie Lamport, Stephan Merz ✔ Nat
60 VoldemortKV Voldemort distributed key value store Murat Demirbas ✔ FinSet, Int, Seq ✔
61 Missionaries and Cannibals Missionaries and Cannibals Leslie Lamport ✔ FinSet, Int
62 Misra Reachability Algorithm Misra Reachability Algorithm Leslie Lamport ✔ ✔ Int, Seq, FiniteSets, TLC, TLAPS, NaturalsInduction ✔
63 Loop Invariance Loop Invariance Leslie Lamport ✔ ✔ Int, Seq, FiniteSets, TLC, TLAPS, SequenceTheorems, NaturalsInduction ✔
64 Teaching Concurrency Teaching Concurrency Leslie Lamport ✔ ✔ Int, TLAPS ✔
65 Spanning Tree Spanning Tree Leslie Lamport ✔ Int, FiniteSets, TLC, Randomization
66 Paxos (How to win a Turing Award) Paxos Leslie Lamport ✔ Nat, Int, FiniteSets
67 Tencent-Paxos PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment(Zheng et al., 2017) Xingchen Yi, Hengfeng Wei ✔ ✔ Int, FiniteSets
68 Blocking Queue BlockingQueue Markus Kuppe ✔ ✔ (LiveEnv) Naturals, Sequences, FiniteSets
69 Paxos Paxos ✔ Int, FiniteSets
71 Echo Algorithm Echo Algorithm Stephan Merz ✔ Naturals, FiniteSets, Relation, TLC ✔
72 Cigarette Smokers problem Cigarette Smokers problem Mariusz Ryndzionek ✔ Integers, FiniteSets
73 Conway's Game of Life Conway's Game of Life Mariusz Ryndzionek ✔ Integers
74 Sliding puzzles Sliding puzzles Mariusz Ryndzionek ✔ Integers
75 Lock-Free Set PlusCal spec of a lock-Free set used by TLC Markus Kuppe ✔ Sequences, FiniteSets, Integers, TLC ✔
76 Chameneos Chameneos, a Concurrency Game Mariusz Ryndzionek ✔ Integers
77 ParallelRaft A variant of Raft Xiaosong Gu, Hengfeng Wei, Yu Huang ✔ Integers, FiniteSets, Sequences, Naturals
78 TLC MC PlusCal spec of safety checking as implemented in TLC Markus Kuppe ✔ Integers, FiniteSets, Sequences, TLC ✔
79 TLA+ Level Checking Level-checking of TLA+ formulas as described in Specifying Systems Leslie Lamport Integers, Sequences
80 CRDT-Bug CRDT algorithm with defect and fixed version Alexander Niederbühl ✔ FiniteSets, Naturals, Sequences
81 asyncio-lock Bugs from old versions of Python's asyncio lock Alexander Niederbühl ✔ Sequences
82 Single Lane Bridge problem Single Lane Bridge Younes Akhouayri ✔ Naturals, FiniteSets, Sequences
83 Raft (with cluster changes) Raft with cluster changes, and a version with Apalache type annotations but no cluster changes George Pîrlea, Darius Foom, Brandon Amos, Huanchen Zhang, Daniel Ricketts ✔ Functions, SequencesExt, FiniteSetsExt, TypedBags ✔
84 EWD687a Detecting termination in distributed computations by Edsger Dijkstra and Carel Scholten Stephan Merz (PlusCal spec), Leslie Lamport & Markus Kuppe (TLA+ spec) ✔ Integers, Graphs ✔
85 Huang Termination detection by using distributed snapshots by Shing-Tsaan Huang Markus Kuppe ✔ DyadicRationals
86 Azure Cosmos DB Consistency models provided by Azure Cosmos DB Dharma Shukla, Ailidani Ailijiang, Murat Demirbas, Markus Kuppe ✔ Integers, Sequences, FiniteSets, Functions, SequencesExt ✔
87 MET for CRDT-Redis Model-check the CRDT designs, then generate test cases to test CRDT implementations Yuqi Zhang ✔ Integers, Sequences, FiniteSets, TLC ✔
88 Parallel increment Parallel threads incrementing a shared variable. Demonstrates invariants, liveness, fairness and symmetry Chris Jensen ✔ Integers, FiniteSets, TLC
89 The Streamlet consensus algorithm Specification and model-checking of both safety and liveness properties of Streamlet with TLC Giuliano Losa ✔ Sequences, Integers, FiniteSets ✔
90 Petri Nets Instantiable Petri Nets with liveness properties Eugene Huang ✔ Integers, Sequences, FiniteSets, TLC
91 Knuth Yao & Markov Chains Knuth-Yao algorithm for simulating a sixsided die Ron Pressler, Markus Kuppe ✔ DyadicRationals

License

The repository is under the MIT license. However, we can upload your benchmarks under your license.

Support or Contact

Do you have any questions or comments? Please open an issue or send an email to the TLA+ group.