Last modified on 3 December 2021
PlusCal is a language for writing algorithms—especially concurrent and distributed ones. It looks like a toy programming language with constructs for describing concurrency and nondeterminacy, but its rich expression language makes it well-suited for describing algorithms. PlusCal algorithms can be checked with the TLA+ tools, the most commonly used tool being the TLC model checker.
The PlusCal Tutorial will teach you to write and check PlusCal algorithms. It assumes only a basic knowledge of programming concepts, though PlusCal will be most useful for describing multi-threaded programs and distributed systems. Some knowledge of simple math, as taught at universities to first-year computer science students, will be helpful but is not necessary.
Tutorial Begins Here Table of Contents