From 9ce4db95c8624dbc29d325c445b873c6b6a38c6d Mon Sep 17 00:00:00 2001 From: Scala Steward Date: Tue, 14 Jan 2025 14:27:01 +0000 Subject: [PATCH 1/3] Update scalafmt-core to 3.8.4 --- .scalafmt.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.scalafmt.conf b/.scalafmt.conf index 2f274e9290..03a23702a0 100644 --- a/.scalafmt.conf +++ b/.scalafmt.conf @@ -1,4 +1,4 @@ -version = "3.8.3" +version = "3.8.4" runner.dialect = scala213 fileOverride { From 3c482f9735e3cf539cc9a73ae299bbf5c6106c05 Mon Sep 17 00:00:00 2001 From: Scala Steward Date: Tue, 14 Jan 2025 14:28:21 +0000 Subject: [PATCH 2/3] Reformat with scalafmt 3.8.4 Executed command: scalafmt --non-interactive --- .../infra/passes/DerivedPredicates.scala | 2 +- .../apalache/infra/passes/ToolModule.scala | 6 +++--- .../tla/tooling/opt/ApalacheCommand.scala | 2 +- .../apalache/tla/tooling/opt/ServerCmd.scala | 3 +-- .../tla/passes/pp/ConfigurationPassImpl.scala | 17 +++++++++-------- .../SmtFreeSymbolicTransitionExtractor.scala | 3 +++ .../tla/assignments/SymbTransGenerator.scala | 1 + .../tla/bmcmt/rules/IntArithPacker.scala | 2 +- .../apalache/tla/bmcmt/smt/SolverConfig.scala | 10 ++++++++-- .../aux/caches/UninterpretedLiteralCache.scala | 14 +++++++------- .../stratifiedRules/aux/oracles/Oracle.scala | 8 ++++---- .../tla/bmcmt/TestSeqModelCheckerTrait.scala | 16 ++++++++++++++-- .../tla/bmcmt/TestSymbStateRewriterSet.scala | 9 +++++++-- .../TestRecordingSolverContextWithArrays.scala | 9 +++++++-- ...estRecordingSolverContextWithFunArrays.scala | 9 +++++++-- ...TestRecordingSolverContextWithOOPSLA19.scala | 9 +++++++-- ...sitionExecutorWithIncrementalAndArrays.scala | 9 +++++++-- ...ionExecutorWithIncrementalAndFunArrays.scala | 9 +++++++-- ...tionExecutorWithIncrementalAndOOPSLA19.scala | 9 +++++++-- ...TransitionExecutorWithOfflineAndArrays.scala | 9 +++++++-- ...nsitionExecutorWithOfflineAndFunArrays.scala | 9 +++++++-- ...ansitionExecutorWithOfflineAndOOPSLA19.scala | 9 +++++++-- .../apalache/io/annotations/Annotation.scala | 4 ++-- .../at/forsyte/apalache/io/lir/TlaWriter.scala | 2 +- .../tla/pp/SetMembershipSimplifier.scala | 2 +- .../apalache/tla/lir/oper/ApalacheOper.scala | 2 +- .../apalache/tla/lir/oper/TlaFunOper.scala | 2 +- .../forsyte/apalache/tla/lir/smt/SmtTools.scala | 1 + .../impl/TrackerWithListeners.scala | 2 +- .../at/forsyte/apalache/tla/types/package.scala | 6 +++--- 30 files changed, 134 insertions(+), 61 deletions(-) diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/DerivedPredicates.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/DerivedPredicates.scala index 07c4306bd8..2ef1c4c4ba 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/DerivedPredicates.scala +++ b/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== * diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/ToolModule.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/ToolModule.scala index f4193b1565..eeaf1d22c4 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/ToolModule.scala +++ b/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 diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ApalacheCommand.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ApalacheCommand.scala index ad4dc90e85..c7ff60db5c 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ApalacheCommand.scala +++ b/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., * * {{{ diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ServerCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ServerCmd.scala index fbcd2af272..b2011e0269 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ServerCmd.scala +++ b/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)", diff --git a/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala b/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala index 42faa998a8..cc8a7fa991 100644 --- a/passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala +++ b/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 diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala index fe61cd1edb..ace40c5580 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala +++ b/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) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SymbTransGenerator.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SymbTransGenerator.scala index 29bb6eaabe..c1ebea8121 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SymbTransGenerator.scala +++ b/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))) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntArithPacker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntArithPacker.scala index 61125b8b72..7d582d8a7d 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntArithPacker.scala +++ b/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 diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala index fcd282e5c9..43bf6fcc51 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/SolverConfig.scala +++ b/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(), + ) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala index 6a62339b86..b026f67020 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala +++ b/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: _*)) } /** diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala index 74238f4c78..3ce908a86a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala +++ b/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( diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerTrait.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerTrait.scala index c66cfe9d8c..4976a5523a 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSeqModelCheckerTrait.scala +++ b/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) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala index e10248aa6b..1d56419c29 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterSet.scala +++ b/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("<>")) val mappedSet = - map(mapping, name("x").as(intT), set12minus2.as(intSetT), name("y").as(boolT), setBool).as( - parser("Set(<>)")) + map( + mapping, + name("x").as(intT), + set12minus2.as(intSetT), + name("y").as(boolT), + setBool, + ).as(parser("Set(<>)")) val inMappedSet = in(tuple(bool(true)).typed(TupT1(BoolT1)), mappedSet) .typed(BoolT1) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala index ba43176647..7cbff5338b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithArrays.scala +++ b/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() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala index 9463feb097..93130e695c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithFunArrays.scala +++ b/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() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala index b5dd9265b3..b61de67556 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContextWithOOPSLA19.scala +++ b/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() } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala index 4a0401caac..2f7043a3bf 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndArrays.scala +++ b/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) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala index dca20cf4fe..868d6b7788 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndFunArrays.scala +++ b/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) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala index 3cb658ab3d..6aceb2d003 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithIncrementalAndOOPSLA19.scala +++ b/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) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala index b4df42ad9d..7f18e812e6 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndArrays.scala +++ b/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) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala index e4dec6e82c..3dd52d3b26 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndFunArrays.scala +++ b/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) } } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala index 1ff9ad4d81..491dc58115 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorWithOfflineAndOOPSLA19.scala +++ b/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) } } diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/Annotation.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/Annotation.scala index 19993fff01..1028c96b9b 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/Annotation.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/Annotation.scala @@ -12,8 +12,8 @@ case class Annotation(name: String, args: AnnotationArg*) { /** *

A string representation of the annotation. There are two cases:

* - *
  1. The annotation `name` has zero arguments. The output is `@name`
  2. The annotation `name` has N > 0 - * arguments `arg1`, ..., `argN`. The output is `@name(arg1, ..., argN)`
+ *
  1. The annotation `name` has zero arguments. The output is `@name`
  2. The annotation `name` has N > 0 + * arguments `arg1`, ..., `argN`. The output is `@name(arg1, ..., argN)`
* * @return * the string representation of the annotation. diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala index b1f4a3f995..6fd6572594 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala +++ b/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} /** - *

An abstract writer of TLA+ expressions. For an example, see `PrettyWriter`.

+ *

An abstract writer of TLA+ expressions. For an example, see `PrettyWriter`.

* *

Igor: We should refactor the writers' architecture. Use the Writer monad?

*/ diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index 118d33d251..8c0b50d8ec 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/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 diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala index f17344c907..09fefd3d97 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala @@ -188,7 +188,7 @@ object ApalacheOper { * key \in Dom |-> CHOOSE value \in Rng: <<key, value>> \in R ] * *

Note that the relation `R` may be ambiguous in the sense that the same key has more than one value. In this - * case, the Apalache encodings choose one of the values, which corresponds to `CHOOSE`.

+ * case, the Apalache encodings choose one of the values, which corresponds to `CHOOSE`.

*/ object setAsFun extends ApalacheOper { override def name: String = "Apalache!SetAsFun" diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala index 396b9f653a..dee48c3134 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/TlaFunOper.scala @@ -86,7 +86,7 @@ object TlaFunOper { * been defined before. That is why we keep function definitions intermingled with operator definitions. Moreover, we * do not refer to the function name in its body, as otherwise, we would run in two problems: (1) the operator name * would clash with the function name, an (2) the renaming transformations would try to rename the function. TLA+ - * forbids mutually recursive functions, so it is sound to refer to the function with the operator `recFunDef`.

+ * forbids mutually recursive functions, so it is sound to refer to the function with the operator `recFunDef`.

* *

Example. `Fact[n \in Int] == IF n <= 1 THEN 1 ELSE n * Fact[n - 1]` is translated into:

* diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/smt/SmtTools.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/smt/SmtTools.scala index c3d0718b5e..6144e609ab 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/smt/SmtTools.scala +++ b/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. diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl/TrackerWithListeners.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl/TrackerWithListeners.scala index df58980349..65409791ba 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl/TrackerWithListeners.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl/TrackerWithListeners.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.lir.TlaOperDecl import at.forsyte.apalache.tla.lir.transformations._ /** - *

TrackerWithListeners tracks a transformation by executing all of its `listeners`' onTransformation, whenever the + *

TrackerWithListeners tracks a transformation by executing all of its `listeners` ' onTransformation, whenever the * tracked transformation is executed.

* *

For any input x, track(t)(x) and t(x) are equal.

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala index d39d3a411e..23ee3e0825 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala @@ -38,8 +38,8 @@ import at.forsyte.apalache.tla.lir.TlaEx * val tlaEx = v.build * }}} * Here, `build` is an implicit `TBuilderInstruction => TlaEx` conversion defined in [[typecomp]]. The same package - * defines an implicit class, with a `_.build` method, so `build` may be used as a suffix-call to - * `TBuilderInstruction`s. These implicits get imported alongside [[tla]] with + * defines an implicit class, with a `_.build` method, so `build` may be used as a suffix-call to `TBuilderInstruction` + * s. These implicits get imported alongside [[tla]] with * {{{ * import at.forsyte.apalache.tla.types._ * }}} @@ -96,7 +96,7 @@ import at.forsyte.apalache.tla.lir.TlaEx * *
  • `IllegalArgumentException`: This exception indicates that one or more arguments has an illegal shape, w.r.t. the * operator, or that the number of arguments is incorrect. Some operators require e.g. `ValEx(TlaStr(_))` values - * specifically, instead of just `Str`-typed values (for instance keys in + * specifically, instead of just `Str` -typed values (for instance keys in * [[typecomp.ScopedBuilder.rec the record constructor]]). Other operators are variadic, but require the number of * arguments to be of a specific parity (e.g. [[typecomp.ScopedBuilder.funDefMixed funDefMixed]]), or require a positive * number of arguments (e.g. [[typecomp.ScopedBuilder.enumSet enumSet]]). Example: From 12c16f3ba8623be63656dc1b5f370353473cfc4e Mon Sep 17 00:00:00 2001 From: Scala Steward Date: Tue, 14 Jan 2025 14:28:21 +0000 Subject: [PATCH 3/3] Add 'Reformat with scalafmt 3.8.4' to .git-blame-ignore-revs --- .git-blame-ignore-revs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index 71e9c75789..db30cdcb37 100644 --- a/.git-blame-ignore-revs +++ b/.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