tlaplus · FedericoPonzi · Mar 9, 2026 · Mar 8, 2026 · Mar 9, 2026
diff --git a/TESTING.md b/TESTING.md
@@ -10,39 +10,6 @@ Individual component tests located in `src/test/java/me/fponzi/tlaplusformatter/
 ### Integration Tests  
 End-to-end tests that format complete TLA+ specifications and compare against expected outputs in `src/test/resources/`.
 
-### Property-Based Tests
-Automated tests using [jqwik](https://jqwik.net/) that generate hundreds of random TLA+ specifications to verify formatter correctness.
-
-## Property-Based Testing
-
-The `PropertyBasedFormatterTest` class uses property-based testing to automatically verify formatter behavior across a wide range of inputs. Property-based testing generates random test data and verifies that certain properties always hold, making it excellent for finding edge cases that manual testing might miss.
-
-The implementation generates syntactically valid TLA+ specifications with:
-- Random module names  
-- 0-3 constant declarations
-- Simple operator definitions using the declared constants
-
-Two critical properties are tested:
-
-**Semantic Preservation**: The formatter must preserve the meaning of the code. This is verified by parsing both the original and formatted specifications into Abstract Syntax Trees (ASTs) and ensuring they are structurally identical.
-
-**Idempotence**: Running the formatter multiple times should produce the same result. This ensures the formatter reaches a stable state and doesn't continuously modify the code.
-
-### Running Property-Based Tests
-
-```bash
-# Run all property-based tests (1000 examples each by default)
-./gradlew test --tests PropertyBasedFormatterTest
-
-# Run with specific seed for reproducible results
-./gradlew test --tests PropertyBasedFormatterTest -Djqwik.seeds=123456789
-
-# Run all tests
-./gradlew test
-```
-
-The property-based tests automatically run 1000 random examples by default and include edge case testing, providing comprehensive coverage with minimal test code.
-
 ## Running Tests
 
 ```bash

diff --git a/build.gradle.kts b/build.gradle.kts
@@ -1,7 +1,7 @@
 plugins {
     id("java")
     id("io.ktor.plugin") version "2.3.12"
-    id("com.github.spotbugs") version "6.0.7"
+    id("com.github.spotbugs") version "6.1.3"
     jacoco
 }
 
