Initial PBT

Author: FedericoPonzi

.gitignore

@@ -40,4 +40,5 @@ bin/
 .vscode/
 
 ### Mac OS ###
-.DS_Store
+.DS_Store
+.jqwik-database

README.md

@@ -1,13 +1,16 @@
 ## TLA<sup>+</sup> formatter
+
 <p align="center"><img alt="temporary tla+ formatter logo" src="assets/tlaplus-formatter-temp-logo.jpg" width="250"></p>
 
-This is a formatter for the TLA<sup>+</sup> language. 
+This is a formatter for the TLA<sup>+</sup> language.
 
-It uses tlaplus tools' SANY library to parse your specification, and it applies some (at the moment) predefined format to it.
+It uses tlaplus tools' SANY library to parse your specification, and it applies some (at the moment) predefined format
+to it.
 
 This is still _ALPHA_ software, feel free to try it out and leave feedback but be aware it might break your specs.
 
 ## Project Goals:
+
 * A formatter for the TLA+ language. Pluscal is currently not a priority.
 * It should be configurable but also provide sane defaults.
 * It should never add useless chars (no extra spaces or extra newlines)
@@ -16,40 +19,71 @@ This is still _ALPHA_ software, feel free to try it out and leave feedback but b
 * It should be fast.
 
 ## Configurations:
+
 If you have specific requests for configuration options you would like to have, please consider opening an issue.
 
-Currently, the idea is to follow the same ideas behind rustfmt. A user level formatter config and a project level formatter config.
+Currently, the idea is to follow the same ideas behind rustfmt. A user level formatter config and a project level
+formatter config.
 
 ## Example
+
 To see some examples of current reformatting, compare:
-* HourClock.tla: [before](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/inputs/HourClock.tla) and [after](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/outputs/HourClock.tla)
-* TowerOfHanoi.tla: [before](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/inputs/TowerOfHanoi.tla) and [after](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/outputs/TowerOfHanoi.tla)
-* Stones.tla: [before](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/inputs/Stones.tla) and [after](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/outputs/Stones.tla)
 
