Report an error when --max-error > 1 and no --view is provided (#2144)

See #2139
apalache-mc · Sep 9, 2022 · bf1e8f4 · bf1e8f4
1 parent 5987b87
commit bf1e8f4
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 34 deletions.
diff --git a/.unreleased/bug-fixes/no-view1004.md 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
@@ -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
@@ -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
@@ -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