search

chubbymaggie / synoptic

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

Add AFbyLower invariant #337

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Implement AFbyLower in model checking and refinement.

This will almost certainly require some (hopefully minor) fixes/refactoring in 
the super class ConstrainedTracingSet. Also copy APUpperTracingSet, and modify 
transition(...) to conform to the AFbyLower FSM.  Furthermore, the constrained 
refinement process in Bisimulation will need to be finished for lower-bound 
invariants, as some parts were only completed for upper-bound invariants so far.

Also remember to add new tests in ConstrainedTracingSetTests, and find 
conditionals beneath TODOs in Bisimulation, ConstrainedTracingSet, or 
FsmModelChecker which need to be modified as new constrained tracing sets are 
implemented.

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

GoogleCodeExporter commented 9 years ago

Original comment by tonyohm...@gmail.com on 11 Sep 2013 at 8:34

GoogleCodeExporter commented 9 years ago 
Solution in revision 76c9a28b189d, please review.

Original comment by tonyohm...@gmail.com on 12 Sep 2013 at 9:56

GoogleCodeExporter commented 9 years ago 
Merged into default with revision 3587bf7d39a3

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