From 4db48e48b9122cca7e348f5e483b79cbf6fa0000 Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas@informal.systems>
Date: Fri, 13 May 2022 11:49:17 +0200
Subject: [PATCH 1/4] Add new exit code constants

Co-authored-by: Shon Feder <shon@informal.systems>
---
 .../apalache/tla/tooling/ExitCodes.scala      | 53 +++++++++++++++----
 1 file changed, 43 insertions(+), 10 deletions(-)

diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala
index db721f4bfb..f99e91fcc2 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala
@@ -3,27 +3,60 @@ package at.forsyte.apalache.tla.tooling
 import tlc2.output.EC
 
 /**
- * Exit codes that are reported by Tool. In contrast, we are using a small subset of exit codes. Although we maintain
- * exit codes that are compatible with TLC, we believe that exit codes should not replace richer error explanations.
+ * Exit codes that are reported by `Tool`.
+ *
+ * We maintain compatibility with TLC on a small subset of its exit codes, believing that exit codes should not replace
+ * richer error explanations.
+ *
+ * TLC currently specifies exit codes
+ *   - 0 for success,
+ *   - 10–14 for (various kinds of) property violations,
+ *   - 75–77 for "failures" (e.g., properties that are tautologies, or primed variables in invariants), and
+ *   - 150–153 and 255 for syntax errors and system-level errors, respectively.
+ *
+ * Apalache uses exit codes
+ *   - 0 for success,
+ *   - 12 for all kinds of property violations,
+ *   - 75 for semantic failures to evaluate a specification,
+ *   - 120 for type-checking errors,
+ *   - 150 for syntactic errors, and
+ *   - 255 for general system-level errors.
  *
  * @author
- *   Igor Konnov
+ *   Igor Konnov, Thomas Pani
  */
 object ExitCodes {
+  type TExitCode = Int
+
+  /**
+   * No error in the specification.
+   */
+  val OK: TExitCode = EC.ExitStatus.SUCCESS // = 0
+
+  /**
+   * The model checker has found a counterexample. We do not distinguish between different kinds of counterexamples and
+   * always report VIOLATION_SAFETY.
+   */
+  val ERROR_COUNTEREXAMPLE: TExitCode = EC.ExitStatus.VIOLATION_SAFETY // = 12
+
+  /**
+   * Semantic failure to evaluate a specification, e.g. due to unsupported language constructs and operators, or those
+   * that introduce infinite structures.
+   */
+  val FAILURE_SPEC_EVAL: TExitCode = EC.ExitStatus.FAILURE_SPEC_EVAL // = 75
 
   /**
-   * This exit code should be used when the tool is reporting no error in a specification.
+   * Type-checking error.
    */
-  val OK: Int = EC.ExitStatus.SUCCESS
+  val ERROR_TYPECHECK: TExitCode = 120
 
   /**
-   * This exit code should be used when the model checker has found a counterexample. We do not distinguish between
-   * different kinds of counterexamples and always report VIOLATION_SAFETY.
+   * Syntactic error when parsing the spec.
    */
-  val ERROR_COUNTEREXAMPLE: Int = EC.ExitStatus.VIOLATION_SAFETY
+  val ERROR_SPEC_PARSE: TExitCode = EC.ExitStatus.ERROR_SPEC_PARSE // = 150
 
   /**
-   * This exit code should be used for other kinds of errors, e.g., configuration errors, type errors, runtime errors.
+   * All other kinds of errors, e.g., runtime errors.
    */
-  val ERROR: Int = EC.ExitStatus.ERROR
+  val ERROR: TExitCode = EC.ExitStatus.ERROR // 255
 }

From d8088df6331970a42978287eb897041162e6f880 Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas@informal.systems>
Date: Fri, 13 May 2022 11:57:25 +0200
Subject: [PATCH 2/4] Return either an exit code or the resulting TlaModule
 from a pass

Introduces the new return type PassResult = Either[TExitCode, TlaModule].
A pass returns either an exit code as Left(42) or the resulting TlaModule as Right(module).

