The TLA+ Hyperbook

The TLA+ Hyperbook

Last modified 7 April 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 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 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.)


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

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
Contact Us Terms of Use Trademarks Privacy Statement ©2010 Microsoft Corporation. All rights reserved.Microsoft