Check for local violation resolution / subgraph model checking

[GoogleCodeExporter]

== Current refinement ==

Refinement generates potential splits and then tries to choose the best one.  
For the latter, it checks if the split globally resolves the invariant 
violation (e.g., there are no longer any "login AP logout <= 25" 
counter-examples in the entire graph).  If it does globally resolve, then split 
here.  Else pick one of the potential splits arbitrarily, and apply it.

== New optimization ==

We could intermediately add a check for local violation resolution.  This would 
mean model checking on a subgraph of the partition graph that only includes

(1) the two partitions that start and end the violation subpath and
(2) partitions that are both (a) somehow reachable from the start of the 
violation subpath and (b) can somehow reach the end of the violation subpath

This is an optimization that can help choose better splits, although its actual 
effectiveness on real data is unknown at this point.  The only required change 
for constrained refinement would be implementing the currently-empty 
Bisimulation.splitSatisfiesInvariantLocally(...) method.  Other small changes 
in Bisimulation would be needed for unconstrained refinement.

Original issue reported on code.google.com by tonyohm...@gmail.com on 10 Sep 2013 at 7:25

[GoogleCodeExporter]

More info from duplicate Issue 333:

This will be used during constrained refinement to choose better splits: after 
determining that a split that globally satisfies the invariant does not exist, 
we will now search for splits that satisfy the invariant locally in this 
subgraph.

This will require a local version of FsmModelChecker.getCounterExample(...) and 
FsmModelChecker.runChecker(...) which will be very similar to their existing 
counterparts, almost certainly meaning a refactoring will be necessary.  The 
only difference will be that ConstrainedTracingSet.setInitial(...) will be 
called on the starting partition rather than the initial node, and model 
checking needs to stop after reaching the ending partition rather than the 
terminal node.

Original comment by tonyohm...@gmail.com on 1 Oct 2013 at 9:43

[GoogleCodeExporter]

Issue 333 has been merged into this issue.

Original comment by tonyohm...@gmail.com on 1 Oct 2013 at 9:44