Dynoptic hangs during refinement

What steps will reproduce the problem?

Run dynoptic from the command line using the attached files, e.g.  
`./dynoptic.sh -c args_short.in simple_short.trace`

What is the expected output? What do you see instead?

A completed model. See log.txt (attached) for the output of the above command.

What version of the product are you using? On what operating system?

I am using OSX 10.7 with Synoptic downloaded and built from source on April 16, 
2013.

Please provide any additional information below.

As you can see in 'args_short.in', I am using one of the McScM binaries 
included in the repository.

Original issue reported on code.google.com by rjwall...@gmail.com on 18 Apr 2013 at 8:18

Attachments:

I'm closing the issue as I think it's been resolved. Feel free to re-open or
create new issues if you run into any further problems.

thanks!
ivan.

>>>>>>>>>>>>>>>>>>>>>>> details:

I was able to reproduce your problem locally. The project pages aren't
particular clear on this, but here are some key properties of how
Dynoptic works that explain what's happening:

1. Dynoptic relies on an external tool, called McScM, which is a model
checker for CFSM models. Because checking a CFSM with unbounded queue
length is an undecidable problem McScM is not guaranteed to terminate.
So, it may run indefinitely.

2. To make sure that Dynoptic always terminates I've added a
timeout/retry mechanism. Dynoptic checks an invariant until a base
timeout threshold is reached (current code uses 40min!). If McScM
times out, Dynoptic moves on to checking the following invariant. If
McScM times out on all invariants, then Dynoptic increments the
timeout (by 1min) and rechecks the invariants. It does this until some
max threshold is reached (1 hour), at which point Dynoptic gives up.
(If you are feeling adventurous, the timing out logic is in
DynopticMain.checkInvsRefineGFSM).

3. McScM is fast on some simple examples, but slow on almost
everything interesting. Thus the high timeout values above.

So, the underlying cause of your original problem was that the timeout
values were too high. If you run things with lower thresholds then
Dynoptic times out on the offending invariant quicker and then makes
progress and completes okay.

The timeout variables mentioned above were hardcoded in the code. But,
I've exposed them in the latest commit (revision 56d50baa23ac). If you
run ./dynoptic -h, you'll see three new verification options (note the
lower defaults -- these should work fine for your example):

--baseTimeout=<int>                   - Initial timeout (in seconds)
  that is used to time out McScM verification. [default 20]

--timeoutDelta=<int>                  - Time (in seconds) to add to
  -base-timeout after each time McScM times out, before reaching max
  timeout. [default 10]

--maxTimeout=<int>                    - Maximum timeout (in seconds)
  to use for McScM verification. [default 60]

Original comment by bestchai on 19 Apr 2013 at 6:30

Changed state: Fixed

chubbymaggie / synoptic

Dynoptic hangs during refinement #304