The TLA+ Hyperbook
The TLA+ Hyperbook
Last modified 20 August 2015
This is the start of a hypertext "book" containing two tutorials:
Principles of Concurrent Computing and Specification of
The tutorials are two tracks that share much text--especially at the
Both tutorials are based
The Principles track, which I hope will eventually be suitable
for an undergraduate course on concurrent computing, will mainly use
the PlusCal algorithm language rather than
TLA+ for describing algorithms. There is also a TLA+
Proof track that explains how to use the TLAPS
You will probably read the hyperbook with Adobe Reader,
Other readers should also work, but it seems that Preview, the default
pdf reader on the Mac, does not.
I welcome comments and suggestions on the form, style, and
Also, please tell me if anything doesn't work as you think it should.
My email address is on my home page.
The hyperbook consists of a collection of pdf files; the root file is
start.pdf and the remaining files are in the folder
They are distributed as a zip file that you can download (save, do not open) by
Extract (unzip) the contents into a convenient folder and open (probably by
double-clicking on) the file
Be sure to follow the directions, which means clicking where it says
If you are just starting to read
this hyperbook, click here.
This leads you to the introduction About This Hyperbook.
You will then know what to do next.
I am still rewriting some parts of the hyperbook, so some material may
be in an inconsistent state. Read the About This Hyperbook
page for more information . (Click on "If you are just starting..."
from the start page or on the "?" in the left margin from most other
The LaTeX sources for the hyperbook have been released.
The Source Files
The LaTeX source files for the hyperbook are now available for
One reason for this is to encourage you to contribute your own
material to the hyperbook.
(Contact me before starting if you want that material to appear
in the official release of the hyperbook.)
You could also write your own hypertext documents using the
commands that I created for the purpose.
Reading the source files will allow you to figure out how to do
it. The file hypertlabook.sty and the packages it imports
define the relevant commands.
The source files can be downloaded
Extracting the files from thie zip file creates a folder (directory)
To create the pdf files that constitute the hyperbook, open a Unix
shell window from which you can run
and connect to the
(To do this in Windows, you can install
In that shell, run the command
I hope to post new versions of the hyperbook continually.
So, far I haven't been very good at doing that, but I hope to do
better. Major changes will be announced on
TLA+ Google Group.
However, I may post a new version and change the last modified
date of this page whenever something you should read has changed--even
if it's just the correction of a minor typo.
Downloading and unzipping a file is easy, so check this page
- Version of 20 August 2015
Rewrote Section 8 (Bounded Channel and Bounded Buffer)
Revised Section 7.9 (Mutual Exclusion in Modern Programs).
Revised Section 18 (Now titled
Variable Hiding and Auxiliary Variables)
- Version of 28 February 2015
Revised Section 7 (Mutual Exclusion)
Revised Sections 10-12 of
The TLA+ Proof Track.
Rewrote Section 17 (Temporal Logic).
- Version of 24 March 2014
Revised the first two sections of
The TLA+ Proof Track
to conform to the current version
and added a section explaining the proof language.
- Version of 28 November 2013
Finished Section 7.8 on the bakery algorithm.
- Version of 19 November 2013
- Rewrote material explaining temporal logic and moved
it to Section 17 of the Math track.
- Rewrote the first six sections of the Mutual Exclusion
section of the Principles track.
- Version of 24 May 2013
- Moved the old section 4 (The Bounded Channel and Bounded Buffer)
to section 8
of the Principles track.
- Added sections 3 and 5 on the Die Hard problem
and section 6 on Alternation.
- Rewrote much of the rest of sections 1, 2, and 4.
- Continued writing section 7 (Mutual Exclusion)
- Version of 14 July 2012
- Finished description of the One-Bit Protocol
in Section 5 of the Principles track.
- Modified the Proof track to describe the SMT backend prover.
- Corrected an error in the Simple PlusCal Reduction Theorem
in Section 4.8.
- Version of 12 April 2012
- Added Section 8, An Input/Output Specification on
the Specification track.
- Began a new Section 19, Debugging with TLC.
- Began the Principles track.
- Added descriptions of
- Version of 30 January 2012
- Added a summary of TLA+, reachable from the S
button on each page.
- Finished the Miscellaneous Constructs section
of the Math section.
- Added a tiny start of the Specification track.
- Gave up trying to indicate recent modifications
in the document.
- Version of 10 October 2011
- Expanded Section 3.7 and added Section 3.8 in the
section on Euclid's Algorithm.
- Added The Bounded Channel and Bounded Buffer,
the final section on both tracks.
- Began The Bounded Buffer section of the
- Made some further progress on the Math section.