tlaplus / Examples
Licence: other
A collection of TLA+ specifications of varying complexities
Stars: โญ 720
Projects that are alternatives of or similar to Examples
Merkletreejs
๐ฑ Construct Merkle Trees and verify proofs in JavaScript.
Stars: โญ 238 (-66.94%)
Mutual labels: algorithm, protocol
Drtlaplus
Dr. TLA+ series - learn an algorithm and protocol, study a specification
Stars: โญ 561 (-22.08%)
Mutual labels: algorithm, protocol
Quickfixj
QuickFIX/J is a full featured messaging engine for the FIX protocol. - This is the official project repository.
Stars: โญ 638 (-11.39%)
Mutual labels: protocol
Ahocorasickdoublearraytrie
An extremely fast implementation of Aho Corasick algorithm based on Double Array Trie.
Stars: โญ 695 (-3.47%)
Mutual labels: algorithm
Turf
A modular geospatial engine written in JavaScript
Stars: โญ 6,659 (+824.86%)
Mutual labels: algorithm
Algorithms
Data Structure Libraries and Algorithms implementation
Stars: โญ 624 (-13.33%)
Mutual labels: algorithm
Tech Refrigerator
๐ฐ ๊ธฐ์ ๋์ฅ๊ณ ์
๋๋ค. ๐ ๊ธฐ์ ๋ฉด์ , ์ ๊ณต ์ํ , ์ง์ ํจ์ ๋ฑ ๋ถ๋ช
๋์๋ ๊ฑฐ์์! ๐ค
Stars: โญ 699 (-2.92%)
Mutual labels: algorithm
Arabiccompetitiveprogramming
The repository contains the ENGLISH description files attached to the video series in my ARABIC algorithms channel.
Stars: โญ 675 (-6.25%)
Mutual labels: algorithm
Dsa.js Data Structures Algorithms Javascript
๐ฅData Structures and Algorithms explained and implemented in JavaScript + eBook
Stars: โญ 6,251 (+768.19%)
Mutual labels: algorithm
Jcsprout
๐จโ๐ Java Core Sprout : basic, concurrent, algorithm
Stars: โญ 26,536 (+3585.56%)
Mutual labels: algorithm
Goraph
Package goraph implements graph data structure and algorithms.
Stars: โญ 635 (-11.81%)
Mutual labels: algorithm
Light Tips
Some code tips about algorithms, php and more ๐ฅ
Stars: โญ 705 (-2.08%)
Mutual labels: algorithm
Get better at cp in 2 months
This contains the curriculum that I will follow to get better at Competitive Programming in 2 months.
Stars: โญ 627 (-12.92%)
Mutual labels: algorithm
Node Minecraft Protocol
Parse and serialize minecraft packets, plus authentication and encryption.
Stars: โญ 697 (-3.19%)
Mutual labels: protocol
Multihash
Self describing hashes - for future proofing
Stars: โญ 656 (-8.89%)
Mutual labels: protocol
Ipban
IPBan Monitors failed logins and bad behavior and bans ip addresses on Windows and Linux. Highly configurable, lean and powerful. Learn more at -->
Stars: โญ 652 (-9.44%)
Mutual labels: protocol
Xviz
A protocol for real-time transfer and visualization of autonomy data
Stars: โญ 691 (-4.03%)
Mutual labels: protocol
Welcome to TLA+ Examples
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 |
|---|---|---|---|---|---|---|---|
| 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 (Mattern, 1987) | Giuliano Losa | โ | FinSet, Bags, Nat | โ | |
| 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 |
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.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].