The TLA+ Hyperbook
The TLA+ Hyperbook
Last modified 14 July 2012
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.
You will probably read the hyperbook with Adobe Reader,
though other readers such as Foxit Reader should also work.
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.
Versions
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 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 chapter
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
chapter on Euclid's Algorithm.
- Added The Bounded Channel and Bounded Buffer,
the final chapter on both tracks.
- Began The Bounded Buffer chapter of the
Proof track.
- Made some further progress on the Math section.
