Merge branch 'main' into jk/oracles2

.unreleased/breaking-changes/2759-drop-nworkers.md

@@ -0,0 +1 @@
+Removed the (unused) `--nworkers` flag, see #2275

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala

@@ -164,8 +164,6 @@ object Config {
    *   whether to stop on the first error or to produce up to a given number of counterexamples
    * @param noDeadLocks
    *   do not check for deadlocks
-   * @param nworkers
-   *   the number of workers for the parallel checker (not currently used)
    * @param smtEncoding
    *   the SMT encoding to use
    * @param temporalProps
@@ -185,7 +183,6 @@ object Config {
       length: Option[Int] = Some(10),
       maxError: Option[Int] = Some(1),
       noDeadlocks: Option[Boolean] = Some(false),
-      nworkers: Option[Int] = Some(1),
       smtEncoding: Option[SMTEncoding] = Some(SMTEncoding.OOPSLA19),
       temporalProps: Option[List[String]] = None,
       view: Option[String] = None)
@@ -664,7 +661,6 @@ object OptionGroup extends LazyLogging {
       length: Int,
       maxError: Int,
       noDeadlocks: Boolean,
-      nworkers: Int,
       smtEncoding: SMTEncoding,
       tuning: Map[String, String])
       extends OptionGroup
@@ -685,7 +681,6 @@ object OptionGroup extends LazyLogging {
         discardDisabled <- checker.discardDisabled.toTry("checker.discardDisabled")
         length <- checker.length.toTry("checker.length")
         noDeadlocks <- checker.noDeadlocks.toTry("checker.noDeadlocks")
-        nworkers <- checker.nworkers.toTry("checker.nworkers")
         smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding")
         tuning <- checker.tuning.toTry("checker.tuning")
         maxError <- checker.maxError.toTry("checker.maxError").flatMap(validateMaxError)
@@ -695,7 +690,6 @@ object OptionGroup extends LazyLogging {
           length = length,
           maxError = maxError,
           noDeadlocks = noDeadlocks,
-          nworkers = nworkers,
           smtEncoding = smtEncoding,
           tuning = tuning,
       )

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -36,8 +36,6 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
     Read.reads[Algorithm](s"a checking algorithm, either ${Algorithm.Incremental} or ${Algorithm.Offline}")(
         Algorithm.ofString)
 
-  var nworkers: Option[Int] = opt[Option[Int]](name = "nworkers", default = None,
-      description = "the number of workers for the parallel checker (soon), default: 1")
   var algo: Option[Algorithm] = opt[Option[Algorithm]](name = "algo", default = None,
       description = "the search algorithm: offline, incremental, parallel (soon), default: incremental")
   var smtEncoding: Option[SMTEncoding] = opt[Option[SMTEncoding]](name = "smt-encoding", useEnv = true, default = None,
@@ -79,7 +77,6 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
     super.toConfig().map { cfg =>
       val newCfg = cfg.copy(
           checker = cfg.checker.copy(
-              nworkers = nworkers,
               algo = algo,
               smtEncoding = smtEncoding,
               tuning = Some(combinedTuningOptions),

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala

@@ -47,7 +47,6 @@ class TestCmd
           next = Some(action),
           inv = Some(List(assertion)),
           cinit = cinit,
-          nworkers = Some(1),
           length = Some(1),
           discardDisabled = Some(false),
           noDeadlocks = Some(false),

test/tla/ChangRobertsTyped_Test.tla

@@ -158,7 +158,6 @@ GlobalCorrectness == []Correctness
 \* @testOption("tool", "apalache")
 \* @testOption("search.smt.timeout", 10)
 \* @testOption("checker.algo", "offline")
-\* @testOption("checker.nworkers", 2)
 TestExec_n0_n1_with_options ==
     TestExec_n0_n1
 

test/tla/cli-integration-tests.md

@@ -3817,7 +3817,6 @@ checker {
     length=0
     max-error=1
     no-deadlocks=false
-    nworkers=1
     smt-encoding {
         type=oopsla-19
     }

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala

@@ -60,10 +60,6 @@ class BoundedCheckerPassImpl @Inject() (
       CheckerInputVC(invariantsAndNegations.toList, actionInvariantsAndNegations.toList,
           traceInvariantsAndNegations.toList, optView)
     val input = new CheckerInput(module, initTrans.toList, nextTrans.toList, cinitP, verificationConditions)
-    /*
-        TODO: uncomment when the parallel checker is transferred from ik/multicore
-    val nworkers = options.getOrElse("checker", "nworkers", 1)
-     */
     val stepsBound = options.checker.length
     val debug = options.common.debug
     val tuning = options.checker.tuning
@@ -81,10 +77,6 @@ class BoundedCheckerPassImpl @Inject() (
     val solverConfig = SolverConfig(debug, smtProfile, smtRandomSeed, smtEncoding)
 
     val result = options.checker.algo match {
-      /*
-        TODO: uncomment when the parallel checker is transferred from ik/multicore
-      case "parallel" => runParallelChecker(params, input, tuning, nworkers)
-       */
       case Algorithm.Incremental => runIncrementalChecker(params, input, tuning, solverConfig)
       case Algorithm.Offline     => runOfflineChecker(params, input, tuning, solverConfig)
     }