[FEATURE] Implement precise deadlock detection

[konnov]

Following the bug reports #711 and #110, we should implement precise deadlock detection.

We should implement an additional deadlock detection mode that encodes the following query: Is there a state, in which all transitions are disabled. The current version implements a simpler query: Is there k such that all transitions are disabled in all states that are produced by k steps.

The more precise version requires us to deal with ENABLED, see #800. This is not a trivial extension.

[danwt]

I was wondering, if a state S_E is found with no out-edges then is there an easy way to check if the state is reachable from S_0 (assuming it's not k reachable)?

I can't think of one and would be interested to know. My naive idea is to bfs in parallel from both S_0 and S_E and check if the reachable sets ever overlap. But this is still ultimately bounded by some k.

[konnov]

I was wondering, if a state S_E is found with no out-edges then is there an easy way to check if the state is reachable from S_0 (assuming it's not k reachable)?

I can't think of one and would be interested to know. My naive idea is to bfs in parallel from both S_0 and S_E and check if the reachable sets ever overlap. But this is still ultimately bounded by some k.

Are you considering explicit-state model checking (TLC) or bounded model checking (Apalache)? In the explicit-state world, it's all easy: Just run BFS as you are saying. When we are using a solver (SAT or SMT), we have to somehow summarize sets of states. There are algorithms for doing that like IC3 or PDR, but we don't know yet how to apply them in the context of TLA+.