The TLA+ Hyperbook
The TLA+ Hyperbook
Last modified 28 November 2013
I have begun rewriting the hyperbook from the beginning to make it
easier to read and more relevant to ordinary engineers. The first six
sections, which constitute the part common to all tracks, have been
completed. Other 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 pages.)
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.
You will probably read the hyperbook with Adobe Reader,
though other readers such as Foxit Reader should also work.
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 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. The web site
TLA+ | The Way To Specify
may announce major changes.
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 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.