Files
specifications
Folders and files
Name | Name | Last commit date | ||
---|---|---|---|---|
parent directory.. | ||||
This is a directory of examples, containing the following subdirectories. allocator Specification of a resource allocator, written by Stephan Merz. CarTalkPuzzle A TLA+ specification of the solution to a nice puzzle. chang_roberts A PlusCal specification of the algorithm by Chang and Roberts (1979) for electing a leader on a unidirectional ring. DieHard A very elementary example based on a puzzle from a movie. It provides a good first introduction to TLA+. dijkstra-mutex A PlusCal version of the first published mutual exclusion algorithm, written by Edsger Dijkstra. ewd840 A TLA+ specification of an algorithm due to Dijkstra, Feijen, and van Gasteren for detecting distributed termination on a unidirectional ring, together with a safety proof. lamport_mutex A TLA+ specification of the distributed mutual-exclusion algorithm that appeared as an example in Lamport's classic paper "Time, Clocks and the Ordering of Events in a Distributed System", together with a hierarchical proof of mutual exclusion. MissionariesAndCannibals This is a very simple TLA+ spec that can be read by someone knowing nothing about TLA+. The spec, including all the TLA+ constructs it uses, are explained in comments. The pdf file contains a pretty-printed version of the actual spec. N-Queens TLA+ and PlusCal descriptions of a solution to the N queens problem. Written by Stephan Merz. Paxos A high-level specification of the Paxos consensus algorithm, consisting of a specification of consensus, a very high level spec of the algorithm (with no messages) that implements consensus and is implemented by the Paxos algorithm. Prisoners A simple specification that solves a puzzle that was presented on an American radio program. The solution is rather subtle, and hence it's not so easy to understand why the solution is correct. SpecifyingSystems Examples to accompany the book Specifying Systems. Stones Another specification that solves the same proble as CarTalkPuzzle. sums_even Two proofs for showing that x+x is even, for any natural number x. tower_of_hanoi The well-known Towers of Hanoi puzzle. transaction_commit TLA+ specifications underlying the paper "Consensus on Transaction Commit" by Gray and Lamport (2006). TransitiveClosure Someone once posted on TLAPlus.net a question asking how the transitive closure of a relation can be defined in TLA+. This answers the question by giving several equivalent definitions. Reading them might help you when you have to define some mathematical operation that requires a recursive definition. TwoPhase A specification of a very simple hardware protocol and of the problem it solves. This is a nice example of the use of instantiation to describe a refinement mapping, and of the use of constant operator parameters to describe unspecified actions. There is also a TLA+ proof of correctness that has been checked by the TLAPS proof system.