On Prism (or the SEL-VM) invoke tla from the command line. You can also install the TLA+ Toolbox/IDE on your Laptop.

youtube playlist of Introductory Videos for analyzing TLA+ Specifications and checking them for specification error using the TLC modelchecker.

TLA+ Summary

TLA stands for the Temporal Logic of Actions. TLA+ is the TLA specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems.

PlusCal is an algorithm language that, at first glance, looks like a typical tiny toy programming language. However, a PlusCal expression can be any TLA+ expression, which means anything that can be expressed with mathematics. This makes PlusCal much more expressive than any (real or toy) programming language. A PlusCal algorithm is translated into a TLA+ specification, to which the TLA+ tools can be applied.

The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+ proof system. All the tools are normally used from the Toolbox, an IDE (integrated development environment). Go to the TLA home page to find out more about TLA.

TLC is a so-called “explicit-state” model checker that computes the state space generated by your specification and can then verify (safety and liveness) properties fully automatically. Its main constraint is state space explosion: the size of the state space grows exponentially with the number of processes etc., and this leads to a corresponding increase in verification time. There are a number of techniques to push back the frontiers of what TLC can handle effectively, including using symbolic constants, symmetry reduction etc., but the most important one is for you to decide how big you need your model to be to have enough confidence in correctness.

TLAPS is an interactive proof assistant: you provide a proof of why your system satisfies a property, and TLAPS can check if that proof is logically consistent and complete. It uses different automatic back-ends, including SMT solvers, to check proof steps, but it is still the user who designs and writes the proof. Although the effort is independent of the size of the state space, and also infinite-state systems can be verified in this way, I would not recommend using TLAPS for users who do not have sufficient experience with theorem proving.

Youtube: Simple Traffic Light. TLA+ Specification and TLC modelchecker.

Youtube: Bank System with multiple accounts. TLA+ Specification and TLC modelchecker.

• File: bank_video.tla.zip.

• See TLA+ Toolbox Details
  • Invoke as tla160& from the command line on EECS servers (or as “tla&”).
  • TLA 1.6 Release Notes
  • On EECS servers we also use tlaplus_repl60 (instructions).
• TLA Toolbox User's Guide
• Specifying Systems TLA+ Book by Leslie Lamport. PDF
• TLA Examples
• TLC from the command line

• TLA Videos. This is a series of video lectures to teach programmers and software engineers how to write their own TLA+ specifications.
  • Video Paxos Algorithm. Videos of two 1.5-hour lectures Leslie Lamport gave summer 2019 on the Paxos consensus algorithm. The algorithm is developed through a sequence of TLA+ specs. No prior knowledge of the algorithm or TLA+ is assumed. The videos constitute a crash course on TLA+. Links to the videos, the specs, and accompanying exercises are at the link.

• Current Tools.This document describes differences between the descriptions of the TLA+ tools in the book Specifying Systems and the currently released versions. References are to the version of the book currently available on the web. The book and this document do not describe the features provided by the TLA+ Toolbox for using the tools. They are described by the Toolbox’s help pages and the TLA+ Hyperbook.