Examples for TLA+ Proof System
Adapted from the examples accompany with the tlaps tool.
- Euclid
- Euclid-Hyperbook
- Proofs about Euclid's Algorithm.
- Ref: Chapter 11 "Correctness of Euclid's Algorithm" of Hyperbook
- Euclid-TLAPS-Example
- Proofs about Euclid's Algorithm.
- From tlaps/examples
- Euclid-Hyperbook
TODO: re-organized
Allocator.tla: allocator managing a set of resources
Bakery.tla AtomicBakery.tla AtomicBakeryWithoutSMT.tla different versions of Lamport's bakery algorithm, Bakery.tla being the most faithful representation with non-atomic operations on shared registers
BubbleSort.tla the classic BubbleSort algorithm as a PlusCal algorithm, and its correctness proof
Euclid.tla proofs about Euclid's algorithm for computing the GCD of two positive integers, cf. the TLAPS tutorial
Peterson.tla: Peterson's algorithm for mutual exclusion between two processes using shared memory
SimpleMutex.tla: the essence of many mutual exclusion protocols
SumAndMax.tla: a simple challenge problem from VSTTE 2010
Sub-directories:
paxos/Paxos.tla TLA+ specification of the Paxos consensus algorithm and a proof of its correctness (safety)
two-phase/*.tla two-phase handshake
cantor/Cantor*.tla several proofs of Cantor's theorem using TLA+'s hierarchical proof language
consensus/PaxosProof.tla high level specification of Consensus with two refinements implementing an abstract Paxos algorithm (incomplete and largely superseded by paxos/)
data/*.tla various theorems on sets, sequences and graphs (incomplete)