search

mgijsberti / synoptic

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

Add AFbyUpper invariant #335

Closed GoogleCodeExporter closed 9 years ago

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

Of the 3 remaining constrained invariants to be implemented, this will be 
easiest (and should probably be done first).  This should involve no changes or 
fixes to constrained refinement or to the super class ConstrainedTracingSet.  
Simply copy APUpperTracingSet, primarily modifying transition(...) to conform 
to the AFbyUpper FSM.

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 
Solution in revision 465848046834, please review.

Original comment by tonyohm...@gmail.com on 29 Aug 2013 at 10:52

GoogleCodeExporter commented 9 years ago 
Merged into default with revision dcba6587c52d

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