diff --git a/.unreleased/bug-fixes/no-view1004.md b/.unreleased/bug-fixes/no-view1004.md new file mode 100644 index 0000000000..349a3d7e10 --- /dev/null +++ b/.unreleased/bug-fixes/no-view1004.md @@ -0,0 +1 @@ +Report an error, when --max-error > 1 and no --view is provided, see #2144 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 6b9020a5b9..6118cb8cdd 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 @@ -2,20 +2,13 @@ package at.forsyte.apalache.infra.passes.options import at.forsyte.apalache.infra.PassOptionException import at.forsyte.apalache.infra.tlc.TlcConfigParserApalache -import at.forsyte.apalache.infra.tlc.config.BehaviorSpec -import at.forsyte.apalache.infra.tlc.config.InitNextSpec -import at.forsyte.apalache.infra.tlc.config.TlcConfig +import at.forsyte.apalache.infra.tlc.config.{BehaviorSpec, InitNextSpec, TlcConfig, TlcConfigParseError} import at.forsyte.apalache.tla.lir.Feature -import at.forsyte.apalache.infra.tlc.config.TlcConfigParseError - import com.typesafe.scalalogging.LazyLogging -import java.io.File -import java.io.FileReader -import java.io.IOException import org.apache.commons.io.FilenameUtils -import scala.util.Failure -import scala.util.Success -import scala.util.Try + +import java.io.{File, FileReader, IOException} +import scala.util.{Failure, Success, Try} /** * The components of this package specify the configurations and options used to configure Apalache @@ -580,25 +573,36 @@ object OptionGroup extends LazyLogging { extends OptionGroup object Checker extends Configurable[Config.Checker, Checker] with LazyLogging { - def apply(checker: Config.Checker): Try[Checker] = for { - algo <- checker.algo.toTry("checker.algo") - discardDisabled <- checker.discardDisabled.toTry("checker.discardDisabled") - length <- checker.length.toTry("checker.length") - maxError <- checker.maxError.toTry("checker.maxError") - noDeadlocks <- checker.noDeadlocks.toTry("checker.noDeadlocks") - nworkers <- checker.nworkers.toTry("checker.nworkers") - smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding") - tuning <- checker.tuning.toTry("checker.tuning") - } yield Checker( - algo = algo, - discardDisabled = discardDisabled, - length = length, - maxError = maxError, - noDeadlocks = noDeadlocks, - nworkers = nworkers, - smtEncoding = smtEncoding, - tuning = tuning, - ) + def apply(checker: Config.Checker): Try[Checker] = { + + def validateMaxError(n: Int) = + if (n > 1 && checker.view.isEmpty) { + val msg = s"Option maxError = ${n} requires a view. None specified." + Failure(new PassOptionException(msg)) + } else { + Success(n) + } + + for { + algo <- checker.algo.toTry("checker.algo") + 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) + } yield Checker( + algo = algo, + discardDisabled = discardDisabled, + 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 433be11984..6b0e56dd6e 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 @@ -3,11 +3,12 @@ package at.forsyte.apalache.tla.tooling.opt import at.forsyte.apalache.infra.PassOptionException import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.config.CheckerModule -import java.io.{File, FileNotFoundException} import org.apache.commons.configuration2.builder.fluent.Configurations import org.apache.commons.configuration2.ex.ConfigurationException import org.backuity.clist._ import org.backuity.clist.util.Read + +import java.io.{File, FileNotFoundException} import scala.jdk.CollectionConverters._ import at.forsyte.apalache.infra.passes.options.Config import at.forsyte.apalache.infra.passes.options.OptionGroup @@ -52,12 +53,12 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci var maxError: Option[Int] = opt[Option[Int]](name = "max-error", description = - "do not stop on first error, but produce up to a given number of counterexamples (fine tune with --view), default: 1", + "do not stop on first error, but produce at most the given number of errors (requires --view when greater than 1), default: 1", default = None) var view: Option[String] = - opt[Option[String]](name = "view", - description = "the state view to use with --max-error=n, default: transition index", default = None) + opt[Option[String]](name = "view", description = "the state view to use with --max-error=n, default: none", + default = None) var saveRuns: Boolean = opt[Boolean](name = "output-traces", description = "save an example trace for each symbolic run, default: false", diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 99e4d3e8fd..9f98cbadf4 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -2078,6 +2078,16 @@ The outcome is: Error EXITCODE: ERROR (12) ``` +### check View2.tla without --view + +```sh +$ apalache-mc check --inv=Inv --max-error=10 View2.tla | sed 's/[IEW]@.*//' +... +Option maxError = 10 requires a view. None specified. +... +EXITCODE: ERROR (255) +``` + ### check bug #874 Unhandled `IllegalArgumentException` when accessing a non-existent field on a