The Current State of the Hyperbook [show]
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 I'm recommending Hillel Wayne's Web Site and Book as 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.
The Hyperbook [show]
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.
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
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 [show]
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
Extracting the files from thie zip file creates a folder (directory)
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.