Auxiliary Variables in TLA+

Last modified 11 June 2017

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.