Merge pull request #3069 from scala-steward/update/scalafmt-core-3.8.5

Update scalafmt-core to 3.8.5

Author: konnov

.git-blame-ignore-revs

@@ -9,3 +9,6 @@
 
 # Scala Steward: Reformat with scalafmt 3.8.3
 60dd752b3c25a2b578b9f0a967878904d6941982
+
+# Scala Steward: Reformat with scalafmt 3.8.5
+11a37745e7051f1346f84101f9b9b4bd9e5dec32

.scalafmt.conf

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

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/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/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)
   }
 }

tlair/src/main/scala/at/forsyte/apalache/tla/lir/smt/SmtTools.scala

@@ -59,6 +59,7 @@ object SmtTools {
    */
   def simplify(phi: BoolFormula): BoolFormula = {
     phi match {
+
       /**
        * Recursively simplify branches first. If any branch is false, the whole formula is false. It is important to
        * recurse first, since otherwise false-simplification would not propagate upward.