Check/refine invariants in a particular order

[GoogleCodeExporter]

Currently, Dynoptic checks/refines invariants in an arbitrary order (the order 
in which they are returned by the invariant miner).

Instead, it makes sense to order invariant checking/refinement as follows. Note 
that these are heuristics -- sometimes they will give better results, and 
sometimes not. However, I think they are better than using an arbitrary 
ordering.

1. Check "x NFby y". Since an NFby counter-example path is first refined in 
between the first x and y appearance. Therefore, it has the most limited 
refinement scope.

2. Check "x AP y". This will refine the prefix of the counter-example, up to 
the first y.

3. Check "x AFby y". This refines counter-example tails, or sections of paths 
after an x.

4. Check "Eventually x". As with AP, this too will refine the prefix, or the 
first stitching of the counter-example path. However, the refinement is 
unbounded -- refinement may occur anywhere along the path.

Original issue reported on code.google.com by bestchai on 25 Sep 2012 at 3:43

[GoogleCodeExporter]

One approach to determine the best ordering is to generate different CFSMs and 
check how well McScM performs on different invariant types. Different invariant 
types use different queue regular expressions and the complexity of these 
expressions might well be the key feature that determines model checker 
performance.

Once we find out which invariants are checked faster, we would check these 
invariants first -- since refinement leads to models with fewer behaviors and 
helps to improve the performance of checking the slower invariants.

Original comment by bestchai on 6 Oct 2012 at 10:16