Add local model checking

Add the ability to model check only a subgraph between a starting partition and 
an ending partition rather than the entire partition graph. This will be used 
during constrained refinement to choose better splits by finding 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.

Bisimulation.splitSatisfiesInvariantLocally(...) needs to be implemented as 
well.

Original issue reported on code.google.com by tonyohm...@gmail.com on 22 Aug 2013 at 11:39

Merged into: #340

chubbymaggie / synoptic

Add local model checking #333