Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Toolbox does not correctly handle TLC's -continue flag #79

Open
lemmy opened this issue Oct 4, 2017 · 1 comment

Comments

1 participant
@lemmy
Copy link
Member

commented Oct 4, 2017

The -continue flag causes TLC to keep exploring the state graph even if a counterexample is found. As a result, TLC can find N counterexamples instead of just one. This confuses the Toolbox which expects exactly one counterexample.

I do not think "-continue" is used widely enough to warrant a Toolbox fix. If the community feels strongly about it, please step up and provide a patch/pull request.

@lemmy lemmy added this to TLC Breakpoints in ldq Jan 10, 2019

@lemmy

This comment has been minimized.

Copy link
Member Author

commented Apr 9, 2019

LL: "I'm not sure what should happen if the user wants to use -continue from the Toolbox. As I recall, TLC just keeps running with that option. I don't see doing that from the Toolbox being useful. For using with the Toolbox, TLC should be stopped when an error is reported and the user allowed to then tell the Toolbox to resume running the model from where it left off. Implementing that would be difficult--especially if two different worker threads concurrently discover an error. (But that situation must be handled now, so maybe that's not a problem.) Anyway, we don't have to worry about that now."

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.