Specifying Systems

Last modified 4 March 2002

This page contains the 4 March 2002 draft version of a book about specifying systems with TLA+ and accompanying materials, all available for downloading.   Please address all comments and suggestions to   lamport  at  pa.dec.com .

The Book

The book is 365 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

The List of Corrections

This is a list of all known errors and omissions in previous versions of the draft.   If you are the first to report an error, you will be acknowledged in the published version.

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.   I hope that readers will provide additional exercises.   I would also like to include example specifications written by others.   Now, the only other example is the Wildfire challenge problem.   The specification of the Alpha memory that it contains will be of particular interest to readers of the memory specifications in Chapter 11.   Please contact me if you have any suggestions.

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 Unix users.

Downloading

The Book
You may download this book and print one copy for your own use only.   You may not make additional copies or send the electronic version to anyone else without the express permission of the author.
Postscript     Gzipped Postscript     PDF

The List of Corrections
Postscript     Gzipped Postscript     PDF

The Supporting Material
Windows Zip File     Unix  Gzipped Tar File