The TLA+ Hyperbook

Last modified 28 February 2014

The Hyperbook

This is the start of a hypertext “book” containing two tutorials:
Principles of Concurrent Computing and Specification of
Concurrent Systems

The tutorials are two tracks that share much text–especially at the

Both tutorials are based
on TLA+

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+
track that explains how to use the TLAPS
proof system

You will probably read the hyperbook with Adobe Reader,
Foxit Reader
also works. 

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
(directory) hyper-tla

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 start.pdf

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

Read it. 

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. 
See below.

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 hyper-tla folder. 

(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.  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 February 2015
  • Revised Section 7 (Mutual Exclusion)
  • Revised Section 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
    of TLAPS,
    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 LAMBDA, SUBSET
    and UNION.


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
    Proof track.
  • Made some further progress on the Math section.

Original URL:

Original article

Comments are closed.

Proudly powered by WordPress | Theme: Baskerville 2 by Anders Noren.

Up ↑

%d bloggers like this: