examples

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.
   
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.

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.
   
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.
   
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.