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 statebased 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.

