add `--timeout-smt` to `check` and `simulate`

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint

https://apalache-mc.org/

Apache License 2.0

429 stars 40 forks source link

add `--timeout-smt` to `check` and `simulate` #2936

Closed konnov closed 1 month ago

konnov commented 1 month ago

In our experiments, it sometimes happens that apalache-mc simulate gets stuck in a randomly selected schedule, without progressing for many hours. Since we would like to get quicker feedback with simulate, this PR add the CLI option --timeout-smt that limits the time spent on a single SMT query. Also, we are removing the old tuning option search.smt.timeout, which is hard to discover.

[x] Tests added for any new code
[x] Ran make fmt-fix (or had formatting run automatically on all files edited)
[x] Documentation added for any new functionality
[x] Entries added to ./unreleased/ for any new functionality

Kukovec commented 1 month ago

As a question unrelated to the review, should we be supporting timeout-smt with check? Simulation is probabilistic anyway, so no real harm there, but setting a timeout may incorrectly give the impression that check succeeded, since the behavior is to assume invariants hold whenever timeouts happen.

konnov commented 1 month ago

As a question unrelated to the review, should we be supporting timeout-smt with check? Simulation is probabilistic anyway, so no real harm there, but setting a timeout may incorrectly give the impression that check succeeded, since the behavior is to assume invariants hold whenever timeouts happen.

check --timeout-smt=n finishes with a runtime error on timeout. Also, in case of simulate, the user gets a message that there were timeouts.

Kukovec commented 1 month ago

check --timeout-smt=n finishes with a runtime error on timeout. Also, in case of simulate, the user gets a message that there were timeouts.

I see a lot of searchState.onResult(RuntimeError()) replaced with searchState.onResult(SmtTimeout(...)). Is it this bit? https://github.com/apalache-mc/apalache/blob/f7aeb232442052916bca82b1708b8eb9bc594fa7/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala#L269-L274

konnov commented 1 month ago

check --timeout-smt=n finishes with a runtime error on timeout. Also, in case of simulate, the user gets a message that there were timeouts.

I see a lot of searchState.onResult(RuntimeError()) replaced with searchState.onResult(SmtTimeout(...)). Is it this bit?

https://github.com/apalache-mc/apalache/blob/f7aeb232442052916bca82b1708b8eb9bc594fa7/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala#L269-L274

Yeah. This is the clear distinction here. There are other cases where I am less certain. In any case, you will get a message that there were timeouts. I think we should play with this UX a bit and figure out what works the best.