Merge branch 'unstable' of https://github.com/informalsystems/apalache …

…into ro/infinite-sets-bug

docs/src/tutorials/symbmc.md

@@ -175,7 +175,7 @@ has a finite diameter (more specifically, a diameter of 6), because:
   1. for any \\(k \ge 6\\), \\(r(k) = r(6) = R\\)
 
 ### Invariants
-Much like `Init`, an invariant operator `Inv` defines a predicate. However, it is not, in general, the case that `Inv` defines a predicate over `S`. There are different cases we can consider, discussed in more detail [here](../apalache/invariants.md). For the purposes of this document, we focus on _state invariants_, i.e. operators which use only unprimed variables and no temporal- or trace- operators. A state invariant operator `Inv` defines a predicate \\(I\\) over \\(S\\).
+Much like `Init`, an invariant operator `Inv` defines a predicate. However, it is not, in general, the case that `Inv` defines a predicate over `S`. There are different cases we can consider, discussed in more detail [here](../apalache/principles/invariants.md). For the purposes of this document, we focus on _state invariants_, i.e. operators which use only unprimed variables and no temporal- or trace- operators. A state invariant operator `Inv` defines a predicate \\(I\\) over \\(S\\).
 We say that the \\(I\\) is an _invariant_ in the transition system, if \\(R \subseteq I\\), that is, for every reachable state \\(s_r \in R\\), \\(I(s_r)\\) holds true. If \\(R \setminus I\\) is nonempty (i.e., there exists a state \\(s_r \in R\\), such that \\(\neg I(s_r)\\)), we refer to elements of \\(R \setminus I\\) as _witnesses_ to invariant violation.
 
 ### Goals of model checking

mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala

@@ -5,21 +5,25 @@ import com.typesafe.scalalogging.LazyLogging
 /**
  * An abstract error message.
  */
-sealed abstract class ErrorMessage
+sealed abstract class ErrorMessage {
+
+  /** The concrete content of a message */
+  val msg: String
+}
 
 /**
  * A normal error that does not require a stack trace.
  * @param msg
  *   the message text
  */
-case class NormalErrorMessage(msg: String) extends ErrorMessage
+case class NormalErrorMessage(val msg: String) extends ErrorMessage
 
 /**
  * A failure message that should be printed along with a stack trace.
  * @param msg
  *   the message text
  */
-case class FailureMessage(msg: String) extends ErrorMessage
+case class FailureMessage(val msg: String) extends ErrorMessage
 
 /**
  * ExceptionAdapter allows us to convert an exception into a message string. The purpose of the adapter is to push the

mod-infra/src/main/scala/at/forsyte/apalache/infra/Executor.scala

@@ -0,0 +1,41 @@
+package at.forsyte.apalache.infra
+
+import at.forsyte.apalache.infra.passes.{Pass, PassChainExecutor, ToolModule, WriteablePassOptions}
+import com.google.inject.Guice
+
+/**
+ * This Executor abstracts the dependency injection and execution logic required for executing a PassChainExecutor
+ *
+ * @param toolModule
+ *   The [[ToolModule]] that specifies the sequence of passes
+ * @throws [[AdaptedException]]
+ *   if any exceptions are caught by the configured [[ExceptionAdapter]]
+ * @author
+ *   Shon Feder
+ */
+case class Executor(val toolModule: ToolModule) {
+  private val injector = Guice.createInjector(toolModule)
+
+  /** Exposes mutable access to options configuring the behavior of the [passChainExecutor] */
+  val passOptions = injector.getInstance(classOf[WriteablePassOptions])
+
+  private val exceptionAdapter = injector.getInstance(classOf[ExceptionAdapter])
+
+  private val passChainExecutor = {
+    val passes = toolModule.passes.zipWithIndex.map { case (p, i) =>
+      injector.getInstance(p).withNumber(i)
+    }
+    new PassChainExecutor(passOptions, passes)
+  }
+
+  /** Run the underlying PassChainExecutor, adapting exceptions as needed, and returning a `PassResult` */
+  def run(): Pass.PassResult = {
+    try {
+      passChainExecutor.run()
+    } catch {
+      case e: Throwable if exceptionAdapter.toMessage.isDefinedAt(e) =>
+        throw new AdaptedException(exceptionAdapter.toMessage(e))
+    }
+  }
+
+}

mod-infra/src/main/scala/at/forsyte/apalache/infra/exceptions.scala

@@ -14,3 +14,10 @@ class PassExecException(message: String) extends Exception(message)
  *   an error message
  */
 class PassOptionException(message: String) extends Exception(message)
+
+/**
+ * An error that has been adapted by the [[ExceptionAdaptor]]
+ * @param err
+ *   the [[ErrorMessage]] into which the originating error was adapted
+ */
+class AdaptedException(val err: ErrorMessage) extends Exception(err.msg)