Resources

This page lists several resources to improve your understanding of PlusCal and TLA+.

PlusCal and TLA documentation

The official documentation is available on the computers at ENSEIRB-MATMECA under the directory ~herbrete/public/TLA. It consists in two files.

• c-manual.pdf is a short introduction to the PlusCal language, up to formal verification.
• pluscal.pdf gives a mor edetailed overview of the PlusCal language, with several modeling examples.

A cheatsheet on PlusCal syntax is available from the pluscal.help website.

Leslie Lamport’s introduction to formal verification

• If you are not writing a program, don’t use a programming language by Leslie Lamport

Hillel Wayne’s Learn TLA+

• A very good set of documents to Learn TLA+

Ron Pressler’s blog (advanced)

• Why writing correct software is hard
• Part 1: The principles of TLA+
• Part 2: The + in TLA+
• Part 3: The (temporal) logic of actions
• Part 4: Order in TLA+