The TLA+ Hyperbook

The hyperbook is an unfinished hypertext document that was meant to be what one would read to learn TLA+ and PlusCal.  The TLA+ Video Course now serves as an introduction to TLA+, and The PlusCal Tutorial is an introduction to PlusCal.  I have stopped working on the hyperbook and don't know what to do with it.  (I would welcome suggestions.)

The first 6 chapters of the hyperbook cover approximately the same material as the Video Course, but in greater depth and with different examples.  It also teaches the use of PlusCal.  Chapters 7 through 9 provide more realistic examples.  The hyperbook's TLA+ Proof Track is probably the best introduction to writing TLA+ proofs and checking them with the TLAPS prover.

The rest of this web page describes the state of the hyperbook at the time of the last release, in 2015.

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. 

IMPORTANT   The Hyperbook uses many popups.  To make them appear as popops, the pdf reader must be set to open new files in a new window, rather in a new tab in the same window.  Here's how to get Adobe Reader to do this: Click on Edit, choose Preferences and then General.  Then uncheck the box labeled Open documents as new tabs in the same window (requires relaunch).  You must then close and reopen the reader.  Also, the Hyperbook consists of many separate pdf files.  If you don't like the way your reader displays a file, you can change things like the sizes of the text and the window.  Here is how to get Adobe Reader to remember those changes the next time you view the file: Click on Edit, choose Preferences and then Documents.   Then check the box labeled Restore last view settings when reopening documents.

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 here.  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 pages.)

The LaTeX sources for the hyperbook have been released.  See below.

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

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