Simpler constrained refinement algorithm

[GoogleCodeExporter]

Simplify the constrained refinement algorithm.  Traverse the violation subpath 
in reverse, and for each partition, ask:

1. Does this partition contain a stitch?
2a. (for upper-bound invariants) Is the running time of the FSM here* within 
(below) the time bound?
2b. (for lower-bound invariants) Does some concrete trace from here to the end 
of the violation have a large enough time** to be within (above) the time bound?

If the answer to both questions (1 and 2a for upper-bound invariants or 1 and 
2b for lower-bound) is yes, splitting here makes progress***.

* i.e., time after taking all max timed transitions from the violation start to 
here
** when added to the time from the violation start to here
*** i.e., breaks at least one combination of concrete paths that forms a 
counter-example to this invariant

Original issue reported on code.google.com by tonyohm...@gmail.com on 12 Sep 2013 at 9:53

[GoogleCodeExporter]

Simplifying further, make a candidate split at *every* stitched partition, 
ignoring 2a and 2b above.

Original comment by tonyohm...@gmail.com on 17 Sep 2013 at 7:28

[GoogleCodeExporter]

Solution in revision e3c17fb2e2ba, please review.

Original comment by tonyohm...@gmail.com on 18 Sep 2013 at 4:41

[GoogleCodeExporter]

Merged into default with revision 81abfeb34faf

Original comment by tonyohm...@gmail.com on 1 Oct 2013 at 4:00

• Changed state: Fixed