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.

glowingRaccoon
   A specification of PCR using refinement mapping in TLA+.

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.

SDP_Verification
   This project is about the TLA+ Spec of SDP architecture and algorithm 
   written by Luming Dong and Zhi niu based on the open source project fwknop.
   The subdirectory SDP_Attack_Spec contains the specification based on the 
   following materials:(* https://cloudsecurityalliance.org/artifacts/software-defined-perimeter-zero-trust-specification-v2/)(http://www.cipherdyne.org/fwknop/ *)
   The verification results show that current SDP protocol framework has a vulnerability 
   in the scenario of remote access through NAT technology.
   The subdirectory SDP_Attack_New_Solution_Spec contains the specification for the improved 
   SDP architecture design which fixed the flaw related to service concealment feature.