Hi Evgeniy,
Stephan already mentioned some issues. I would like to comment on our experience when developing such a symbolic model checker for TLA+ [1]. The web page is more up-to-date now.
1. There are no built-in types in TLA+. On one hand, TLC nicely avoids this issue, as it computes values dynamically and reports a type mismatch exactly when it happens. In this sense it acts as an interpreter, not a compiler. On the other hand, symbolic techniques work more like a compiler, that is, they translate a specification into a symbolic transition system: binary decision diagrams (BDDs), Boolean formulas (SAT), first-order theories (SMT), constraints over integer variables, etc. To do such a translation one needs to statically find proper types.
2. One has to find a good encoding of TLA+ expressions in the target symbolic representation. When using BDDs or SAT solvers, one has to translate all kinds of TLA+ expressions into Boolean formulas. While it is not conceptually hard for fix-width integers or tuples, it becomes tricky for sets and functions. A naive translation of the _expression_ "x \in SUBSET {1, 2, 3}" would just compute all the subsets before constructing symbolic constraints, which defeats the purpose of using symbolic techniques.
It is somewhat easier with the SMT solvers that support integers, arrays, uninterpreted functions, etc. However, one still has to find good ways to translate sets, sets of sets, sets of functions, set cardinalities, etc.
We believe that we have come up with a good SMT encoding for a large part of TLA+ expressions that can be found in the actual TLA+ code. But the tool is still far from being useful. When it is ready for any kind of testing, we will announce it on the list.
Best regards,
Igor
[1] http://forsyte.at/research/apalache/
On Wednesday, July 4, 2018 at 10:24:58 AM UTC+2, Evgeniy Shishkin wrote:
Hello researchers!
Relying on the fact that this forum is inhabited with inventors of TLA+, I would really like
to know the answer.
Thanks.