search

mgijsberti / synoptic

Automatically exported from code.google.com/p/synoptic
0 stars 0 forks source link

NFby invariants are ignored by pynoptic #343

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Pynoptic's ConstrainedInvMiner creates one upper- and one lower-bound version 
of each AFby and AP invariant, but it simply tosses any NFby invariants rather 
than retaining them as unconstrained invariants.  This only requires changing a 
few lines near the end of 
ConstrainedInvMiner.computeInvariants(ChainsTraceGraph,boolean,TemporalInvariant
Set).

However, testing will be required to ensure that there are no bugs in model 
checking, refinement, or coarsening when the TemporalInvariantSet contains both 
unconstrained and constrained invariants.

Original issue reported on code.google.com by tonyohm...@gmail.com on 1 Oct 2013 at 9:56

GoogleCodeExporter commented 9 years ago

Original comment by tonyohm...@gmail.com on 16 Oct 2013 at 12:29

GoogleCodeExporter commented 9 years ago

Original comment by tonyohm...@gmail.com on 16 Oct 2013 at 1:47

GoogleCodeExporter commented 9 years ago 
Solution in revision 1986:222d08d4ac57, please review.

Original comment by sebastia...@gmail.com on 29 Oct 2013 at 7:55

GoogleCodeExporter commented 9 years ago 
Merged into default with revision d57cd63445c3.

Original comment by tonyohm...@gmail.com on 6 Nov 2013 at 5:45