Unsupported TLA+ features

• Recursive operator definitions are not supported. Recursive function definitions are handled correctly.
• None of the back-end provers support reasoning about real numbers.
• Quantification over tuples and set constructors using tuples are not supported
  (for example {<<x, y>> \in S \X T : ...}). Note that this produces a really obscure error message, or sometimes a silent crash of TLAPS.
• ENABLED, \cdot (action composition), and many temporal operators are unsupported.
• The Zenon and Isabelle back-ends do not know the definition of the .. operator, but you can reason about it with SMT solvers. In general, proof obligations involving arithmetic can usually only be proved by the SMT backend.
• TLAPS has no built-in knowledge of (most of) the operators defined in the TLC standard module, and it cannot use their definitions either.

Poorly Supported TLA+ Features

While the following features are supported, the back-end provers do not provide much automatic proving and require a lot of guidance.

• The CASE construct, strings, tuples, and records. For records, the provers usually need to be told explicitly to use a fact of the form r.f = e even when they are given the fact r = [f |-> e, ...].
• To reason about an expression e of the form CHOOSE x : P(x), you will have to explicitly state P(e) and prove it (by proving \E x : P(x)).
• When doing arithmetic, the back-end provers cannot do any reasoning that involves the division, modulus, or exponentiation operators.

Known Limitations and Problems

The following limitations and problems of TLAPS and its backends are known to us and will hopefully be removed in a future version. We welcome your feedback on problems that you encounter. Why not subscribe to the Google TLA+ group where such issues are discussed?

• The SMT backend may fail to prove obligations involving several CHOOSE expressions. In particular, the axioms for determinacy of CHOOSE stating
  (\A x : P(x) <=> Q(x)) => (CHOOSE x : P(x)) = (CHOOSE x : Q(x))
  may not be available to the SMT solver.
• Expressions inside a proof obligation of the form
  ASSUME ..., NEW P(_), ... PROVE ...
  where P is an operator with one or more arguments are only supported by the Isabelle backend.
• We have reports of tlapm crashing with a stack backtrace that starts with
  Unix.Unix_error(3, "select", "")
  If you see such a crash, please report it, with as much detail as possible and the whole contents of the .tlaps directory.
• In an ASSUME, tlapm accepts NEW STATE, NEW VARIABLE, NEW ACTION, and NEW TEMPORAL declarations but does not handle them correctly.
• Parameterized instantiations of theorems are not handled correctly.
• Subexpression references are not handled correctly when referencing a subexpression of an ASSUME ... PROVE.