A High-Level View of TLA+

Summary

A High-Level View of TLA+ Leslie Lamport Last modified on 10 August 2021 You'll miss a lot on this web site unless you enable Javascript in your browser. Introduction [show] TLA+ is a language for modeling software above the code level and hardware above the circuit level. It has an IDE (Integrated Development Environment) for writing models and running tools to check them. The tool most commonly used by engineers is the TLC model checker, but there is also a proof checker. TLA+ is based on mathematics and does not resemble any programming language. Most engineers will find PlusCal, described below, to be the easiest way to start using TLA+. TLA+ models are usually called specifications. They are called in this introduction. PlusCal is a language for writing algorithms—especially concurrent and distributed ones. It is meant to replace pseudocode with precise, testable code. PlusCal looks like a simple toy programming language, but with constructs for describing concurrency and nondeterminacy. It is infinitely more expressive than any programming language because any mathematical formula can be used as a PlusCal expression. A PlusCal algorithm is translated into a TLA+ model that can be checked with the TLA+ tools. Because it looks like a programming language, most engineers find PlusCal easier to learn than TLA+. But because it looks like a programming language, PlusCal cannot structure complex models as well as TLA+ can. Click here for an example of an algorithm written in PlusCal. Models [show] Computers and computer networks are physical objects whose behaviors are described by continuous physical laws. They differ from most other kinds of physical objects in that their behaviors are naturally modeled as sets of discrete events. Programming, software engineering, and most of computer science is concerned with models in which a behavior of a system is described as a set of discrete events. No model is a completely accurate description of a real system. A model is ...