Co-authored-by: Shon Feder <shon@informal.systems>
---
 .../forsyte/apalache/infra}/ExitCodes.scala   |  2 +-
 .../forsyte/apalache/infra/passes/Pass.scala  |  8 ++-
 .../infra/passes/PassChainExecutor.scala      | 37 +++++++------
 .../infra/passes/TestPassChainExecutor.scala  | 12 ++--
 .../scala/at/forsyte/apalache/tla/Tool.scala  | 25 ++++-----
 .../assignments/passes/PrimingPassImpl.scala  |  5 +-
 .../passes/TransitionPassImpl.scala           |  5 +-
 .../tla/bmcmt/passes/AnalysisPassImpl.scala   |  5 +-
 .../bmcmt/passes/BoundedCheckerPassImpl.scala | 10 ++--
 .../passes/ReTLAToVMTTranspilePassImpl.scala  |  5 +-
 .../tla/bmcmt/passes/VCGenPassImpl.scala      |  5 +-
 .../tla/imp/passes/SanyParserPassImpl.scala   | 55 +++++++++----------
 .../tla/pp/passes/ConfigurationPassImpl.scala |  5 +-
 .../tla/pp/passes/DesugarerPassImpl.scala     |  5 +-
 .../tla/pp/passes/InlinePassImpl.scala        |  5 +-
 .../apalache/tla/pp/passes/OptPassImpl.scala  |  5 +-
 .../tla/pp/passes/PreproPassImpl.scala        |  3 +-
 .../tla/pp/passes/PreproPassPartial.scala     | 10 ++--
 .../tla/pp/passes/ReTLAPreproPassImpl.scala   |  3 +-
 .../tla/pp/passes/WatchdogPassImpl.scala      |  5 +-
 .../passes/EtcTypeCheckerPassImpl.scala       |  8 ++-
 21 files changed, 120 insertions(+), 103 deletions(-)
 rename {mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling => mod-infra/src/main/scala/at/forsyte/apalache/infra}/ExitCodes.scala (97%)

diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExitCodes.scala
similarity index 97%
rename from mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala
rename to mod-infra/src/main/scala/at/forsyte/apalache/infra/ExitCodes.scala
index f99e91fcc2..5715e0d806 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/ExitCodes.scala
+++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExitCodes.scala
@@ -1,4 +1,4 @@
-package at.forsyte.apalache.tla.tooling
+package at.forsyte.apalache.infra
 
 import tlc2.output.EC
 
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/Pass.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/Pass.scala
index 15dbe320aa..5638b40cd1 100644
--- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/Pass.scala
+++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/Pass.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.infra.passes
 
+import at.forsyte.apalache.infra.ExitCodes.TExitCode
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
 
 /**
@@ -46,7 +48,7 @@ trait Pass {
    * @return
    *   the transformed module, if the pass was successful
    */
