Examples
This page contains a list examples of TLA+ specifications and PlusCal algorithms.
A zip file containing a collection of examples that will be part of the TLA+ tools distribution is temporarily available here. (It also includes the examples from the TLA+ book.) Each directory contains a README file that describes the examples in the directory.
Other Examples
Wildfire challenge problem
This example comes closest to a realistic industrial system specification of any of the examples described on this page. The specification of the Alpha memory that it contains will be of particular interest to readers of the memory specifications in Chapter 11 of the book.
Checking a Multithreaded Algorithm with +CAL
This paper describes a realistic (though not real) example of how PlusCal can be used to find bugs in interesting algorithms. There is a link to the specification used and the error trace that it produced.
