| Hello Evgeniy, symbolic model checking is not easy to implement for an expressive language such as TLA+. For example, some form of type inference is necessary in order to know how to symbolically represent the value of a variable. The explicit construction of successor states by interpreting the next-state relation is much easier to implement. Moreover, it is not a given that symbolic model checking is always superior to explicit-state model checking. For example, asynchronous systems whose processes communicate via FIFO channels tend to give rise to state spaces for which no good symbolic representation is known. However, a symbolic model checker for TLA+ is being built [1], and we hope that it will become a useful complement to TLC. You may also want to experiment with ProB that supports a subset of TLA+ [2] and contains implementations of symbolic model checking algorithms [3]. Best regards, Stephan
|