@@ -16,28 +16,20 @@ java {
 repositories {
     mavenLocal()
     mavenCentral()
-    // Add the repository for the snapshot dependency
+    // Snapshot repository for org.lamport:tla2tools
     maven {
-        url = uri("https://oss.sonatype.org/content/repositories/snapshots/")
-    }
-    maven {
-        url = uri("https://jitpack.io")
+        url = uri("https://central.sonatype.com/repository/maven-snapshots/")
     }
 }
 
 dependencies {
-    // TODO: Replace with a stable release when available:
-    implementation("com.github.FedericoPonzi:tlaplus:0d86214464")
+    implementation("org.lamport:tla2tools:1.8.0-SNAPSHOT")
     implementation("commons-io:commons-io:2.16.1")
-    testImplementation("com.github.FedericoPonzi:tlaplus-smith:f5a70e21d1") {
-        isChanging = true
-    }
 
     testImplementation(platform("org.junit:junit-bom:5.10.0"))
     testImplementation("org.junit.jupiter:junit-jupiter")
     testImplementation("org.mockito:mockito-core:5.7.0")
     testImplementation("org.mockito:mockito-junit-jupiter:5.7.0")
-    testImplementation("net.jqwik:jqwik:1.8.0")
     implementation("commons-cli:commons-cli:1.8.0")
 
     // Logging

diff --git a/src/main/java/me/fponzi/tlaplusformatter/constructs/impl/OperatorConstruct.java b/src/main/java/me/fponzi/tlaplusformatter/constructs/impl/OperatorConstruct.java
@@ -42,6 +42,19 @@ public Doc buildDoc(TreeNode node, ConstructContext context, int indentSize) {
 
         var name = context.buildChild(o[0]);
         var exprNode = context.buildChild(o[2]);
+
+        int exprKind = o[2].getKind();
+        boolean isConjDisjList = exprKind == NodeKind.CONJ_LIST.getId()
+                || exprKind == NodeKind.DISJ_LIST.getId();
+
+        if (isConjDisjList) {
+            // Always break after == for conjunction/disjunction lists
+            return qualifier.append(name
+                    .appendSpace(Doc.text("=="))
+                    .append(Doc.line().append(exprNode)
+                            .indent(indentSize)));
+        }
+
         return qualifier.append(name
                 .appendSpace(Doc.text("=="))
                 .append(Doc

diff --git a/src/test/java/me/fponzi/tlaplusformatter/PropertyBasedFormatterTest.java b/src/test/java/me/fponzi/tlaplusformatter/PropertyBasedFormatterTest.java
diff --git a/src/test/java/me/fponzi/tlaplusformatter/constructs/impl/OperatorConstructTest.java b/src/test/java/me/fponzi/tlaplusformatter/constructs/impl/OperatorConstructTest.java
@@ -73,4 +73,44 @@ void testMixedLocalAndNonLocal() {
                 "====\n";
         Utils.assertSpecUnchanged(spec);
     }
+
+    @Test
+    void testConjListBodyBreaksAfterEquals() {
+        String input = "---- MODULE Spec ----\n" +
+                "CONSTANTS a, b\n" +
+                "TypeInv == /\\ a = 1\n" +
+                "           /\\ b = 2\n" +
+                "====\n";
+        String expected = "---- MODULE Spec ----\n" +
+                "CONSTANTS a, b\n" +
+                "TypeInv ==\n" +
+                "  /\\ a = 1\n" +
+                "  /\\ b = 2\n" +
+                "====\n";
+        Utils.assertSpecEquals(expected, input);
+    }
+
+    @Test
+    void testDisjListBodyBreaksAfterEquals() {
+        String input = "---- MODULE Spec ----\n" +
+                "CONSTANTS a, b\n" +
+                "Next == \\/ a = 1\n" +
+                "        \\/ b = 2\n" +
+                "====\n";
+        String expected = "---- MODULE Spec ----\n" +
+                "CONSTANTS a, b\n" +
+                "Next ==\n" +
+                "  \\/ a = 1\n" +
+                "  \\/ b = 2\n" +
+                "====\n";
+        Utils.assertSpecEquals(expected, input);
+    }
+
+    @Test
+    void testSimpleExpressionStaysOnSameLine() {
+        String spec = "---- MODULE Spec ----\n" +
+                "Zero == 0\n" +
+                "====\n";
+        Utils.assertSpecUnchanged(spec);
+    }
 }
diff --git a/src/test/resources/outputs/AllConstructs.tla b/src/test/resources/outputs/AllConstructs.tla
@@ -83,32 +83,35 @@ UpdateExamples ==
      /\ [f0 EXCEPT ![2] = 42, ![3] = @ + 1][3] = 4
      /\ DOMAIN f0 = 1 .. 3
 
-QuantExamples(U) == /\ \A u \in U: u = u
-                    /\ \E u \in U: u \in U
-                    /\ \A s1 \in SUBSET U: s1 \subseteq U
-                    /\ \A <<a ,b>> \in U \X U: a \in U /\ b \in U
+QuantExamples(U) ==
+  /\ \A u \in U: u = u
+  /\ \E u \in U: u \in U
+  /\ \A s1 \in SUBSET U: s1 \subseteq U
+  /\ \A <<a ,b>> \in U \X U: a \in U /\ b \in U
 
 InfixUse == Equal(1, 1)
 
 
 (****************************************************************)
 (* State predicates and actions                                  *)
 (****************************************************************)
-TypeInv == /\ x \in Nat
-           /\ y \in 0 .. N
-           /\ z \subseteq S
-           /\ DOMAIN f = 1 .. N /\ \A i \in 1 .. N: f[i] \in Int
-           /\ r \in [a:Nat, b:SUBSET S ]
-           /\ s \in Seq(S)
-           /\ q \in BOOLEAN
-
-Init == /\ x = 0
-        /\ y \in 0 .. N
-        /\ z \in SUBSET S
-        /\ f = [i \in 1 .. N |-> i]
-        /\ r = [ a |-> 0, b |-> {} ]
-        /\ s = <<>>
-        /\ q = FALSE
+TypeInv ==
+  /\ x \in Nat
+  /\ y \in 0 .. N
+  /\ z \subseteq S
+  /\ DOMAIN f = 1 .. N /\ \A i \in 1 .. N: f[i] \in Int
+  /\ r \in [a:Nat, b:SUBSET S ]
+  /\ s \in Seq(S)
+  /\ q \in BOOLEAN
+
+Init ==
+  /\ x = 0
+  /\ y \in 0 .. N
+  /\ z \in SUBSET S
+  /\ f = [i \in 1 .. N |-> i]
+  /\ r = [ a |-> 0, b |-> {} ]
+  /\ s = <<>>
+  /\ q = FALSE
 
 IncX == x' = x + 1
 DecX == x' = x - 1
@@ -121,22 +124,24 @@ AppendS == \E e \in S: s' = Append(s, e)
 
 Stutter == UNCHANGED << x, y, z, f, r, s, q >>
 
-Next == \/ ( IncX /\ UNCHANGED << y, z, f, r, s, q >> )
-        \/ ( ToggleQ /\ UNCHANGED << x, y, z, f, r, s >> )
-        \/ ( AssignY /\ UNCHANGED << x, z, f, r, s, q >> )
-        \/ ( UpdateZ /\ UNCHANGED << x, y, f, r, s, q >> )
-        \/ ( BumpFAny /\ UNCHANGED << x, y, z, r, s, q >> )
-        \/ ( UpdateR /\ UNCHANGED << x, y, z, f, s, q >> )
-        \/ ( AppendS /\ UNCHANGED << x, y, z, f, r, q >> )
-        \/ Stutter
+Next ==
+  \/ ( IncX /\ UNCHANGED << y, z, f, r, s, q >> )
+  \/ ( ToggleQ /\ UNCHANGED << x, y, z, f, r, s >> )
+  \/ ( AssignY /\ UNCHANGED << x, z, f, r, s, q >> )
+  \/ ( UpdateZ /\ UNCHANGED << x, y, f, r, s, q >> )
+  \/ ( BumpFAny /\ UNCHANGED << x, y, z, r, s, q >> )
+  \/ ( UpdateR /\ UNCHANGED << x, y, z, f, s, q >> )
+  \/ ( AppendS /\ UNCHANGED << x, y, z, f, r, q >> )
+  \/ Stutter
 
 Spec == Init /\ [][Next]_vars /\ WF_vars(IncX) /\ SF_vars(AssignY)
 
 Invariance == []TypeInv
 LeadsToExample == ( x < N ) ~> ( x = N )
 
-EnablementExample == /\ ENABLED IncX
-                     /\ ~ENABLED DecX
+EnablementExample ==
+  /\ ENABLED IncX
+  /\ ~ENABLED DecX
 
 ---- MODULE SimpleImported ----
 EXTENDS Naturals, Sequences

diff --git a/src/test/resources/outputs/Slush.tla b/src/test/resources/outputs/Slush.tla
@@ -249,8 +249,9 @@ Message == QueryMessage \cup QueryReplyMessage \cup TerminationMessage
 
 NoMessage == CHOOSE m : m \notin Message
 
-TypeInvariant == /\ pick \in [Node -> Color \cup { NoColor }]
-                 /\ message \subseteq Message
+TypeInvariant ==
+  /\ pick \in [Node -> Color \cup { NoColor }]
+  /\ message \subseteq Message
 
 PendingQueryMessage(pid) == {m \in message: /\ m.type = QueryMessageType
                                             /\ m.dst = pid}
@@ -416,8 +417,9 @@ AssignColorToNode ==
 ClientRequest == ClientRequestLoop \/ AssignColorToNode
 
 (* Allow infinite stuttering to prevent deadlock on termination. *)
-Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
-               /\ UNCHANGED vars
+Terminating ==
+  /\ \A self \in ProcSet: pc[self] = "Done"
+  /\ UNCHANGED vars
 
 Next ==
   ClientRequest \/ ( \E self \in SlushQueryProcess: SlushQuery(self) ) \/

diff --git a/src/test/resources/outputs/TowerOfHanoi.tla b/src/test/resources/outputs/TowerOfHanoi.tla
@@ -47,7 +47,8 @@ TypeOK ==
 (* Now we define of the initial predicate, that specifies the initial      *)
 (* values of the variables.                                                *)
 (***************************************************************************)
-Init == /\ towers = [i \in 1 .. N |-> IF i = 1 THEN 2 ^ D - 1 ELSE 0]
+Init ==
+  /\ towers = [i \in 1 .. N |-> IF i = 1 THEN 2 ^ D - 1 ELSE 0]
 \* all towers are empty except all disks are on the first Tower
 (***************************************************************************)
 (* TRUE iff the tower is empty                                             *)
@@ -57,25 +58,29 @@ IsEmptyTower(tower) == tower = 0
 (***************************************************************************)
 (* TRUE iff the disk is located on the given tower                         *)
 (***************************************************************************)
-IsOnTower(tower, disk) == /\ tower & disk = disk
+IsOnTower(tower, disk) ==
+  /\ tower & disk = disk
 
 (***************************************************************************)
 (* TRUE iff disk is the smallest disk on tower                             *)
 (***************************************************************************)
-IsSmallestDisk(tower, disk) == /\ IsOnTower(tower, disk)
-                               /\ tower & ( disk - 1 ) = 0
+IsSmallestDisk(tower, disk) ==
+  /\ IsOnTower(tower, disk)
+  /\ tower & ( disk - 1 ) = 0
 \* All less significant bits are 0
 (***************************************************************************)
 (* TRUE iff disk can be moved off of tower                                 *)
 (***************************************************************************)
-CanMoveOff(tower, disk) == /\ IsOnTower(tower, disk)
-                           /\ IsSmallestDisk(tower, disk)
+CanMoveOff(tower, disk) ==
+  /\ IsOnTower(tower, disk)
+  /\ IsSmallestDisk(tower, disk)
 
 (***************************************************************************)
 (* TRUE iff disk can be moved to the tower                                 *)
 (***************************************************************************)
-CanMoveTo(tower, disk) == \/ tower & ( disk - 1 ) = 0
-                          \/ IsEmptyTower(tower)
+CanMoveTo(tower, disk) ==
+  \/ tower & ( disk - 1 ) = 0
+  \/ IsEmptyTower(tower)
 
 (***************************************************************************)
 (*                                                                         *)