Remove tlaplus-smith dependency for now

Author: FedericoPonzi

CHANGELOG.md

@@ -1,3 +1,6 @@
+## Upcoming: 0.3.0
+* Operator definitions with conjunction/disjunction list bodies now break after `==`, improving VS Code code folding.
+
 ## 0.2.1
 * Fix: no longer inserts spurious whitespace after symbolic prefix operators (`[]`, `<>`, `~`, `-`).
   For example, `[][Next]_vars` was incorrectly formatted as `[] [Next]_vars`.

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

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