Modeling TLA+ in Z3Py

There are several issues regarding liveness:

1. Afaik, NuSMV implements the standard propositional encoding of lasso detection with SAT [1], which should also work SMT (when we can guarantee that the transition system is finite). While I am sure this is the case for NuSMV, it is a bit of guessing in case of nuXmv as it is available in binaries, and its default license prohibits industrial use. Although the encoding [1] is linear in the formula size, it is still producing a lot of constraints. Unfortunately, practical TLA+ specifications are very heavy on fairness constraints (WF and SF), which are actually expressed as formulas over []<>p and <>[]q. So we first have to make Apalache scale to bounded model checking of safety, before trying it in a much harder setting.

2. Apalache also supports integer constants (under some syntactic assumptions), e.g., one can write \E x \in Int: P. While this makes Apalache quite useful in reasoning about timestamps, such specifications are infinite-state. That requires generalized liveness-to-safety reductions, such as the one implemented in Ivy.

3. Finally, distributed systems quite often require non-standard liveness. For instance, it is often the case that messages should be delivered within a predefined time interval. While we can model these systems by writing LTL formulas, this usually leads to huge LTL formulas, so see point 1. Moreover, some distributed systems have only probabilistic liveness guarantees. In this setting, the benefit of LTL is less obvious than the benefit of safety checking. It may be easier and more efficient to write a liveness monitor by hand, rather than rely on an automatically generated one, which will for sure explode.

[1] Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan: Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. 2(5) (2006)

This is interesting, because undecidability of SMT theories is a very practical issue. Actually, many people in academia have this point of view that solving many practical problems is useful. It helps us to drive research progress, but it is a completely useless metric for industry. What is better: (1) a tool that wins a competition by solving X out of Y benchmarks, (2) or a tool that solves your problem? In academia, (1) is a clear winner, as it gives you a free way to publish a paper, modulo peer review. In industry, you don't care about (1), because you have exactly 1 (one!) benchmark that is important for you, that is, case (2).

Imagine a compiler that works on 85% of syntactically-correct (and well-typed) programs, and you never know when it would hang on your code. This is exactly the behavior of SMT solvers when you start using quantifiers. By knowing the internals of SMT and its techniques, you can quite often work around these problems. However, TLA+ users do not want to know the guts of SMT; why would they? This is why Apalache implements a quantifier-free encoding. Sometimes, it hits us badly, but it is somewhat more predictable. Ivy does it differently, by providing the user with a language that is actually quite close to the theories implemented in z3. While it gives the user a finer control over the SMT constraints, the user has to understand first-order logic much better than in case of Apalache.