It is sometimes necessary to add auxiliary variables to a description
of an algorithm or system to show that it implements a higher-level
specification.
The paper Auxiliary Variables in TLA+ by Leslie Lamport and
Stephan Merz is a manual on how to do that for descriptions and
specifications written in TLA+.
This page contains a link to that paper and a link to a zip
file containing the TLA+ specifications of all the examples in
the paper.
The zip file contains the TLA+ source files of the
examples, their pretty-printed versions, and the toolbox directories
containing small TLC models for checking the specifications.
To run those models from the Toolbox, create specifications
for each of the following root modules:
MinMax2H,
SendInt1P,
SendSetUndoP,
SendSeqUndoP,
Hour,
LinearSnapshot,
NewLinearSnapshot,
AfekSimplifiedH.
Click here for the paper.
Right-click here to download the zip file.