search

mgijsberti / synoptic

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

Constrained model checking never leaves loops #344

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
ConstrainedTracingSets are missing isSubSet(...) implementations to prevent 
infinitely following loops, so model checking never terminates.  For now, 
implement these using the same simple strategy synoptic uses: check if the FSM 
states inhabited after transitioning to the current node are a subset of the 
states inhabited by the existing tracing set already at that node.  If so, do 
not continue exploring the path (i.e., don't follow the loop again).

Original issue reported on code.google.com by tonyohm...@gmail.com on 2 Oct 2013 at 2:19

GoogleCodeExporter commented 9 years ago 
Solution in revision 756730db62f7, please review.

Original comment by tonyohm...@gmail.com on 4 Oct 2013 at 5:15

GoogleCodeExporter commented 9 years ago 
Merged into default with revision 878aa680b4be

Original comment by tonyohm...@gmail.com on 24 Oct 2013 at 9:24