Stop verification when each partitions is a singleton

chubbymaggie / synoptic

Automatically exported from code.google.com/p/synoptic

0 stars 0 forks source link

Stop verification when each partitions is a singleton #265

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago

A simple performance shortcut for short traces is to break out of the 
check/refine loop when each partition contains a single observed fifo state. In 
this case, all of the invariants must be true of the corresponding CFSM model, 
so we can skip the model checking and return this final model.

Original issue reported on code.google.com by bestchai on 26 Sep 2012 at 7:59

GoogleCodeExporter commented 9 years ago

I'll handle this one.

Original comment by bobyan...@gmail.com on 12 May 2014 at 11:03

Changed state: Accepted

GoogleCodeExporter commented 9 years ago

Solution in revision 6108281fb0af, please review.

Changes are found in:
CSightMain.checkInvsRefineGFSM()
GFSM.isSingleton()
GFSMState.isSingleton()

Tests are:
CSightMainTests.testCheckInvsRefineGFSMWithNonSingleton()
CSightMainTests.testCheckInvsRefineGFSMWithSingletonPartition()
GFSMTests.testIsSingleton()

Original comment by bobyan...@gmail.com on 21 May 2014 at 8:28

Changed state: Started
Added labels: Type-Review
Removed labels: Type-Enhancement

GoogleCodeExporter commented 9 years ago

Correction:
There was an error in the previous revision.

Please check revision d2a1baace72e instead.

Original comment by bobyan...@gmail.com on 26 May 2014 at 10:35

GoogleCodeExporter commented 9 years ago

This issue was closed by revision efab50e6ba80.

Original comment by bestchai on 28 May 2014 at 5:01

Changed state: Fixed

GoogleCodeExporter commented 9 years ago

Merged into default with revision 52813ea54d96

Original comment by bestchai on 28 May 2014 at 5:02