diff --git a/TESTING.md b/TESTING.md index 16f17e3..016980d 100644 --- 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 index cd9b25b..0d23536 100644 --- 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 index 2ce6799..50e0345 100644 --- 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 deleted file mode 100644 index b1a8e61..0000000 --- a/src/test/java/me/fponzi/tlaplusformatter/PropertyBasedFormatterTest.java +++ /dev/null @@ -1,61 +0,0 @@ -package me.fponzi.tlaplusformatter; - -import me.fponzi.tlaplusformatter.exceptions.SanyFrontendException; -import me.fponzi.tlasmith.TLASmith; -import net.jqwik.api.*; -import org.junit.jupiter.api.Disabled; -import tla2sany.st.TreeNode; - -import java.io.IOException; - -import static me.fponzi.tlaplusformatter.Utils.idempotency; - -class PropertyBasedFormatterTest extends LexiconTest { - // this is just for debugging purposes - // it will print out some of the generated specs and their formatted versions - @Property(tries = 3) - @Disabled - void showExampleSpecs(@ForAll("validTlaSpecs") - String spec) - throws IOException, - SanyFrontendException { - System.err.println("=== Generated TLA+ Spec ==="); - System.err.println(spec); - System.err.println("=== After Formatting ==="); - try { - System.err.println(format(spec)); - } catch (Exception e) { - System.err.println("FORMATTING ERROR: " + e.getMessage()); - System.err.println("Failed spec: " + spec); - } - System.err.println("*******************"); - } - - @Property - void formatterPreservesSemanticsAndIdempotent(@ForAll("validTlaSpecs") String spec) - throws IOException, SanyFrontendException { - idempotency(spec); - } - - private String format(String spec) throws IOException, SanyFrontendException { - return new TLAPlusFormatter(spec).getOutput(); - } - - private TreeNode parse(String spec) throws IOException, SanyFrontendException { - return new TLAPlusFormatter(spec).root; - } - - @Provide - Arbitrary validTlaSpecs() { - return Arbitraries.integers().between(1, 10000).map(seed -> { - try { - return TLASmith.toTLAString(TLASmith.generateSpec("PropTest", seed)); - } catch (Exception e) { - System.err.println("Failed to generate spec with seed: " + seed); - throw e; - } - }); - } - - -} \ No newline at end of file diff --git a/src/test/java/me/fponzi/tlaplusformatter/constructs/impl/OperatorConstructTest.java b/src/test/java/me/fponzi/tlaplusformatter/constructs/impl/OperatorConstructTest.java index f723b4d..6a15c3a 100644 --- 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 index 2604ea9..d34a9da 100644 --- a/src/test/resources/outputs/AllConstructs.tla +++ b/src/test/resources/outputs/AllConstructs.tla @@ -83,10 +83,11 @@ 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 <> \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 <> \in U \X U: a \in U /\ b \in U InfixUse == Equal(1, 1) @@ -94,21 +95,23 @@ 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 index 9482534..4df339d 100644 --- 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 index d99193d..393bb28 100644 --- 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) (***************************************************************************) (* *)