Remove unconstrained model checking from Perfume

[GoogleCodeExporter]

In Perfume, refinement for one constrained invariant (e.g., A AFby B <= 2.0) 
approximately involves the following steps:

1. Model check for A AFby B (unconstrained). Violation? Note it and go to #3.
2. Model check for A AFby B <= 2.0 (constrained). Violation? Note it.
3. Possibly split if there's a violation.

Investigate whether #1 is necessary at all, since we believe #2 probably does 
(or at least should) subsume the logic in #1. If #1 can indeed be eliminated, 
it will immediately increase performance somewhat but will have especially 
important benefits for adding multi-resource support to Perfume.

Original issue reported on code.google.com by tonyohm...@gmail.com on 13 Jan 2015 at 6:39

[GoogleCodeExporter]

The above description is partially correct. Actually, unconstrained model 
checking is only used in Perfume when deciding *where* to split after a 
violation has already been detected. Only constrained model checking is used to 
find the violations.

For that reason, Perfume already relies on constrained model checking subsuming 
unconstrained model checking (for the same base invariant). We have decided to 
remove unconstrained model checking from Perfume entirely, which won't violate 
correctness (or at least won't introduce any *new* bugs).

Original comment by tonyohm...@gmail.com on 14 Jan 2015 at 8:19

• Changed title: Remove unconstrained model checking from Perfume
• Added labels: Type-Enhancement
• Removed labels: Type-Task

[GoogleCodeExporter]

Fixed in revision 9737b0ad1b2e.

Original comment by tonyohm...@gmail.com on 14 Jan 2015 at 8:53

• Changed state: Fixed