-  def execute(module: TlaModule): Option[TlaModule]
+  def execute(module: TlaModule): PassResult
 
   /**
    * List the dependencies of the pass. These are properties the module has to have in order to be processed by the
@@ -68,3 +70,7 @@ trait Pass {
   def transformations: Set[ModuleProperty.Value]
 
 }
+
+object Pass {
+  type PassResult = Either[TExitCode, TlaModule]
+}
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/PassChainExecutor.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/PassChainExecutor.scala
index 99bea8045d..7587ac356e 100644
--- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/PassChainExecutor.scala
+++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/PassChainExecutor.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.infra.passes
 
+import at.forsyte.apalache.infra.ExitCodes.TExitCode
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import com.typesafe.scalalogging.LazyLogging
 import at.forsyte.apalache.tla.lir.{MissingTransformationError, TlaModule, TlaModuleProperties}
 
@@ -15,12 +17,11 @@ import at.forsyte.apalache.tla.lir.{MissingTransformationError, TlaModule, TlaMo
  */
 
 class PassChainExecutor(val options: WriteablePassOptions, passes: Seq[Pass]) extends LazyLogging {
-
-  def run(): Option[TlaModule] = {
-    def exec(seqNo: Int, passToRun: Pass, module: TlaModule): Option[TlaModule] = {
+  def run(): PassResult = {
+    def exec(seqNo: Int, passToRun: Pass, module: TlaModule): PassResult = {
       logger.info("PASS #%d: %s".format(seqNo, passToRun.name))
       val result = passToRun.execute(module)
-      val outcome = if (result.isDefined) "[OK]" else "[FAIL]"
+      val outcome = result.fold(_ => "[FAIL]", _ => "[OK]")
       // TODO: As part of #858, PassWithOutputs.writeOut should be called here.
       logger.debug("PASS #%d: %s %s".format(seqNo, passToRun.name, outcome))
       result
@@ -34,21 +35,21 @@ class PassChainExecutor(val options: WriteablePassOptions, passes: Seq[Pass]) ex
       }
     }
 
-    passes.zipWithIndex
-      .foldLeft(Option[TlaModule with TlaModuleProperties](new TlaModule("empty", Seq()) with TlaModuleProperties)) {
-        case (moduleOpt, (pass, index)) =>
-          // Raise error if the pass dependencies aren't satisfied
-          moduleOpt.map { m => checkDependencies(m, pass) }
+    val emptyModuleWithProperties: TlaModule with TlaModuleProperties = new TlaModule("empty", Seq())
+      with TlaModuleProperties
+    val startValue: Either[TExitCode, TlaModule with TlaModuleProperties] = Right(emptyModuleWithProperties)
+    passes.zipWithIndex.foldLeft(startValue) { case (moduleOpt, (pass, index)) =>
+      // Raise error if the pass dependencies aren't satisfied
+      moduleOpt.map { m => checkDependencies(m, pass) }
 
-          for {
-            module <- moduleOpt
-            transformedModule <- exec(index, pass, module)
-          } yield {
-            val newModule = new TlaModule(transformedModule.name, transformedModule.declarations)
-              with TlaModuleProperties
-            newModule.properties = module.properties ++ pass.transformations
-            newModule
-          }
+      for {
+        module <- moduleOpt
+        transformedModule <- exec(index, pass, module)
+      } yield {
+        val newModule = new TlaModule(transformedModule.name, transformedModule.declarations) with TlaModuleProperties
+        newModule.properties = module.properties ++ pass.transformations
+        newModule
       }
+    }
   }
 }
diff --git a/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala b/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala
index 10710d604d..78b07c1ff2 100644
--- a/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala
+++ b/mod-infra/src/test/scala/at/forsyte/apalache/infra/passes/TestPassChainExecutor.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.infra.passes
 
+import at.forsyte.apalache.infra.ExitCodes
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import org.junit.runner.RunWith
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatestplus.junit.JUnitRunner
@@ -11,11 +13,11 @@ class TestPassChainExecutor extends AnyFunSuite {
   class ParametrizedPass(result: Boolean, deps: Set[ModuleProperty.Value], transfs: Set[ModuleProperty.Value])
       extends Pass {
     override def name = "TestPass"
-    override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+    override def execute(tlaModule: TlaModule): PassResult = {
       if (result) {
-        Some(new TlaModule("TestModule", Seq()))
+        Right(TlaModule("TestModule", Seq()))
       } else {
-        None
+        Left(ExitCodes.ERROR)
       }
     }
     override def dependencies = deps
@@ -30,7 +32,7 @@ class TestPassChainExecutor extends AnyFunSuite {
 
     val executor = new PassChainExecutor(options, Seq(pass1, pass2))
     val result = executor.run()
-    assert(result.isDefined)
+    assert(result.isRight)
   }
 
   test("""Throws error on a bad ordered chain""") {
@@ -54,6 +56,6 @@ class TestPassChainExecutor extends AnyFunSuite {
     val executor = new PassChainExecutor(options, Seq(pass1, pass2))
 
     val result = executor.run()
-    assert(result.isEmpty)
+    assert(result.isLeft)
   }
 }
diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
index f6222f2a7a..9db7ef6573 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
@@ -2,15 +2,14 @@ package at.forsyte.apalache.tla
 
 // Generated from the build.sbt file by the buildInfo plugin
 import apalache.BuildInfo
+import at.forsyte.apalache.infra._
 import at.forsyte.apalache.infra.log.LogbackConfigurator
 import at.forsyte.apalache.infra.passes.{PassChainExecutor, ToolModule, WriteablePassOptions}
-import at.forsyte.apalache.infra.{ExceptionAdapter, FailureMessage, NormalErrorMessage, PassOptionException}
 import at.forsyte.apalache.io.{ConfigManager, ConfigurationError, OutputManager, ReportGenerator}
 import at.forsyte.apalache.tla.bmcmt.config.{CheckerModule, ReTLAToVMTModule}
 import at.forsyte.apalache.tla.bmcmt.rules.vmt.TlaExToVMTWriter
 import at.forsyte.apalache.tla.imp.passes.ParserModule
 import at.forsyte.apalache.tla.lir.TlaModule
-import at.forsyte.apalache.tla.tooling.ExitCodes
 import at.forsyte.apalache.tla.tooling.opt._
 import at.forsyte.apalache.tla.typecheck.passes.TypeCheckerModule
 import com.google.inject.{Guice, Injector}
@@ -37,8 +36,8 @@ object Tool extends LazyLogging {
   lazy val ISSUES_LINK: String = "[https://github.com/informalsystems/apalache/issues]"
 
   /**
-   * Run the tool in the standalone mode with the provided arguments. This method calls System.exit with the computed
-   * exit code. If you like to call the tool without System.exit, use the the Tool#run.
+   * Run the tool in the standalone mode with the provided arguments. This method calls [[System.exit]] with the
+   * computed exit code. To call the tool without System.exit, use [[run]].
    *
    * @param args
    *   the command line arguments
@@ -184,15 +183,15 @@ object Tool extends LazyLogging {
   private def runAndExit(
       executor: PassChainExecutor,
       msgIfOk: TlaModule => String,
-      msgIfFail: String,
-      errCode: Int = ExitCodes.ERROR): Int = {
+      msgIfFail: String): ExitCodes.TExitCode = {
     val result = executor.run()
-    if (result.isDefined) {
-      logger.info(msgIfOk(result.get))
-      ExitCodes.OK
-    } else {
-      logger.info(msgIfFail)
-      errCode
+    result match {
+      case Left(errorCode) =>
+        logger.info(msgIfFail)
+        errorCode
+      case Right(module) =>
+        logger.info(msgIfOk(module))
+        ExitCodes.OK
     }
   }
 
@@ -265,7 +264,6 @@ object Tool extends LazyLogging {
         executor,
         _ => "Checker reports no error up to computation length " + check.length,
         "Checker has found an error",
-        ExitCodes.ERROR_COUNTEREXAMPLE,
     )
   }
 
@@ -308,7 +306,6 @@ object Tool extends LazyLogging {
         executor,
         _ => "No example found",
         "Checker has found an example. Check counterexample.tla.",
-        ExitCodes.ERROR_COUNTEREXAMPLE,
     )
   }
 
diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala
index 358b601ccc..a1122224de 100644
--- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala
+++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/PrimingPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.assignments.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.io.lir.TlaWriterFactory
@@ -18,7 +19,7 @@ class PrimingPassImpl @Inject() (options: PassOptions, tracker: TransformationTr
 
   override def name: String = "PrimingPass"
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     val declarations = tlaModule.declarations
     val varSet = tlaModule.varDeclarations.map(_.name).toSet
     val constSet = tlaModule.constDeclarations.map(_.name).toSet
@@ -57,7 +58,7 @@ class PrimingPassImpl @Inject() (options: PassOptions, tracker: TransformationTr
 
     writeOut(writerFactory, newModule)
 
-    Some(newModule)
+    Right(newModule)
   }
 
   override def dependencies = Set(ModuleProperty.Configured)
diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala
index f69098ce92..829414c2a8 100644
--- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala
+++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.assignments.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.assignments._
 import at.forsyte.apalache.tla.imp.findBodyOf
@@ -27,7 +28,7 @@ class TransitionPassImpl @Inject() (
 
   override def name: String = "TransitionFinderPass"
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     // extract transitions from InitPrimed
     val initOperName = options.getOrElse("checker", "init", "Init")
     val initOperNamePrimed = initOperName + "Primed"
@@ -75,7 +76,7 @@ class TransitionPassImpl @Inject() (
     // print the resulting module
     writeOut(writerFactory, outModule)
 
-    Some(outModule)
+    Right(outModule)
   }
 
   private def extractTransitions(module: TlaModule, inOperName: String, outOperName: String): Seq[TlaOperDecl] = {
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala
index d8be80f994..b91b73d79b 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/AnalysisPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.bmcmt.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.bmcmt.analyses._
 import at.forsyte.apalache.io.lir.TlaWriterFactory
@@ -27,7 +28,7 @@ class AnalysisPassImpl @Inject() (
     override def compare(x: Object, y: Object): Int = x.toString.compare(y.toString)
   }
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
+  override def execute(module: TlaModule): PassResult = {
     val transformationSequence =
       List(
           // mark some expressions as to be Skolemized
@@ -65,7 +66,7 @@ class AnalysisPassImpl @Inject() (
 
     logger.info("  > Introduced expression grades")
 
-    Some(marked)
+    Right(marked)
   }
 
   override def dependencies = Set(ModuleProperty.TransitionsFound)
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 babd725d2f..0870a75231 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
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.passes
 
+import at.forsyte.apalache.infra.ExitCodes
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.assignments.ModuleAdapter
 import at.forsyte.apalache.tla.bmcmt._
@@ -33,7 +35,7 @@ class BoundedCheckerPassImpl @Inject() (
 
   override def name: String = "BoundedChecker"
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
+  override def execute(module: TlaModule): PassResult = {
     for (decl <- module.operDeclarations) {
       LanguageWatchdog(KeraLanguagePred()).check(decl.body)
     }
@@ -86,11 +88,7 @@ class BoundedCheckerPassImpl @Inject() (
       case algo          => throw new IllegalArgumentException(s"Unexpected checker.algo=$algo")
     }
 
-    if (result) {
-      Some(module)
-    } else {
-      None
-    }
+    if (result) Right(module) else Left(ExitCodes.ERROR_COUNTEREXAMPLE)
   }
 
   private def runIncrementalChecker(
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/ReTLAToVMTTranspilePassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/ReTLAToVMTTranspilePassImpl.scala
index 5401e14d7d..290e1c9bef 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/ReTLAToVMTTranspilePassImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/ReTLAToVMTTranspilePassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.bmcmt.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.bmcmt.rules.vmt.TlaExToVMTWriter
 import at.forsyte.apalache.tla.lir.oper.TlaActionOper
@@ -35,7 +36,7 @@ class ReTLAToVMTTranspilePassImpl @Inject() (
         (d.name, d.body)
       }
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
+  override def execute(module: TlaModule): PassResult = {
     // Check if still ok fragment (sanity check, see postTypeChecker)
     LanguageWatchdog(pred).check(module)
 
@@ -54,7 +55,7 @@ class ReTLAToVMTTranspilePassImpl @Inject() (
     vmtWriter.annotateAndWrite(module.varDeclarations, module.constDeclarations, cinitP, initTrans, nextTrans,
         vcInvs ++ vcActionInvs)
 
-    Some(module)
+    Right(module)
   }
 
   override def dependencies = Set()
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala
index a410005b2b..49f24ded42 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/VCGenPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.bmcmt.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.bmcmt.VCGenerator
 import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
@@ -19,7 +20,7 @@ class VCGenPassImpl @Inject() (options: PassOptions, tracker: TransformationTrac
 
   override def name: String = "VCGen"
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     val newModule =
       options.get[List[String]]("checker", "inv") match {
         case Some(invariants) =>
@@ -38,7 +39,7 @@ class VCGenPassImpl @Inject() (options: PassOptions, tracker: TransformationTrac
 
     writeOut(writerFactory, newModule)
 
-    Some(newModule)
+    Right(newModule)
   }
 
   override def dependencies = Set(ModuleProperty.Inlined)
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala
index b8dcf4ed1a..d1b83f49a8 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/passes/SanyParserPassImpl.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.tla.imp.passes
 
+import at.forsyte.apalache.infra.ExitCodes
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.io.annotations.store._
 import at.forsyte.apalache.io.json.impl.{DefaultTagReader, UJsonRep, UJsonToTla}
@@ -28,53 +30,48 @@ class SanyParserPassImpl @Inject() (
 
   override def name: String = "SanyParser"
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
-    var rootModule: Option[TlaModule] = None
-
+  override def execute(module: TlaModule): PassResult = {
     val filename = options.getOrError[String]("parser", "filename")
-    if (filename.endsWith(".json")) {
+    var rootModule: TlaModule = if (filename.endsWith(".json")) {
       try {
         val moduleJson = UJsonRep(ujson.read(new File(filename)))
         val modules = new UJsonToTla(Some(sourceStore))(DefaultTagReader).fromRoot(moduleJson)
-        rootModule = modules match {
-          case rMod +: Nil => Some(rMod)
-          case _           => None
+        modules match {
+          case rMod +: Nil => rMod
+          case _ => {
+            logger.error("  > Error parsing file " + filename)
+            return Left(ExitCodes.ERROR_SPEC_PARSE)
+          }
         }
       } catch {
         case e: Exception =>
+          logger.error("  > Error parsing file " + filename)
           logger.error("  > " + e.getMessage)
-          rootModule = None
+          return Left(ExitCodes.ERROR_SPEC_PARSE)
       }
     } else {
       val (rootName, modules) =
         new SanyImporter(sourceStore, annotationStore)
           .loadFromFile(new File(filename))
-      rootModule = modules.get(rootName)
+      modules.get(rootName).get
     }
-    rootModule match {
-      case None =>
-        logger.error("  > Error parsing file " + filename)
-        None
 
-      case Some(mod) =>
-        // In rare cases, declarations may be out of order, as a result of substitution. Reorder them.
-        rootModule =
-          try {
-            Some(DeclarationSorter.instance(mod))
-          } catch {
-            case e: CyclicDependencyError =>
-              // re-throw the error for the nice error message
-              throw new SanyImporterException(e.getMessage)
-          }
+    rootModule =
+      try {
+        DeclarationSorter.instance(rootModule)
+      } catch {
+        case e: CyclicDependencyError =>
+          // re-throw the error for the nice error message
+          throw new SanyImporterException(e.getMessage)
+      }
 
-        // save the output
-        writeOut(writerFactory, rootModule.get)
+    // save the output
+    writeOut(writerFactory, rootModule)
 
-        // write parser output to specified destination, if requested
-        utils.writeToOutput(rootModule.get, options, writerFactory, logger, sourceStore)
+    // write parser output to specified destination, if requested
+    utils.writeToOutput(rootModule, options, writerFactory, logger, sourceStore)
 
-        rootModule
-    }
+    Right(rootModule)
   }
 
   override def dependencies = Set()
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala
index a0200cc098..1b34c7d265 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ConfigurationPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.{PassOptions, WriteablePassOptions}
 import at.forsyte.apalache.io.ConfigurationError
 import at.forsyte.apalache.io.lir.TlaWriterFactory
@@ -36,7 +37,7 @@ class ConfigurationPassImpl @Inject() (
 
   override def name: String = "ConfigurationPass"
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     // Since this is the 1st pass after Inline, check absence of recursion first
     LanguageWatchdog(NonrecursiveLanguagePred).check(tlaModule)
 
@@ -70,7 +71,7 @@ class ConfigurationPassImpl @Inject() (
     // dump the configuration result
     writeOut(writerFactory, configuredModule)
 
-    Some(configuredModule)
+    Right(configuredModule)
   }
 
   // Returns new declarations, where CInit has been extended (or constructed)
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala
index 51f6f1d3c2..a3be1023dc 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/DesugarerPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.lir.{ModuleProperty, TlaModule}
 import at.forsyte.apalache.io.lir.TlaWriterFactory
@@ -28,7 +29,7 @@ class DesugarerPassImpl @Inject() (
 
   override def name: String = "DesugarerPass"
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     logger.info("  > Desugaring...")
     val input = tlaModule
     val varNames = input.varDeclarations.map {
@@ -38,7 +39,7 @@ class DesugarerPassImpl @Inject() (
 
     // dump the result of preprocessing
     writeOut(writerFactory, output)
-    Some(output)
+    Right(output)
   }
 
   override def dependencies = Set(ModuleProperty.TypeChecked)
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala
index be74cd0738..2d034c904c 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/InlinePassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.io.lir.TlaWriterFactory
 import at.forsyte.apalache.tla.imp.findBodyOf
@@ -22,7 +23,7 @@ class InlinePassImpl @Inject() (
 
   override def name: String = "InlinePass"
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
+  override def execute(module: TlaModule): PassResult = {
     // Since PrimingPass now happens before inlining, we have to add InitPrime and CInitPrime as well
     val initName = options.getOrElse[String]("checker", "init", "Init")
     val cinitName = options.getOrElse[String]("checker", "cinit", "CInit")
@@ -71,7 +72,7 @@ class InlinePassImpl @Inject() (
     // dump the result of preprocessing
     writeOut(writerFactory, constInlinedModule)
 
-    Some(constInlinedModule)
+    Right(constInlinedModule)
   }
 
   override def dependencies = Set()
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala
index fd0a01f8a7..7d02839a91 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/OptPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.io.lir.TlaWriterFactory
 import at.forsyte.apalache.tla.lir.transformations.TransformationTracker
@@ -30,7 +31,7 @@ class OptPassImpl @Inject() (
 
   override def name: String = "OptimizationPass"
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
+  override def execute(module: TlaModule): PassResult = {
     val transformationSequence =
       List(
           ConstSimplifier(tracker),
@@ -48,7 +49,7 @@ class OptPassImpl @Inject() (
     // dump the result of preprocessing
     writeOut(writerFactory, optimized)
 
-    Some(optimized)
+    Right(optimized)
   }
 
   override def dependencies = Set(ModuleProperty.Preprocessed)
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala
index 1fd6a70bef..6ae73cd80f 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.io.lir.TlaWriterFactory
@@ -39,7 +40,7 @@ class PreproPassImpl @Inject() (
         writerFactory,
     ) {
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     logger.info("  > Before preprocessing: unique renaming")
     val varSet = tlaModule.varDeclarations.map(_.name).toSet
 
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassPartial.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassPartial.scala
index f80b5f4ac9..ef7d99efa1 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassPartial.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassPartial.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.ExitCodes
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.io.lir.TlaWriterFactory
 import at.forsyte.apalache.tla.imp.src.SourceStore
@@ -56,25 +58,25 @@ abstract class PreproPassPartial(
     }
   }
 
-  protected def postLanguageCheck(tlaModule: TlaModule, lPred: LanguagePred): Option[TlaModule] =
+  protected def postLanguageCheck(tlaModule: TlaModule, lPred: LanguagePred): PassResult =
     // check, whether all expressions fit in the language
     lPred.isModuleOk(tlaModule) match {
       case PredResultOk() =>
-        Some(tlaModule)
+        Right(tlaModule)
 
       case PredResultFail(failedIds) =>
         for ((id, errorMessage) <- failedIds) {
           val message = "%s: unsupported expression: %s".format(findLoc(id), errorMessage)
           logger.error(message)
         }
-        None
+        Left(ExitCodes.FAILURE_SPEC_EVAL)
     }
 
   protected def executeWithParams(
       tlaModule: TlaModule,
       transformationSequence: List[(String, TlaModuleTransformation)],
       postRename: Boolean,
-      lPred: LanguagePred): Option[TlaModule] = {
+      lPred: LanguagePred): PassResult = {
     val afterModule = applyTx(tlaModule, transformationSequence, postRename)
 
     checkLocations(tlaModule)
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ReTLAPreproPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ReTLAPreproPassImpl.scala
index 20281ed9dd..a1db327739 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ReTLAPreproPassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/ReTLAPreproPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.io.lir.TlaWriterFactory
@@ -29,7 +30,7 @@ class ReTLAPreproPassImpl @Inject() (
         writerFactory,
     ) {
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     val varSet = tlaModule.varDeclarations.map(_.name).toSet
 
     val transformationSequence: List[(String, TlaModuleTransformation)] =
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/WatchdogPassImpl.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/WatchdogPassImpl.scala
index c1e5234d9e..018c58f457 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/WatchdogPassImpl.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/WatchdogPassImpl.scala
@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.pp.passes
 
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.tla.lir.transformations.{LanguagePred, LanguageWatchdog}
 import at.forsyte.apalache.tla.lir.TlaModule
@@ -11,11 +12,11 @@ class WatchdogPassImpl @Inject() (val options: PassOptions, val pred: LanguagePr
 
   override def name: String = "WatchdogPass"
 
-  override def execute(module: TlaModule): Option[TlaModule] = {
+  override def execute(module: TlaModule): PassResult = {
     // Only call the watchdog, then return true, don't change the module in any way
     LanguageWatchdog(pred).check(module)
 
-    Some(module)
+    Right(module)
   }
 
   override def dependencies = Set()
diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
index 5e36366c7e..acf40624fc 100644
--- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
+++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/passes/EtcTypeCheckerPassImpl.scala
@@ -1,5 +1,7 @@
 package at.forsyte.apalache.tla.typecheck.passes
 
+import at.forsyte.apalache.infra.ExitCodes
+import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.infra.passes.PassOptions
 import at.forsyte.apalache.io.annotations.store.AnnotationStore
 import at.forsyte.apalache.tla.imp.src.SourceStore
@@ -28,7 +30,7 @@ class EtcTypeCheckerPassImpl @Inject() (
 
   override def name: String = "TypeCheckerSnowcat"
 
-  override def execute(tlaModule: TlaModule): Option[TlaModule] = {
+  override def execute(tlaModule: TlaModule): PassResult = {
     logger.info(" > Running Snowcat .::.")
 
     val tool = new TypeCheckerTool(annotationStore, inferPoly, useRows)
@@ -55,10 +57,10 @@ class EtcTypeCheckerPassImpl @Inject() (
 
         utils.writeToOutput(newModule, options, writerFactory, logger, sourceStore)
 
-        Some(newModule)
+        Right(newModule)
       case None =>
         logger.info(" > Snowcat asks you to fix the types. Meow.")
-        None
+        Left(ExitCodes.ERROR_TYPECHECK)
     }
   }
 

From 840ac2fd61bc12657db897bd82dba28728f747dc Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas@informal.systems>
Date: Fri, 13 May 2022 11:57:41 +0200
Subject: [PATCH 3/4] Update integration tests

---
 test/tla/cli-integration-tests.md | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index 4902d1f9a8..144f165297 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -1346,7 +1346,7 @@ $ apalache-mc typecheck --features=rows Bug914.tla | sed 's/[IE]@.*//'
 [Bug914.tla:21:9-21:26]: Arguments to = should have the same type. For arguments m, ["foo" ↦ TRUE] with types {  }, { foo: Bool }, in expression m = (["foo" ↦ TRUE])
 [Bug914.tla:21:1-21:26]: Error when computing the type of Init
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ### check RecordExcept987 succeeds
@@ -1381,7 +1381,7 @@ $ apalache-mc check Bug1126.tla | sed 's/[IE]@.*//'
 ...
 Bug1126.tla:15:14-15:27: unsupported expression: Seq(_) produces an infinite set of unbounded sequences. See: https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs
 ...
-EXITCODE: ERROR (12)
+EXITCODE: ERROR (75)
 ```
 
 ### check SetSndRcv succeeds (array-encoding)
@@ -1509,7 +1509,7 @@ $ apalache-mc check --config=Config1.cfg Config.tla | sed 's/[IEW]@.*//'
 ...
 Config.tla:58:5-58:14: unsupported expression: ♢(x > 10)
 ...
-EXITCODE: ERROR (12)
+EXITCODE: ERROR (75)
 ```
 
 ### configure via TLC config and override it via CLI
@@ -1525,7 +1525,7 @@ $ apalache-mc check --config=Config1.cfg --init=Init2 --next=Next2 Config.tla |
 ...
 Config.tla:58:5-58:14: unsupported expression: ♢(x > 10)
 ...
-EXITCODE: ERROR (12)
+EXITCODE: ERROR (75)
 ```
 
 ### configure missing property in TLC config
@@ -1832,7 +1832,7 @@ $ apalache-mc typecheck --features=rows Bug874.tla | sed 's/[IEW]@.*//'
 ...
 [Bug874.tla:4:17-4:27]: Cannot apply ["a" ↦ 2] to the argument "b" in (["a" ↦ 2])["b"].
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ### check letpoly.tla
@@ -1934,7 +1934,7 @@ Test that model values of different sorts are incomparable
 ```sh
 $ apalache-mc check --cinit=CInit --inv=Inv ModelValFail.tla | sed 's/[IEW]@.*//'
 ...
-EXITCODE: ERROR (12)
+EXITCODE: ERROR (120)
 ```
 
 ### check MC3_TwoPhaseUFO.tla succeeds with model values
@@ -2094,7 +2094,7 @@ $ apalache-mc check --length=0 --inv=AllTests TestFolds.tla | sed 's/[IEW]@.*//'
 ...
 TestFolds.tla:21:5-21:50: unsupported expression: Not supported: MapThenFoldSet. Use FoldSet, FoldSeq, FoldFunction.
 ...
-EXITCODE: ERROR (12)
+EXITCODE: ERROR (75)
 ```
 
 ### check Test1343.tla reports no error
@@ -2654,7 +2654,7 @@ $ apalache-mc typecheck --features=rows Bug925.tla | sed 's/[IEW]@.*//'
 ...
 [Bug925.tla:7:1-7:24]: Error when computing the type of Optional
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ### typecheck letpoly.tla
@@ -2806,7 +2806,7 @@ No ill-typed record access.
 ```sh
 $ apalache-mc typecheck --features=rows TestRecordsNewIll1.tla | sed 's/[IEW]@.*//'
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ### typecheck TestRecordsNewIll2.tla
@@ -2816,7 +2816,7 @@ No ill-typed record access.
 ```sh
 $ apalache-mc typecheck --features=rows TestRecordsNewIll2.tla | sed 's/[IEW]@.*//'
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ### typecheck TestRecordsNewIll3.tla
@@ -2826,7 +2826,7 @@ No ill-typed record access.
 ```sh
 $ apalache-mc typecheck --features=rows TestRecordsNewIll3.tla | sed 's/[IEW]@.*//'
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ### typecheck TestRecordsNewIll4.tla
@@ -2836,7 +2836,7 @@ No ill-typed record access.
 ```sh
 $ apalache-mc typecheck --features=rows TestRecordsNewIll4.tla | sed 's/[IEW]@.*//'
 ...
-EXITCODE: ERROR (255)
+EXITCODE: ERROR (120)
 ```
 
 ## configuring the output manager

From 5bd325b399e51013d5edc978fd359739e83b067e Mon Sep 17 00:00:00 2001
From: Thomas Pani <thomas@informal.systems>
Date: Fri, 13 May 2022 12:12:41 +0200
Subject: [PATCH 4/4] Update release notes

Co-authored-by: Shon Feder <shon@informal.systems>
---
 UNRELEASED.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/UNRELEASED.md b/UNRELEASED.md
index 05ef6c2855..36db7f5e2d 100644
--- a/UNRELEASED.md
+++ b/UNRELEASED.md
@@ -10,6 +10,12 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Breaking changes
+
+ * Introduce dedicated exit codes for type-checking errors, parser errors, and
+   evaluation errors (e.g., due to unsupported language constructs or
+   operators), see #1749
+
 ### Features
 
- * Support sound records (over rows) in the model checker, see #1717
\ No newline at end of file
+ * Support sound records (over rows) in the model checker, see #1717