forked from tlaplus/Examples
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
92 lines (72 loc) · 3.02 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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.