Advanced Topics

This page assumes you are familiar enough with TLA+ to be able to understand a simple TLA+ spec (not just a PlusCal spec).  It contains links to documents 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+. 

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].  I don't understand why many people write such weird specs.

The terms safety, liveness, and fairness are used informally throughout the TLA+ documentation—including in the TLA+ Video Course.  They are defined precisely in this note, which also describes their significance.  Although it requires little knowledge of TLA+, you might find the note to be tough going if you're not used to reading mathematics.  But it's worth the effort if you want a more complete understanding of TLA+.

I have been writing correctness proofs of concurrent algorithms for about 45 years.  I developed what I find to be a natural way of writing these proofs.  However, writing rigorous proofs has remained a black art that few people have mastered.  Learning to write these proofs starts with learning to write proofs of safety properties.  I believe that TLA+ and its tools can help you learn to write these proofs.  The document Proving Safety Properties shows you how.  It explains the art of writing rigorous proofs, but not completely formal machine-checked proofs.  Writing machine-checked proofs requires a lot of additional effort, as well as practice using the TLAPS proof system.

I started thinking about writing specifications around 1980.  I quickly realized that it was important to understand what it meant for a program to satisfy a spec.  I knew that, in principle, a spec and an executable program are both specifications of a physical system, written at two different levels of abstractions.  So, I needed to understand what it meant for one specification to implement or refine another.  This ultimately led me to TLA, the temporal logic underlying the TLA+ language, and to using the temporal existential quantification operator (written \EE in TLA+) to write specifications.  This operator served to distinguish variables that represent externally observable parts of the system from ones that represent unobservable parts that need not appear in an implementation.  Temporal existential quantification hid those unobservable variabled.

With the development of the TLA+ tools and seeing how TLA+ is used in practice, I came to realize that engineers and computer scientists didn't need the \EE operator.  So, I generally don't talk about it; and I explain refinement without it.  For example, \EE is not mentioned in the TLA+ Video Course. 

While engineers don't need to use variable hiding and the \EE operator, knowing why I used them to write specs provides a deeper understanding of refinement and auxiliary variables.  So, I have explained this background in the note Hiding, Refinement, and Auxiliary Variables.  You should read it before attempting to read the complete guide to auxiliary variables in the paper Auxiliary Variables in TLA+.