Advanced Topics

Leslie Lamport

Last modified on 4 January 2019

You'll miss a lot on this web site unless you enable Javascript in your browser.

Introduction       [show]

This page is a work in progress.  It assumes you are familiar enough with TLA+ to be able to understand a simple TLA+ spec (not just a PlusCal spec).  Eventually, it will link to web pages explaining topics that go beyond what most engineers need to know about TLA+.  These topics may be useful to engineers who want to push the boundary of what they can do with TLA+, and they will be of interest to those who want a deeper understanding of the principles underlying TLA+.  Because there is not yet any standard way of properly formatting mathematics in html, all TLA+ statements and mathematical formulas are written in the ascii notation of TLA+.

Stuttering Steps       [show]

It seems obvious to me that in any sensible definition of implementation, a clock that displays hours, minutes, and seconds should implement the specification of a clock that displays hours and minutes.  I realized in 1983 that the simplest way to ensure that this is true is to require that all specifications allow stuttering steps—steps in which the state of the system does not change.  Steps of an hour/minute/second clock in which only the seconds change implement stuttering steps of the hour/minute clock's specification.  In the decades since then, I have continued to explain this to people.  To my knowledge, no state-based specification formalism other than TLA has adopted the idea.  I suspect that even many TLA+ users think it's weird to require that specifications allow stuttering steps.  Here is a link to a short note explaining why not requiring it is weird: [a link].

Liveness and Fairness       [show]

Not yet written.

Proving Safety Properties       [show]

Not yet written.

Hidden Variables and Refinement Mappings       [show]

Not yet written.