| Hello, some model checkers indeed work backwards from states violating the invariant, but in principle there is no reason to expect that this would lead to finding counter-examples faster. For TLA+ in particular (and even for the fragment accepted by TLC), computing predecessor states seems much harder than computing successor states, i.e. exploring the state space starting from the initial states. Stephan
|