-More examples are in the test/java/resources/{inputs|outputs} folders. These sources are taken from the TLA+ Examples repo.
+*
+
+HourClock.tla: [before](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/inputs/HourClock.tla)
+and [after](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/outputs/HourClock.tla)
+
+*
+
+TowerOfHanoi.tla: [before](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/inputs/TowerOfHanoi.tla)
+and [after](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/outputs/TowerOfHanoi.tla)
+
+*
+
+Stones.tla: [before](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/inputs/Stones.tla)
+and [after](https://github.com/FedericoPonzi/tlaplus-formatter/blob/main/src/test/resources/outputs/Stones.tla)
+
+More examples are in the test/java/resources/{inputs|outputs} folders. These sources are taken from the TLA+ Examples
+repo.
+
+## Testing with TLA+-Smith
+
+This project integrates [TLA+-Smith](https://github.com/fponzi/tlaplus-smith), a random TLA+ specification generator,
+for comprehensive testing. TLA+-Smith helps ensure the formatter works correctly with a wide variety of TLA+ constructs
+and edge cases.
 
 ## How to run
-If you want to try it out, go to the build page of the latest commit, and download the "Package.zip" file from the artifact section at the bottom of the page ([Example](https://github.com/FedericoPonzi/tlaplus-formatter/actions/runs/10027954925)).
 
-You will need at least java 11 (same requirement as tlatools).
+If you want to try it out, go to the build page of the latest commit, and download the "Package.zip" file from the
+artifact section at the bottom of the
+page ([Example](https://github.com/FedericoPonzi/tlaplus-formatter/actions/runs/10027954925)).
+
+You will need at least java 11 (the same requirement as tlatools).
 
 Unzip the file, and you can invoke the formatter like this:
+
 ```
 java -jar tlaplus-formatter.jar <INFILE> [OUTFILE]
 ```
 
-It will print your reformatted spec in output. If the optional "OUTFILE" parameter is specified, it will write the output to that file.
-You can use the input file as output file as well. Run with `-help` parameter for the help text. 
+It will print your reformatted spec in output. If the optional "OUTFILE" parameter is specified, it will write the
+output to that file.
+You can use the input file as the output file as well. Run with `-help` parameter for the help text.
 
 ## VSCode integration
+
 It's a work in progress, see [PR-327](https://github.com/tlaplus/vscode-tlaplus/pull/327/files) on vscode-tlaplus repo.
 
 ## Limitations
-Because it uses SANY underneath (TLC's parser), your spec needs to first succeed SANY's 
-parsing process, otherwise the formatter won't be able to reformat your file.
+
+Because it uses SANY underneath (TLC's parser), your spec needs to first succeed SANY's
+parsing process; otherwise the formatter won't be able to reformat your file.
 
 ---
 
 ## Development
-Some of the `constants` used in the code are coming from SANY's codebase, specifically from this file: `src/tla2sany/st/SyntaxTreeConstants.java` (check [tlaplus repo](https://github.com/tlaplus/tlaplus/)).
+
+Some of the `constants` used in the code are coming from SANY's codebase, specifically from this file:
+`src/tla2sany/st/SyntaxTreeConstants.java` (check [tlaplus repo](https://github.com/tlaplus/tlaplus/)).
 

TESTING.md

@@ -0,0 +1,57 @@
+# Testing Guide
+
+This document describes the testing approach for the TLA+ formatter.
+
+## Test Types
+
+### Unit Tests
+Individual component tests located in `src/test/java/me/fponzi/tlaplusformatter/` that test specific lexicon elements and formatting constructs.
+
+### 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
+# Run all tests
+./gradlew test
+
+# Run specific test class
+./gradlew test --tests FormatterE2ETest
+
+# Build and test
+./gradlew build
+```

build.gradle.kts

@@ -6,21 +6,35 @@ plugins {
 group = "me.fponzi"
 version = "1.0-SNAPSHOT"
 
+java {
+    sourceCompatibility = JavaVersion.VERSION_11
+    targetCompatibility = JavaVersion.VERSION_11
+}
+
 repositories {
+    mavenLocal()
     mavenCentral()
     // Add the repository for the snapshot dependency
     maven {
         url = uri("https://oss.sonatype.org/content/repositories/snapshots/")
     }
+    maven {
+        url = uri("https://jitpack.io")
+    }
 }
 
 dependencies {
     implementation("org.lamport:tla2tools:1.8.0-SNAPSHOT")
     implementation("commons-io:commons-io:2.16.1")
+    testImplementation("com.github.FedericoPonzi:tlaplus-smith:main-SNAPSHOT") {
+        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

src/test/java/me/fponzi/tlaplusformatter/PropertyBasedFormatterTest.java

@@ -0,0 +1,82 @@
+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 org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+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 formatterPreservesSemantics(@ForAll("validTlaSpecs") String spec)
+            throws IOException, SanyFrontendException {
+        try {
+            String formatted = format(spec);
+            TreeNode originalAst = parse(spec);
+            TreeNode formattedAst = parse(formatted);
+
+            assertTrue(compareAst(originalAst, formattedAst),
+                    "AST should be preserved after formatting");
+        } catch (Exception e) {
+            System.err.println("Failed spec: " + spec);
+            throw e;
+        }
+    }
+
+    @Property
+    void formatterIsIdempotent(@ForAll("validTlaSpecs") String spec)
+            throws IOException, SanyFrontendException {
+        String formatted = format(spec);
+        String doubleFormatted = format(formatted);
+
+        assertEquals(formatted, doubleFormatted,
+                "Formatter should be idempotent");
+    }
+
+    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<String> 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;
+            }
+        });
+    }
+
+
+}