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

Solver restart from timeout in simulate mode #2316

Closed
rnbguy opened this issue Dec 8, 2022 · 1 comment
Closed

Solver restart from timeout in simulate mode #2316

rnbguy opened this issue Dec 8, 2022 · 1 comment
Assignees
Labels
feature A new feature or functionality impact-medium Incremental improvement | unblocks non-critical work | saves some time

Comments

@rnbguy
Copy link
Contributor

rnbguy commented Dec 8, 2022

Is your feature request related to a problem? Please describe

The simulate mode can get stuck slow if the solver is taking too long to solve the next transitions or to construct an example run.

I know I can set --tuning-options=search.smt.timeout=15. But this terminates the search globally - and does not try for the next example runs. It would be nice if z3 is timed out, apalache continues trying for the next runs until --max-run many runs are tried - timed out or not.

Describe the solution you'd like

For first versions, something like --tuning-options=search.smt.timeout=15:search.smt.timeout.ignore=true

Describe the impact on your work

I can set a high --max-run and a timeout for the solver to retry for new runs automatically.

Describe alternatives you've considered

On bash shell, until apalache-mc simulate --tuning-options=search.smt.timeout=15 ...; do ...; done

@rnbguy rnbguy added the feature A new feature or functionality label Dec 8, 2022
@konnov konnov added the impact-medium Incremental improvement | unblocks non-critical work | saves some time label Oct 12, 2023
@thpani thpani self-assigned this Oct 12, 2023
@thpani
Copy link
Collaborator

thpani commented Oct 17, 2023

Partially addressed in #2758 – please reopen if this continues to be an issue.

@thpani thpani closed this as completed Oct 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature A new feature or functionality impact-medium Incremental improvement | unblocks non-critical work | saves some time
Projects
None yet
Development

No branches or pull requests

3 participants