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

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.

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 withUnix.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`

.