From 9d7a7604477aeadf118fd2e53f4009d5f6d39564 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 18 Oct 2023 09:08:38 +0200 Subject: [PATCH] Remove `--nworkers` (#2759) * Remove `--nworkers` * Update changelog * Fix integration tests --- .unreleased/breaking-changes/2759-drop-nworkers.md | 1 + .../scala/at/forsyte/apalache/infra/passes/options.scala | 6 ------ .../at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala | 3 --- .../at/forsyte/apalache/tla/tooling/opt/TestCmd.scala | 1 - test/tla/ChangRobertsTyped_Test.tla | 1 - test/tla/cli-integration-tests.md | 1 - .../tla/bmcmt/passes/BoundedCheckerPassImpl.scala | 8 -------- 7 files changed, 1 insertion(+), 20 deletions(-) create mode 100644 .unreleased/breaking-changes/2759-drop-nworkers.md diff --git a/.unreleased/breaking-changes/2759-drop-nworkers.md b/.unreleased/breaking-changes/2759-drop-nworkers.md new file mode 100644 index 0000000000..16ff9cc405 --- /dev/null +++ b/.unreleased/breaking-changes/2759-drop-nworkers.md @@ -0,0 +1 @@ +Removed the (unused) `--nworkers` flag, see #2275 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 1d1af13861..4d676aa3c4 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 @@ -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, ) 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 6de6838765..ea957e1bce 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 @@ -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), diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala index a581f5e353..ba718f35da 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala +++ b/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), diff --git a/test/tla/ChangRobertsTyped_Test.tla b/test/tla/ChangRobertsTyped_Test.tla index 6fc4b78dd5..2eb776b984 100644 --- a/test/tla/ChangRobertsTyped_Test.tla +++ b/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 diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index f2bf1aaff1..52789aecde 100644 --- a/test/tla/cli-integration-tests.md +++ b/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 } 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 b47dd0baea..c74fdafdc3 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 @@ -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) }