search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
441 stars 40 forks source link

Solver restart from timeout in simulate mode #2316

Closed rnbguy closed 1 year ago

rnbguy commented 1 year ago

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

thpani commented 1 year ago

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