[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Reverse search of the state space


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.


On 15 Oct 2018, at 03:15, Matt Jennings <jen...@xxxxxxxxx> wrote:

My spec is composed of many variables and I'm not able to check it due to due to what I assume is state space explosion.   I'm wondering if for certain kinds of specs, it would be better for the model checker to start by assuming a particular invariant is violated, and work backwards looking for a path that leads back to the initial state.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.