Update scalafmt-core to 3.8.4

.git-blame-ignore-revs

@@ -9,3 +9,6 @@
 
 # Scala Steward: Reformat with scalafmt 3.8.3
 60dd752b3c25a2b578b9f0a967878904d6941982
+
+# Scala Steward: Reformat with scalafmt 3.8.4
+3c482f9735e3cf539cc9a73ae299bbf5c6106c05

.scalafmt.conf

@@ -1,4 +1,4 @@
-version = "3.8.3"
+version = "3.8.4"
 
 runner.dialect = scala213
 fileOverride {

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/DerivedPredicates.scala

@@ -3,7 +3,7 @@ package at.forsyte.apalache.infra.passes
 import com.google.inject.Inject
 
 /**
- * For shared-memory communication of information about specification predicates between `Pass`es
+ * For shared-memory communication of information about specification predicates between `Pass` es
  *
  * ==Motivation==
  *

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/ToolModule.scala

@@ -6,9 +6,9 @@ import at.forsyte.apalache.infra.passes.options.OptionGroup
 /**
  * An extension of Google Guice AbstractModule to be used by apalache modules to configure pass order and options.
  *
- * `ToolModule`'s are parameterized on a [[infra.passes.options.OptionGroup OptionGroup]], which statically enforces the
- * connection between a particular sequence of passes and the set of options which are required to run those passes. In
- * the degenerate case were no options are needed for a sequnece of passes, classes can extend
+ * `ToolModule` 's are parameterized on a [[infra.passes.options.OptionGroup OptionGroup]], which statically enforces
+ * the connection between a particular sequence of passes and the set of options which are required to run those passes.
+ * In the degenerate case were no options are needed for a sequnece of passes, classes can extend
  * `ToolModule(OptionGroup.Empty())`.
  *
  * Subclasses are generally expected to reduce the upper bound on `O`, giving a more precise specification of the

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ApalacheCommand.scala

@@ -81,7 +81,7 @@ abstract class ApalacheCommand(name: String, description: String)
    *
    * All execution logic specific to the subcommand should be triggered encapsulated in the [[run]] method.
    *
-   * Most subclasses use the `PassChainExecutor` to sequence a chain of passes. `PassChainExecutor`s are created by
+   * Most subclasses use the `PassChainExecutor` to sequence a chain of passes. `PassChainExecutor` s are created by
    * providing a `ToolModule`. E.g.,
    *
    * {{{

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ServerCmd.scala

@@ -7,8 +7,7 @@ import org.backuity.clist._
 import at.forsyte.apalache.infra.passes.options.Config
 import at.forsyte.apalache.infra.passes.options.OptionGroup
 
-class ServerCmd
-    extends ApalacheCommand(name = "server", description = "Run in server mode (in early development)")
+class ServerCmd extends ApalacheCommand(name = "server", description = "Run in server mode (in early development)")
     with LazyLogging {
 
   var port = opt[Option[Int]](description = "the port served by the RPC server, default: 8822 (overrides envvar PORT)",

passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala

@@ -122,14 +122,15 @@ class ConfigurationPassImpl @Inject() (
       OperEx(TlaOper.eq, NameEx(varName)(body.typeTag), body)(boolTag)
     }
 
-    val newCinitDecl = oldCinitOpt
-      .map { d =>
-        d.copy(body = OperEx(TlaBoolOper.and, d.body +: overridesAsEql: _*)(boolTag))
-      }
-      .getOrElse {
-        TlaOperDecl(cinitName, List.empty, OperEx(TlaBoolOper.and, overridesAsEql: _*)(boolTag))(Typed(OperT1(Seq.empty,
-                    BoolT1)))
-      }
+    val newCinitDecl =
+      oldCinitOpt
+        .map { d =>
+          d.copy(body = OperEx(TlaBoolOper.and, d.body +: overridesAsEql: _*)(boolTag))
+        }
+        .getOrElse {
+          TlaOperDecl(cinitName, List.empty, OperEx(TlaBoolOper.and, overridesAsEql: _*)(boolTag))(
+              Typed(OperT1(Seq.empty, BoolT1)))
+        }
 
     // Since declarations are a Seq not a Set, we may need to remove the old CInit first
     tlaModule.declarations.filterNot(_.name == derivedPreds.cinit) :+ newCinitDecl

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala

@@ -21,6 +21,7 @@ class SmtFreeSymbolicTransitionExtractor(
 
   /** Checks whether expressions, which cannot contain assignments, use unassigned variables */
   private def throwOnUseBeforeAssignment(unassignedVars: Set[String]): TlaEx => Unit = {
+
     /** Manual assignments at such locations throw exceptions */
     case ex @ OperEx(ApalacheOper.assign, OperEx(TlaActionOper.prime, NameEx(_)), _) =>
       val locString = getLocString(ex)
@@ -75,6 +76,7 @@ class SmtFreeSymbolicTransitionExtractor(
 
   // Transition method between partial states
   private def getStrategyOptInternal(currentState: PartialState, operMap: BodyMap): TlaEx => PartialState = {
+
     /** Base case, assignment candidates */
     case ex @ OperEx(TlaOper.eq, OperEx(TlaActionOper.prime, NameEx(name)), assignmentFreeRhs) =>
       // First, check if assignmentFreeRhs contains unassigned varaible access
@@ -101,6 +103,7 @@ class SmtFreeSymbolicTransitionExtractor(
     case OperEx(TlaBoolOper.and, args @ _*) =>
       // We sequentially update the partial state
       args.foldLeft(currentState) { getStrategyOptInternal(_, operMap)(_) }
+
     /** Disjunction */
     case OperEx(TlaBoolOper.or, args @ _*) =>
       handleDisjunctionOrITE(currentState, operMap, args)

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SymbTransGenerator.scala

@@ -54,6 +54,7 @@ class SymbTransGenerator(tracker: TransformationTracker) {
      *   A mapping of the form [e.ID |-> { B \cap A | B \in Branches( e ) } | e \in Sub(ex)]
      */
     def allSelections(ex: TlaEx, letInMap: letInMapType = Map.empty): SelMapType = ex match {
+
       /** Base case, assignments */
       case e @ OperEx(ApalacheOper.assign, _, _) => Map(e.ID -> Set(Set(e.ID)))
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntArithPacker.scala

@@ -16,7 +16,7 @@ trait IntArithPacker {
   private lazy val substRule = new SubstRule
 
   /**
-   * Rewrite `state`'s expression into an expression that is purely arithmetic, referring to arena cells for
+   * Rewrite `state` 's expression into an expression that is purely arithmetic, referring to arena cells for
    * non-arithmetic subexpressions.
    *
    * @param rewriter

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala

@@ -34,6 +34,12 @@ object SolverConfig {
    * Get the default configuration.
    */
   val default: SolverConfig =
-    new SolverConfig(debug = false, profile = false, randomSeed = 0, smtEncoding = SMTEncoding.OOPSLA19,
-        z3StatsSec = 60, z3Params = Map())
+    new SolverConfig(
+        debug = false,
+        profile = false,
+        randomSeed = 0,
+        smtEncoding = SMTEncoding.OOPSLA19,
+        z3StatsSec = 60,
+        z3Params = Map(),
+    )
 }

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala

@@ -49,13 +49,13 @@ class UninterpretedLiteralCache extends Cache[PureArena, (TlaType1, String), Are
    * d2 + ... + dN` disequalities, i.e. {{{\sum_{n=1}^N n(n-1)/2 = N(N^2 -1)/6}}} In contrast, `addAllConstraints`
    * produces `dN = N(N-1)/2` disequalities, which is `O(N^2)`, instead of `O(N^3)`.
    */
-  override def addConstraintsForElem(ctx: SolverContext): (((TlaType1, String), ArenaCell)) => Unit = {
-    case ((utype, _), v) =>
-      require(utype == StrT1 || utype.isInstanceOf[ConstT1], "Type must be Str, or an uninterpreted type.")
-      val others = values().withFilter { c => c.cellType == CellTFrom(utype) && c != v }.map(_.toBuilder).toSeq
-      // The cell should differ from the previously created cells.
-      // We use the SMT constraint (distinct ...).
-      ctx.assertGroundExpr(tla.distinct(v.toBuilder +: others: _*))
+  override def addConstraintsForElem(
+      ctx: SolverContext): (((TlaType1, String), ArenaCell)) => Unit = { case ((utype, _), v) =>
+    require(utype == StrT1 || utype.isInstanceOf[ConstT1], "Type must be Str, or an uninterpreted type.")
+    val others = values().withFilter { c => c.cellType == CellTFrom(utype) && c != v }.map(_.toBuilder).toSeq
+    // The cell should differ from the previously created cells.
+    // We use the SMT constraint (distinct ...).
+    ctx.assertGroundExpr(tla.distinct(v.toBuilder +: others: _*))
   }
 
   /**

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala

@@ -12,7 +12,7 @@ import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
  *
  * For the purposes of describing the oracle's behavior, we can assume that there are `N` distinct possible values,
  * which are indexed with `0,1,2,...,N-1` (though they need not be represented as such in the implementation). We refer
- * to the `i`-th candidate value as `vi`.
+ * to the `i` -th candidate value as `vi`.
  *
  * @author
  *   Jure Kukovec
@@ -34,12 +34,12 @@ trait Oracle {
    * Produce a ground expression that contains assertions for the possible oracle values.
    *
    * The `assertions` sequence must contain `N` elements, where `N` equals the number of oracle value candidates. The
-   * `i`-th element of `assertions` describes a formula, which holds if the oracle value is equal to the `i`-th
+   * `i` -th element of `assertions` describes a formula, which holds if the oracle value is equal to the `i` -th
    * candidate value `vi`.
    *
    * Optionally, a sequence option `elseAssertionsOpt`, containing a sequence of the same length as `assertions`, may be
-   * provided. If it is, the `i`-th element of the sequence describes a formula, which holds if the oracle value is
-   * _not_ equal to the `i`-th candidate value `vi`. If this value is not provided, a default sequence, containing `N`
+   * provided. If it is, the `i` -th element of the sequence describes a formula, which holds if the oracle value is
+   * _not_ equal to the `i` -th candidate value `vi`. If this value is not provided, a default sequence, containing `N`
    * copies of `TRUE` is taken in place of the aforementioned formulas.
    */
   def caseAssertions(

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerTrait.scala

@@ -572,7 +572,13 @@ trait TestSeqModelCheckerTrait extends FixtureAnyFunSuite {
     val notInv = not(inv).typed(types, "b")
 
     val checkerInput =
-      new CheckerInput(mkModuleWithXandY(), initTrans, nextTrans, None, CheckerInputVC(List((inv, notInv))))
+      new CheckerInput(
+          mkModuleWithXandY(),
+          initTrans,
+          nextTrans,
+          None,
+          CheckerInputVC(List((inv, notInv))),
+      )
     val params = new ModelCheckerParams(checkerInput, stepsBound = 2, Map())
     // initialize the model checker
     val ctx = new IncrementalExecutionContext(rewriter)
@@ -787,7 +793,13 @@ trait TestSeqModelCheckerTrait extends FixtureAnyFunSuite {
       .typed(types, "b")
     val dummyModule = TlaModule("root", List(TlaConstDecl("N")(intTag), TlaVarDecl("x")(intTag)))
     val checkerInput =
-      new CheckerInput(dummyModule, initTrans, nextTrans, Some(cInit), CheckerInputVC(List((inv, notInv))))
+      new CheckerInput(
+          dummyModule,
+          initTrans,
+          nextTrans,
+          Some(cInit),
+          CheckerInputVC(List((inv, notInv))),
+      )
     val params = new ModelCheckerParams(checkerInput, stepsBound = 10, Map())
     // initialize the model checker
     val ctx = new IncrementalExecutionContext(rewriter)

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala

@@ -725,8 +725,13 @@ trait TestSymbStateRewriterSet extends RewriterBase {
     val setBool = enumSet(bool(false), bool(true)).as(boolSetT)
     val mapping = tuple(name("y").as(boolT)).as(parser("<<Bool>>"))
     val mappedSet =
-      map(mapping, name("x").as(intT), set12minus2.as(intSetT), name("y").as(boolT), setBool).as(
-          parser("Set(<<Bool>>)"))
+      map(
+          mapping,
+          name("x").as(intT),
+          set12minus2.as(intSetT),
+          name("y").as(boolT),
+          setBool,
+      ).as(parser("Set(<<Bool>>)"))
     val inMappedSet = in(tuple(bool(true)).typed(TupT1(BoolT1)), mappedSet)
       .typed(BoolT1)
 

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala

@@ -8,8 +8,13 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithArrays extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-        smtEncoding = SMTEncoding.Arrays)
+    solverConfig = SolverConfig(
+        debug = false,
+        profile = false,
+        randomSeed = 0,
+        z3StatsSec = 0,
+        smtEncoding = SMTEncoding.Arrays,
+    )
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala

@@ -8,8 +8,13 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithFunArrays extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-        smtEncoding = SMTEncoding.FunArrays)
+    solverConfig = SolverConfig(
+        debug = false,
+        profile = false,
+        randomSeed = 0,
+        z3StatsSec = 0,
+        smtEncoding = SMTEncoding.FunArrays,
+    )
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala

@@ -8,8 +8,13 @@ import org.scalatestplus.junit.JUnitRunner
 @RunWith(classOf[JUnitRunner])
 class TestRecordingSolverContextWithOOPSLA19 extends TestRecordingSolverContext {
   override protected def withFixture(test: NoArgTest): Outcome = {
-    solverConfig = SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-        smtEncoding = SMTEncoding.OOPSLA19)
+    solverConfig = SolverConfig(
+        debug = false,
+        profile = false,
+        randomSeed = 0,
+        z3StatsSec = 0,
+        smtEncoding = SMTEncoding.OOPSLA19,
+    )
     test()
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala

@@ -12,8 +12,13 @@ class TestTransitionExecutorWithIncrementalAndArrays
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver =
-      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-              smtEncoding = SMTEncoding.Arrays))
+      new Z3SolverContext(SolverConfig(
+              debug = false,
+              profile = false,
+              randomSeed = 0,
+              z3StatsSec = 0,
+              smtEncoding = SMTEncoding.Arrays,
+          ))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala

@@ -11,8 +11,13 @@ class TestTransitionExecutorWithIncrementalAndFunArrays
     extends TestTransitionExecutorImpl[IncrementalExecutionContextSnapshot]
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
-    val solver = new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-            smtEncoding = SMTEncoding.FunArrays))
+    val solver = new Z3SolverContext(SolverConfig(
+            debug = false,
+            profile = false,
+            randomSeed = 0,
+            z3StatsSec = 0,
+            smtEncoding = SMTEncoding.FunArrays,
+        ))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala

@@ -18,8 +18,13 @@ class TestTransitionExecutorWithIncrementalAndOOPSLA19
     with TestFilteredTransitionExecutor[IncrementalExecutionContextSnapshot] {
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver =
-      new Z3SolverContext(SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-              smtEncoding = SMTEncoding.OOPSLA19))
+      new Z3SolverContext(SolverConfig(
+              debug = false,
+              profile = false,
+              randomSeed = 0,
+              z3StatsSec = 0,
+              smtEncoding = SMTEncoding.OOPSLA19,
+          ))
     withFixtureInContext(solver, new IncrementalExecutionContext(_), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala

@@ -13,8 +13,13 @@ class TestTransitionExecutorWithOfflineAndArrays extends TestTransitionExecutorI
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
       .createZ3(None,
-          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-              smtEncoding = SMTEncoding.Arrays))
+          SolverConfig(
+              debug = false,
+              profile = false,
+              randomSeed = 0,
+              z3StatsSec = 0,
+              smtEncoding = SMTEncoding.Arrays,
+          ))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala

@@ -14,8 +14,13 @@ class TestTransitionExecutorWithOfflineAndFunArrays
   override protected def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
       .createZ3(None,
-          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-              smtEncoding = SMTEncoding.FunArrays))
+          SolverConfig(
+              debug = false,
+              profile = false,
+              randomSeed = 0,
+              z3StatsSec = 0,
+              smtEncoding = SMTEncoding.FunArrays,
+          ))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala

@@ -19,8 +19,13 @@ class TestTransitionExecutorWithOfflineAndOOPSLA19 extends TestTransitionExecuto
   override def withFixture(test: OneArgTest): Outcome = {
     val solver = RecordingSolverContext
       .createZ3(None,
-          SolverConfig(debug = false, profile = false, randomSeed = 0, z3StatsSec = 0,
-              smtEncoding = SMTEncoding.OOPSLA19))
+          SolverConfig(
+              debug = false,
+              profile = false,
+              randomSeed = 0,
+              z3StatsSec = 0,
+              smtEncoding = SMTEncoding.OOPSLA19,
+          ))
     withFixtureInContext(solver, new OfflineExecutionContext(_, new IncrementalRenaming(new IdleTracker)), test)
   }
 }

tla-io/src/main/scala/at/forsyte/apalache/io/annotations/Annotation.scala

@@ -12,8 +12,8 @@ case class Annotation(name: String, args: AnnotationArg*) {
   /**
    * <p>A string representation of the annotation. There are two cases:</p>
    *
-   * <ol> <li>The annotation `name` has zero arguments. The output is `@name`</li> <li>The annotation `name` has N > 0
-   * arguments `arg1`, ..., `argN`. The output is `@name(arg1, ..., argN)`</li> </ol>
+   * <ol> <li>The annotation `name` has zero arguments. The output is `@name` </li> <li>The annotation `name` has N > 0
+   * arguments `arg1`, ..., `argN`. The output is `@name(arg1, ..., argN)` </li> </ol>
    *
    * @return
    *   the string representation of the annotation.

tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala

@@ -3,7 +3,7 @@ package at.forsyte.apalache.io.lir
 import at.forsyte.apalache.tla.lir.{TlaDecl, TlaEx, TlaModule}
 
 /**
- * <p>An abstract writer of TLA+ expressions. For an example, see `PrettyWriter`.</p>
+ * <p>An abstract writer of TLA+ expressions. For an example, see `PrettyWriter`. </p>
  *
  * <p>Igor: We should refactor the writers' architecture. Use the Writer monad?</p>
  */

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala

@@ -51,7 +51,7 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr
    *   - sets of records over type-defining field types, e.g., [type: STRING, val: Int], ...
    *
    * In particular, `Nat` is not type-defining, nor are sequence sets / power sets thereof, since `i \in Nat` does not
-   * hold for all `IntT1`-typed `i`.
+   * hold for all `IntT1` -typed `i`.
    */
   private def isTypeDefining: Function[TlaEx, Boolean] = {
     // base case: BOOLEAN, Int, Real, STRING