[igornotarobot]

Just curious, what more complex properties do you like to be supported in Apalache? Many tools that are built on top of z3 are checking inductive invariants. By having a strong enough inductive invariant, you should be able to check safety.

If you like to check your specification for arbitrary parameters, then you will have to use quantifiers in z3, which would require a lot of care to write SMT constraints in a way that helps z3 to deal with the quantifiers. The mix of sets and cardinalities is especially hard for SMT. Although academia is making a lot of progress in this direction, e.g., see [1], the mainstream solvers are still leaving you with the problem of encoding sets and cardinalities all by yourself.

Some provers use quantifiers in z3. For instance, IVy [1] can check inductive invariants of systems that have arbitrary size. However, you have to rewrite your specification in uninterpreted first-order logic, e.g., you would have to think about abstracting away integers. Moreover, to make invariant checking decidable, you would have to transform your specification into a special fragment that is called EPR.

[1] Ruzica Piskac. Efficient Automated Reasoning About Sets and Multisets with Cardinality Constraints. VMCAI, 2020. https://link.springer.com/chapter/10.1007%2F978-3-030-51074-...

[2] http://microsoft.github.io/ivy/

[lou1306]

IVy was exactly one of the things I had in mind. 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).

> to make invariant checking decidable

Of course decidability is desirable, but efficient sound procedures in the undecidable case would still solve many practical problems. I realize they are not as "nice" from a theoretical/academic standpoint, though.

[1] https://nuxmv.fbk.eu/

[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)

[igornotarobot]

> Of course decidability is desirable, but efficient sound procedures in the undecidable case would still solve many practical problems. I realize they are not as "nice" from a theoretical/academic standpoint, though.

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.