search

chubbymaggie / synoptic

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

Handling McScM model checker timeouts #266

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
The current Dynoptic code assumes that the McScM model checker always 
completes. However, checking CFSMs is undecidable in general and McScM may 
never return. A few TODOs here:

1. Lower the current timeout of 1hour down to about 5 minutes.

2. Change the check/refine loop to be more adaptive:

(2.a) check the next invariant when there is a timeout, and when the new 
invariant causes a refinement then re-check the timed-out invariant;

(2.b) if all invariants timed out then increase the timeout value a few times 
before giving up on the entire process.

Original issue reported on code.google.com by bestchai on 26 Sep 2012 at 9:23

GoogleCodeExporter commented 9 years ago 
This issue was closed by revision eb5e83a4bbea.

Original comment by bestchai on 27 Sep 2012 at 2:12