Skip to content
This repository was archived by the owner on Mar 16, 2026. It is now read-only.
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 0 additions & 33 deletions TESTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
32 changes: 12 additions & 20 deletions build.gradle.kts
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
plugins {
id("java")
id("io.ktor.plugin") version "2.3.12"
id("com.github.spotbugs") version "6.0.7"
id("io.ktor.plugin") version "3.4.1"
id("com.github.spotbugs") version "6.4.8"
jacoco
}

Expand All @@ -16,33 +16,25 @@ 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("commons-io:commons-io:2.16.1")
testImplementation("com.github.FedericoPonzi:tlaplus-smith:f5a70e21d1") {
isChanging = true
}
implementation("org.lamport:tla2tools:1.8.0-SNAPSHOT")
implementation("commons-io:commons-io:2.21.0")

testImplementation(platform("org.junit:junit-bom:5.10.0"))
testImplementation(platform("org.junit:junit-bom:6.0.3"))
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")
testImplementation("org.mockito:mockito-core:5.22.0")
testImplementation("org.mockito:mockito-junit-jupiter:5.22.0")
implementation("commons-cli:commons-cli:1.11.0")

// Logging
implementation("org.slf4j:slf4j-api:2.0.7")
implementation("ch.qos.logback:logback-classic:1.5.28")
implementation("org.slf4j:slf4j-api:2.0.17")
implementation("ch.qos.logback:logback-classic:1.5.32")

implementation("com.opencastsoftware:prettier4j:0.3.2")
}
Expand Down
Binary file modified gradle/wrapper/gradle-wrapper.jar
Binary file not shown.
4 changes: 2 additions & 2 deletions gradle/wrapper/gradle-wrapper.properties
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
#Sat Jul 20 00:54:34 IST 2024
distributionBase=GRADLE_USER_HOME
distributionPath=wrapper/dists
distributionUrl=https\://services.gradle.org/distributions/gradle-8.5-bin.zip
distributionUrl=https\://services.gradle.org/distributions/gradle-9.4.0-bin.zip
networkTimeout=10000
zipStoreBase=GRADLE_USER_HOME
zipStorePath=wrapper/dists
50 changes: 32 additions & 18 deletions gradlew

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

40 changes: 22 additions & 18 deletions gradlew.bat

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

This file was deleted.

Loading