diff --git a/.unreleased/features/timeout-smt.md b/.unreleased/features/timeout-smt.md new file mode 100644 index 0000000000..dd27979cfb --- /dev/null +++ b/.unreleased/features/timeout-smt.md @@ -0,0 +1 @@ +Add `--timeout-smt` to limit SMT queries (#2936) diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index d3a60c5eeb..22aa77b99a 100644 --- a/docs/src/apalache/tuning.md +++ b/docs/src/apalache/tuning.md @@ -22,14 +22,6 @@ The following options are supported: `smt.randomSeed=` passes the random seed to `z3` (via `z3`'s parameters `sat.random_seed` and `smt.random_seed`). -## Timeouts - -`search.smt.timeout=` defines the timeout to the SMT solver in seconds. -The default value is `0`, which stands for the unbounded timeout. For instance, -the timeout is used in the following cases: checking if a transition is enabled, -checking an invariant, checking for deadlocks. If the solver times out, it -reports 'UNKNOWN', and the model checker reports a runtime error. - ## Invariant mode `search.invariant.mode=(before|after)` defines the moment when the invariant is diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala index 4d676aa3c4..201e26ae1a 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala +++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala @@ -162,6 +162,8 @@ object Config { * maximal number of Next steps * @param maxError * whether to stop on the first error or to produce up to a given number of counterexamples + * @param timeoutSmtSec + * the time limit on SMT queries in seconds * @param noDeadLocks * do not check for deadlocks * @param smtEncoding @@ -182,6 +184,7 @@ object Config { next: Option[String] = None, length: Option[Int] = Some(10), maxError: Option[Int] = Some(1), + timeoutSmtSec: Option[Int] = Some(0), noDeadlocks: Option[Boolean] = Some(false), smtEncoding: Option[SMTEncoding] = Some(SMTEncoding.OOPSLA19), temporalProps: Option[List[String]] = None, @@ -660,6 +663,7 @@ object OptionGroup extends LazyLogging { discardDisabled: Boolean, length: Int, maxError: Int, + timeoutSmtSec: Int, noDeadlocks: Boolean, smtEncoding: SMTEncoding, tuning: Map[String, String]) @@ -684,11 +688,13 @@ object OptionGroup extends LazyLogging { smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding") tuning <- checker.tuning.toTry("checker.tuning") maxError <- checker.maxError.toTry("checker.maxError").flatMap(validateMaxError) + timeoutSmtSec <- checker.timeoutSmtSec.toTry("checker.timeoutSmtSec") } yield Checker( algo = algo, discardDisabled = discardDisabled, length = length, maxError = maxError, + timeoutSmtSec = timeoutSmtSec, noDeadlocks = noDeadlocks, smtEncoding = smtEncoding, tuning = tuning, diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala index ea957e1bce..20a5773436 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala +++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala @@ -69,6 +69,11 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci opt[Boolean](name = "output-traces", description = "save an example trace for each symbolic run, default: false", default = false) + var timeoutSmtSec: Option[Int] = + opt[Option[Int]](name = "timeout-smt", + description = "limit the duration of a single SMT check query with `n` seconds, default: 0 (unlimited)", + default = None) + override def toConfig(): Try[Config.ApalacheConfig] = { val loadedTuningOptions = tuningOptionsFile.map(f => loadProperties(f)).getOrElse(Map()) val combinedTuningOptions = overrideProperties(loadedTuningOptions, tuningOptions.getOrElse("")) ++ Map( @@ -83,6 +88,7 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci discardDisabled = discardDisabled, noDeadlocks = noDeadlocks, maxError = maxError, + timeoutSmtSec = timeoutSmtSec, view = view, ), typechecker = cfg.typechecker.copy( diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index d2debd6027..cfa06d6d28 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -1770,6 +1770,18 @@ The outcome is: NoError EXITCODE: OK ``` +### simulate Paxos.tla with timeout succeeds + +While we cannot rely on an actual timeout happening or not, we can make sure that the option is properly parsed. + +```sh +$ apalache-mc simulate --timeout-smt=1 --length=10 --inv=Inv Paxos.tla | sed 's/I@.*//' +... +The outcome is: NoError +... +EXITCODE: OK +``` + ### simulate y2k with --output-traces succeeds ```sh @@ -3892,6 +3904,7 @@ checker { smt-encoding { type=oopsla-19 } + timeout-smt-sec=0 tuning { "search.outputTraces"="false" } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala index 1723856d11..8bef8a9b07 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala @@ -23,6 +23,8 @@ object Checker { Obj("checking_result" -> "Error", "counterexamples" -> counterexamples, "nerrors" -> nerrors) case Deadlock(counterexample) => Obj("checking_result" -> "Deadlock", "counterexamples" -> counterexample.toList) + case SmtTimeout(nTimeouts) => + Obj("checking_result" -> "SmtTimeout", "ntimeouts" -> nTimeouts) case other => Obj("checking_result" -> other.toString()) } @@ -60,6 +62,20 @@ object Checker { override val isOk: Boolean = true } + /** + * The SMT solver reported a timeout. It should still be possible to check other verification conditions. + * @param nTimeouts + * the number of timeouts, normally, just 1. + */ + case class SmtTimeout(nTimeouts: Int) extends CheckerResult { + override def toString: String = "SmtTimeout" + + /** + * Whether this result shall be reported as success (`true`) or error (`false`). + */ + override val isOk: Boolean = true + } + case class Interrupted() extends CheckerResult { override def toString: String = "Interrupted" diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala index e7360504ff..da36921b93 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala @@ -94,7 +94,7 @@ class SeqModelChecker[ExecutorContextT]( */ private def outputExampleRun(): Unit = { logger.info("Constructing an example run") - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => listeners.foreach(_.onExample(checkerInput.rootModule, trex.decodedExecution(), searchState.nRunsLeft)) case Some(false) => @@ -128,8 +128,8 @@ class SeqModelChecker[ExecutorContextT]( if (!params.discardDisabled && params.checkForDeadlocks) { // We do this check only if all transitions are unconditionally enabled. // Otherwise, we should have found it already. - logger.info(s"Step %d: checking for deadlocks".format(trex.stepNo)) - trex.sat(params.smtTimeoutSec) match { + logger.info(f"Step ${trex.stepNo}: checking for deadlocks") + trex.sat(params.timeoutSmtSec) match { case Some(true) => () // OK case Some(false) => @@ -145,7 +145,8 @@ class SeqModelChecker[ExecutorContextT]( searchState.onResult(Deadlock(counterexample)) case None => - searchState.onResult(RuntimeError()) + logger.info(f"Step ${trex.stepNo}: checking for deadlocks => TIMEOUT") + searchState.onResult(SmtTimeout(1)) } } @@ -204,6 +205,9 @@ class SeqModelChecker[ExecutorContextT]( val transitionIndices = if (params.isRandomSimulation) Random.shuffle(transitions.indices.toList) else transitions.indices + // keep track of SMT timeouts + var nTimeouts = 0 + for (no <- transitionIndices) { var snapshot: Option[SnapshotT] = None if (params.discardDisabled) { @@ -221,7 +225,7 @@ class SeqModelChecker[ExecutorContextT]( val assumeSnapshot = trex.snapshot() // assume that the transition is fired and check, whether the constraints are satisfiable trex.assumeTransition(no) - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => logger.debug(s"Step ${trex.stepNo}: Transition #$no is enabled") // recover to the state before the transition was fired @@ -263,7 +267,8 @@ class SeqModelChecker[ExecutorContextT]( case None => if (params.isRandomSimulation) { - logger.info(s"Step ${trex.stepNo}: Transition #$no enabledness is UNKNOWN; assuming it is disabled") + logger.info(s"Step ${trex.stepNo}: Transition #$no => TIMEOUT. Transition ignored.") + nTimeouts += 1 } else { searchState.onResult(RuntimeError()) return (Set.empty, Set.empty) // UNKNOWN or timeout @@ -284,7 +289,13 @@ class SeqModelChecker[ExecutorContextT]( } if (trex.preparedTransitionNumbers.isEmpty) { - if (params.checkForDeadlocks) { + if (nTimeouts > 0 || !params.checkForDeadlocks) { + // Either (1) there were timeouts, and we cannot claim to have found a deadlock, + // or (2) the user does not care about deadlocks + val msg = "All executions are shorter than the provided bound." + logger.warn(msg) + searchState.onResult(ExecutionsTooShort()) + } else { val counterexample = if (trex.sat(0).contains(true)) { val cx = Counterexample(checkerInput.rootModule, trex.decodedExecution(), tla.bool(true)) notifyOnError(cx, searchState.nFoundErrors) @@ -295,10 +306,6 @@ class SeqModelChecker[ExecutorContextT]( None } searchState.onResult(Deadlock(counterexample)) - } else { - val msg = "All executions are shorter than the provided bound." - logger.warn(msg) - searchState.onResult(ExecutionsTooShort()) } (Set.empty, Set.empty) } else { @@ -355,7 +362,7 @@ class SeqModelChecker[ExecutorContextT]( // check the invariant trex.assertState(notInv) - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => val counterexample = Counterexample(checkerInput.rootModule, trex.decodedExecution(), notInv) searchState.onResult(Error(1, Seq(counterexample))) @@ -369,8 +376,10 @@ class SeqModelChecker[ExecutorContextT]( logger.info(f"State ${stateNo}: ${kind} invariant ${invNo} holds.") case None => - // UNKNOWN or timeout - searchState.onResult(RuntimeError()) + // UNKNOWN or timeout. Assume that the invariant holds true, so we can continue. + invariantHolds = true + logger.info(f"State ${stateNo}: ${kind} invariant ${invNo} => TIMEOUT. Assuming it holds true.") + searchState.onResult(SmtTimeout(1)) } // rollback the context @@ -401,7 +410,7 @@ class SeqModelChecker[ExecutorContextT]( val traceInvApp = applyTraceInv(notInv) trex.assertState(traceInvApp) - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => val counterexample = Counterexample(checkerInput.rootModule, trex.decodedExecution(), traceInvApp) searchState.onResult(Error(1, Seq(counterexample))) @@ -415,7 +424,10 @@ class SeqModelChecker[ExecutorContextT]( invariantHolds = true case None => - searchState.onResult(RuntimeError()) + // Timeout. Assume that the invariant holds true, so we can continue. + invariantHolds = true + logger.info(f"State ${stateNo}: trace invariant ${invNo} => TIMEOUT. Assuming it holds true.") + searchState.onResult(SmtTimeout(1)) } // rollback the context diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala index 39cebd8a91..aa2b3bb34a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala @@ -70,6 +70,7 @@ class BoundedCheckerPassImpl @Inject() ( params.discardDisabled = options.checker.discardDisabled params.checkForDeadlocks = !options.checker.noDeadlocks params.nMaxErrors = options.checker.maxError + params.timeoutSmtSec = options.checker.timeoutSmtSec params.smtEncoding = smtEncoding val smtProfile = options.common.smtprof diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala index 2c7a052aad..8847475fb0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala @@ -68,6 +68,11 @@ class ModelCheckerParams( */ var nMaxErrors: Int = 1 + /** + * The limit on a single SMT query. The default value is 0 (unlimited). + */ + var timeoutSmtSec: Int = 0 + /** * A timeout upon which a transition is split in its own group. This is the minimal timeout. The actual timeout is * updated at every step using `search.split.timeout.factor`. In our experiments, small timeouts lead to explosion of @@ -96,9 +101,6 @@ class ModelCheckerParams( */ def idleTimeoutMs: Long = idleTimeoutSec * 1000 - val smtTimeoutSec: Int = - tuningOptions.getOrElse("search.smt.timeout", "0").toInt - /** * The SMT encoding to be used. */ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala index 0981dbf004..3a8497250d 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala @@ -18,6 +18,7 @@ class SearchState(params: ModelCheckerParams) { private var _result: CheckerResult = NoError() private var _nFoundErrors: Int = 0 + private var _nTimeouts: Int = 0 private val _counterexamples: ListBuffer[Counterexample] = ListBuffer.empty private var _nRunsLeft: Int = if (params.isRandomSimulation) params.nSimulationRuns else 1 @@ -30,6 +31,14 @@ class SearchState(params: ModelCheckerParams) { */ def nFoundErrors: Int = _nFoundErrors + /** + * Get the number of SMT timeouts that occurred in the search. + * + * @return + * number of timeouts + */ + def nTimeouts: Int = _nTimeouts + /** * Get the number of simulation runs to explore. * @@ -49,6 +58,8 @@ class SearchState(params: ModelCheckerParams) { case NoError() => if (_nFoundErrors > 0) { Error(_nFoundErrors, _counterexamples.toList) + } else if (_nTimeouts > 0) { + SmtTimeout(_nTimeouts) } else { NoError() } @@ -98,6 +109,11 @@ class SearchState(params: ModelCheckerParams) { _result = Deadlock(counterexample) } + case SmtTimeout(nTimeouts) => + // we still continue the search, but report incompleteness in [[this.finalResult]]. + _nTimeouts += nTimeouts + _result = NoError() + case _ => _result = result }