ReviseDeadlocksMRV() assertion failure

[grencez]

There is an assertion failure within the ReviseDeadlocksMRV() function that can be avoided by using the -force-rank-deadlocks flag. The revise function might be incompatible with some scenarios.

One bad scenario is when some added action is not a candidate. Another is when more deadlock states are introduced due to the invariant shrinking. Both of these are guarded against.

[grencez]

The default behavior has been changed to never call ReviseDeadlocksMRV().
To enable it, use the new -fast-deadlock-mrv flag.

A good place to investigate further is synthesizing examplespec/TokenRing.prot with M=4 and ring sizes N=2,...,7. Give -no-partial to all systems but the smallest. There assertion fails for the smallest system in check_forward(), definitely a problem with revising the deadlocks in the step right before it.

[grencez]

Changed to be an enhancement because the bug has been "fixed" by not calling that code by default. If the bug gets fixed, then the code will go faster again.

Alternatively, it may be a good idea to change PickActionMRV() to do the reranking. In this case, we can optimize for multiple systems by passing in a known cutoff MRV that a smaller system already has. This would likely be faster than reranking, so that code would be removed completely.

Also, it appears that fixing issue #2 has made the above case not reproducible... so no reproducible cases now.