The TLA+ Hyperbook

The TLA+ Hyperbook

Last modified 20 August 2015

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

You will probably read the hyperbook with Adobe Reader, but 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 contents.  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 clicking hereExtract (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 pages.)

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 download.  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 by clicking here.  Extracting the files from thie zip file creates a folder (directory) hyper-tla.  To create the pdf files that constitute the hyperbook, open a Unix shell window from which you can run pdflatex and connect to the hyper-tla folder.  (To do this in Windows, you can install Cygwin.)  In that shell, run the command sh


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 the 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 regularly.

Version of 20 August 2015
Version of 28 February 2015
Version of 24 March 2014
Version of 28 November 2013
Version of 19 November 2013
Version of 24 May 2013
Version of 14 July 2012
Version of 12 April 2012
Version of 30 January 2012
Version of 10 October 2011