TLA+ | The way to specify

Specifying Systems

The book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers is published by Addison-Wesley Professional, a division of Pearson Education.

The Book

The book is 364 pages long (including a 17-page index). However, most people will want to read only the first part, which comprises the first seven chapters and is 83 pages long. Here is the list of chapters:

1. A Little Simple Math
2. Specifying a Simple Clock
3. An Asynchronous Interface
4. A FIFO
5. A Caching Memory
6. Some More Math
7. Writing a Specification: Some Advice
8. Liveness and Fairness
9. Real Time
10. Composing Specifications
11. Advanced Examples
12. The Syntactic Analyzer
13. The TLATeX Typesetter
14. The TLC Model Checker
15. The Syntax of TLA+
16. The Operators of TLA+
17. The Meaning of a Module
18. The Standard Modules

How to Get It

You can order your copy from the publisher or from Amazon.

You can also download an electronic copy for your own use from this website. Please note that the book Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers by Leslie Lamport is copyright ©2002 by Pearson Education, Inc. It may not be reproduced or distributed for commercial purposes, or for any purpose other than for personal use, without the prior written permission of the publisher.

book-06-18-02 (June 18, 2002)

The List of Corrections

The list of all known errors and omissions in the book can be downloaded below.

errata.pdf (March 14, 2009)

Feel free to report typos and errors, if you find any. If you are the first to report an error, you will be acknowledged in any new edition.

Accompanying Material

Also available for downloading is material to accompany the book. This includes the ASCII versions of all specifications from the book, additional modules and configuration files for using the TLC model checker to check some of the specifications, and a few exercises.

The material is organized hierarchically, with the material for each chapter in a separate folder (directory). Each folder, including the root, has a README file containing the exercises and an explanation of what else is in the directory. The material is available as a Zip file for Windows users and as a gzipped tar file for Linux/Unix users.

Windows ZIP file
Unix gzipped tar file

The examples and the exercises are discussed in the Examples section in more detail.

Reference

• [2002,book] bibtex
  L. Lamport, Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2002.
  @book{DBLP_books_aw_Lamport2002,
  author = {Leslie Lamport},
  title = {Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers},
  publisher = {Addison-Wesley},
  year = {2002},
  isbn = {0-3211-4306-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

PlusCal Manual

The introduction to the PlusCal manual explains how algorithms differ from programs, and how PlusCal differs from programming languages. There are two alternate syntaxes: the original, somewhat prolix p-syntax and a new, more compact c-syntax. The c-syntax is closer to that of C-based languages like C# and Java, using braces { and } instead of begin/do and end. There is a separate version of the manual for each syntax; the two syntaxes are briefly compared in both versions.

p-manual-01-02-09.pdf (January 02, 2009)
c-manual-01-02-09.pdf (January 02, 2009)

The TLA+ Hyperbook

This is a hypertext book that is now being written by Leslie Lamport. It will eventually describe the TLA+ and PlusCal languages and how to use the tools with the Toolbox. Only the very beginning has been written, but that beginning provides a very gentle introduction to TLA+ that also shows you how to start using the tools with the Toolbox.