[igornotarobot]

> Other examples would be checking liveness properties in the unbounded case, and possibly full Linear Temporal Logic, e.g., <>[]p ("eventually, property p is always satisfied"). I realize this is a tall order, but I think nuXmv [1] already implements some kind of SMT-based LTL model checking, so it should be possible to achieve something similar for TLA+ (or at least a subset).

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)