Merge pull request #2936 from apalache-mc/igor/search-timeout

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

.unreleased/features/timeout-smt.md

@@ -0,0 +1 @@
+Add `--timeout-smt` to limit SMT queries (#2936)

docs/src/apalache/tuning.md

@@ -22,14 +22,6 @@ The following options are supported:
 `smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
 `sat.random_seed` and `smt.random_seed`).
 
-##  Timeouts
-
-`search.smt.timeout=<seconds>` 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

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,

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(

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"
     }

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"
 

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

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

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.
    */

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
     }