Nice! But, there are two model checkers available for TLA+: TLC, which is an explicit-state model checker, and Apalache [1], which is a symbolic bounded model checker that uses SMT solvers, like Z3 (and infers types). There's no need to translate TLA+ to Python, therefore, to use Z3 as a TLA+ model checker.
Still, Apalache is essentially a bounded model checker (with support for inductive invariants), so it would be nice if someone managed to use Z3 to verify more complex properties.
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.
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.
> 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)
> 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.
Thanks! If there is an utility to this post other than just as an exercise in using Z3Py, it isn't just getting TLA+ into Z3 which as you say is already covered by the apalache project.
I think that as someone who doesn't really know TLA+, but is very familiar with python, it feels very comforting to being using python instead of something totally foreign. Also since it is such a small translation (really the 10 lines always combinator is the core of it), if you want/need access to the logical guts of the checker, it's easy. Or if you wanted to autogenerate a spec in some manner, being embedded in python is a huge boon.
TBH, this is a point I struggle with. TLA+ is different from programming languages because TLA+ is a language for writing mathematics [1] and mathematics is different from programming. Internalising that -- and learning how to describe things with mathematics -- is the challenge, not learning new syntax. In fact, I think that anything that makes simple mathematics look superficially similar to programming makes learning TLA+ more difficult, not less. But either way, once you've learned how to use mathematics to describe systems, wouldn't you rather use syntax that's as close to standard mathematical notation as possible? If physicists and engineers use standard mathematical notation to write mathematics even when describing the behaviour of some, say, spring system, why would programmers want to use a special notation when writing mathematics?
Don't get me wrong -- I think it's cool to show how to express TLA+ with Z3's Python API, perhaps it even helps some people understand what TLA+ formulas mean, but I disagree that it makes using TLA easier. I realise this is a matter of pedagogy, and preference might be individual, but that's my point of view.
P.S.
This is beside the point, but I've been programming for ~30 years, and while I've programmed professionally in quite a few languages (more than ten), I don't know Python (or JavaScript; at least not well). Neither do most programmers I work with. There's no doubt Python is among the best known programming languages, and millions of programmers know it, but many more than you might expect don't (just as I was surprised to realise there are programmers who don't know C or Java)! IMO, TLA+ is easier to learn, at least as far as syntax and core modules go, than any programming language.
I'm on board for there being a problem with conflating programming languages with things that are not. This was a revelation for me for example with Verilog, which almost has the trappings of an ordinary programming language but is not. It is better conceived of as a DSL for digital circuit diagrams. And I do not think of TLA+ as a programming language. I really used python here as a scripting metalanguage for constructing "TLA+" terms and orchestrating calling the checker, which to my knowledge does not have an analog in the standard TLA+ toolset. In fact one might use python for such a task, writing TLA+ and config files and shelling out to the checker.
It is however usually the case that I find myself annoyed when someone hands me a sandboxed DSL with its own syntax. Most DSLs do not get enough developer resources to become extremely feature complete. Embedding the DSL makes it much easier to extend the capabilities in ways the designer didn't imagine.
When doing things by hand scientists and engineers use ordinary mathematical notation, but when doing scientific computation they use programming languages.
I myself have a physics background and was strongly paper and pencil oriented for years and am now much heavier in the programming side of things. There are insights to be had from both perspectives. The programming/simulation side of a scientific theory is nearly necessary for me to be convinced you're not talking total nonsense. Without a calculating angle, a declarative syntax has little teeth. The precision required by programming makes it difficult to dream and sketch though. Things have to be half built before they're built.
9 comments
[ 0.25 ms ] story [ 35.0 ms ] thread[1]: https://github.com/informalsystems/apalache
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/
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/
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.
I think that as someone who doesn't really know TLA+, but is very familiar with python, it feels very comforting to being using python instead of something totally foreign. Also since it is such a small translation (really the 10 lines always combinator is the core of it), if you want/need access to the logical guts of the checker, it's easy. Or if you wanted to autogenerate a spec in some manner, being embedded in python is a huge boon.
Don't get me wrong -- I think it's cool to show how to express TLA+ with Z3's Python API, perhaps it even helps some people understand what TLA+ formulas mean, but I disagree that it makes using TLA easier. I realise this is a matter of pedagogy, and preference might be individual, but that's my point of view.
P.S.
This is beside the point, but I've been programming for ~30 years, and while I've programmed professionally in quite a few languages (more than ten), I don't know Python (or JavaScript; at least not well). Neither do most programmers I work with. There's no doubt Python is among the best known programming languages, and millions of programmers know it, but many more than you might expect don't (just as I was surprised to realise there are programmers who don't know C or Java)! IMO, TLA+ is easier to learn, at least as far as syntax and core modules go, than any programming language.
[1]: https://old.reddit.com/r/tlaplus/comments/enencr/yet_another...
It is however usually the case that I find myself annoyed when someone hands me a sandboxed DSL with its own syntax. Most DSLs do not get enough developer resources to become extremely feature complete. Embedding the DSL makes it much easier to extend the capabilities in ways the designer didn't imagine.
When doing things by hand scientists and engineers use ordinary mathematical notation, but when doing scientific computation they use programming languages. I myself have a physics background and was strongly paper and pencil oriented for years and am now much heavier in the programming side of things. There are insights to be had from both perspectives. The programming/simulation side of a scientific theory is nearly necessary for me to be convinced you're not talking total nonsense. Without a calculating angle, a declarative syntax has little teeth. The precision required by programming makes it difficult to dream and sketch though. Things have to be half built before they're built.