Merge branch 'main' into jk/stratifiedRules

.git-blame-ignore-revs

@@ -3,3 +3,6 @@
 
 # Scala Steward: Reformat with scalafmt 3.7.0
 940cde8dd83d26a64657982c4b59ec1de2df94e4
+
+# Scala Steward: Reformat with scalafmt 3.7.6
+1b2091c13571348b534076f2183ced2cd2ff67a9

.scalafmt.conf

@@ -1,4 +1,4 @@
-version = "3.7.4"
+version = "3.7.6"
 
 runner.dialect = scala213
 fileOverride {

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/profiler/RuleStatLocator.scala

@@ -5,8 +5,8 @@ import at.forsyte.apalache.io.OutputManager
 import scala.collection.immutable.SortedMap
 
 /**
- * The locator keeps a registry of RuleStat instances
- * -- one per rule name -- and finds the required instances when needed.
+ * The locator keeps a registry of RuleStat instances -- one per rule name -- and finds the required instances when
+ * needed.
  *
  * @author
  *   Igor Konnov

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

@@ -454,7 +454,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase {
     val rewriter = create(rewriterType)
     rewriter.rewriteUntilDone(state)
     assert(rewriter.solverContext.sat())
-  // there is not much to check here, since it is just a function that returns an integer
+    // there is not much to check here, since it is just a function that returns an integer
   }
 
   // the model checker will never meet such an expression, as it will be optimized into several existentials by ExprOptimizer

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

@@ -68,9 +68,9 @@ trait TestSymbStateRewriterChooseOrGuess extends RewriterBase {
     rewriter.rewriteUntilDone(state)
     // the buggy implementation of choose fails on a dynamically empty set
     assert(solverContext.sat())
-  // The semantics of choose does not restrict the outcome on the empty sets,
-  // so we do not test for anything here. Our previous implementation of CHOOSE produced default values in this case,
-  // but this happened to be error-prone and sometimes conflicting with other rules. So, no default values.
+    // The semantics of choose does not restrict the outcome on the empty sets,
+    // so we do not test for anything here. Our previous implementation of CHOOSE produced default values in this case,
+    // but this happened to be error-prone and sometimes conflicting with other rules. So, no default values.
   }
 
   test("""CHOOSE x \in {}: x > 1""") { rewriterType: SMTEncoding =>

tla-io/src/test/scala/at/forsyte/apalache/io/annotations/TestAnnotationParser.scala

@@ -180,7 +180,7 @@ class TestAnnotationParser extends AnyFunSuite with Checkers {
             // To see how testing is different from verification,
             // replace 'passed' with 'falsified' and observe that no error will be found ;-)
             passed
-          // no exceptions
+            // no exceptions
           }
         },
         minSuccessful(300),

tla-io/src/test/scala/at/forsyte/apalache/io/annotations/TestCommentPreprocessor.scala

@@ -166,7 +166,7 @@ class TestCommentPreprocessor extends AnyFunSuite with Checkers with Matchers {
         {
           forAll(asciiStr) { str =>
             hasAnnotationsWhenNonEmpty(str)
-          // no exceptions
+            // no exceptions
           }
         },
         minSuccessful(300),

tla-typechecker/src/test/scala/at/forsyte/apalache/tla/typecheck/TestDefaultType1Parser.scala

@@ -378,7 +378,7 @@ class TestDefaultType1Parser extends AnyFunSuite with Checkers with TlaType1Gen
               case _: Throwable =>
                 falsified
             }
-          // no exceptions
+            // no exceptions
           }
         }, minSuccessful(300))
   }