What resources exist documenting the finer points of TLA+ language interpretation?

[Andrew Helwer]

For example, how would I answer questions like:

• When defining macros, do we allow a space like macroname (arg1, arg2) == ...
  
• How exactly does evaluation of conjuncts/disjuncts with different indentation work
• etc.

Please note I am not asking these specific questions (because there are many more than that and I don't want to bore you); I'm asking what resources exist that would enable me to know the answer to such questions. So far I've found:

• The Operators of TLA+ [Lamport, 1997]
• Specifying Systems
• Trying & seeing what SANY accepts

Is there... a TLA+ spec of TLA+? :)

Andrew

[Leslie Lamport]

First of all, it's important not to confuse TLA+ with TLC.  For example, your second question mentions "evaluation".  TLA+ is math, and there's no concept of evaluation in math.  Evaluation is a programming concept.  TLC is a program, and I presume that question is about TLC.

The original TLA+ language is quite precisely specified.  "Specifying Systems" contains what I believe is an unambiguous informal mathematical specification of TLA+ syntax and semantics.  (Part of the syntax specification is written in TLA+.)  See the TLA+ Version2 Web Page for a link to a fairly precise specification of the language features added in around 2006.  One thing not precisely specified there is the semantics of recursive operator definitions.  They are explained in a paper by Georges Gonthier and me that you don't want to read.

TLC is not well specified.  (Programs seldom are.)  Almost all the questions people have about how TLC works are answered by a careful reading of Chapter 14 of "Specifying Systems".  I believe that few TLC users have even looked at it, let alone tried reading it carefully.  It is not easy reading, and even I am sometimes surprised by things that TLC does.  For example, look at these two actions for a spec with a single variable x :

    /\ p(x) \/ q(x)      /\ ~p(x) => q(x)

    /\ x' = r(x)         /\ x' = r(x)

These two are equivalent mathematical formulas, but TLC evaluates them differently, which can lead to different results.  (In particular, one can produce an error when the other doesn't.)  It takes a very careful reading of that chapter to understand why.  

The basic correctness condition that TLC is supposed to maintain is that, if a model tells it to check properties of the spec, and TLC finishes executing the model and finds no error, then there is an interpretation of the TLA+ semantics for which the specification satisfies those properties.  An interpretation of the TLA+ semantics is a specification of things that the semantics leaves unspecified, such as the value of CHOOSE x \in {1,2,3} : TRUE.  The model can specify things--including the values of constants, a state constraint, and overriding of definitions--that modify the specification for which this correctness condition should hold.  I believe the existing documentation (mainly "Specifying Systems" and the Toolbox help pages) does a reasonable job of explaining what those modifications are.  I don't remember if there are TLC bugs that cause it not to satisfy this correctness condition in some cases; if there are, they will be reported in the Github repository.

There are many TLC features that don't affect this basic correctness condition, such as what it does when evaluating the Print operator, or how much memory it uses.  These features are often not well documented.  We welcome the community's help in identifying where documentation is needed and in providing documentation.

Leslie