On Redundancy in Alloy Models

On Redundancy in Alloy Models This artifact accompanies the paper On Redundancy in Alloy Models.It contains the source code of our custom Alloy Analyzer with redundancy analysis, the dataset of Alloy models used in our experiments, and all scripts to reproduce the results presented in the paper. The artifact can be downloaded from Zenodo: https://doi.org/10.5281/zenodo.21333886 It has the following structure: ├── alloy-redundancy.tar # Docker image ├── alloy-redundancy.zip # Source code archive ├── Dockerfile # Dockerfile to build the image ├── LICENSE # License file ├── org.alloytools.alloy.dist.jar # Customized Alloy Analyzer ├── paper.pdf # Copy of the accepted paper ├── README.md ├── REQUIREMENTS.md └── STATUS.md Setup Docker (recommended) Load the image: docker load -i alloy-redundancy.tar Run the container for your architecture: docker run --rm --name alloy-redundancy -it alloy-redundancy This gives you an interactive shell with all tools ready to use. The dataset and pre-computed results are available in the container at /alloy-redundancy/analysis/ for quick access. Manual Setup If you prefer to set up the environment manually, follow these steps: Install the pre-requisites: Java 17 Python 3.13 with poetry Extract the alloy-redundancy.zip archive. unzip alloy-redundancy.zip Build the project using Gradle: cd alloy-redundancy ./gradlew clean build -x test For Windows, use gradlew.bat instead of ./gradlew. The built JAR file for the custom Alloy Analyzer will be located at org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar. You can run it with: java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar To set up the Python environment for the analysis scripts, use poetry: cd alloy-redundancy poetry install Alternatively, you can also build the docker image yourself using the provided Dockerfile: docker build -t alloy-redundancy . And then run the container as described above (Docker (recommended)). Usage Checking Redundancy via Custom Alloy Analyzer The pre-built custom Alloy Analyzer with redundancy analysis is included as org.alloytools.alloy.dist.jar. You can use it or build it yourself using the instructions above. NOTE: Run from the host machine, NOT inside the Docker container. Copy the JAR to your local machine: docker cp alloy-redundancy:/alloy-redundancy/org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar . Run the jar file: java -jar org.alloytools.alloy.dist.jar It will open the Alloy GUI. You can load any .als file and use the new "Redundancy" and "Exp. Red." buttons to analyze your model. You need to SAVE the model before running the analysis. Smoke Test (Quick Run) [!WARNING]Running the smoke test will overwrite the existing CSV files in analysis/results/csv/ with new results. If you want to preserve our results, consider copying the results directory before running the smoke test. # Optional docker cp alloy-redundancy:/alloy-redundancy/analysis/results/ ./results smokeTest.sh runs the entire pipeline on only 5 files per step, verifying that all scripts work correctly: # Run from /alloy-redundancy (Docker container) ./analysis/scripts/smokeTest.sh Full Pipeline [!WARNING]The full benchmark runs on the entire dataset and may take couple of weeks depending on your hardware. Each script applies a 10-minute timeout per file. If you want to run the full pipeline on a subset of the dataset, you can use the --max argument in the smokeTest.sh script to limit the number of alloy models processed. For example: # Run from /alloy-redundancy (Docker container) # For 100 models, run: ./analysis/scripts/smokeTest.sh --max 100 All scripts live in analysis/scripts/ and must be run from /alloy-redundancy. Each script accepts two optional arguments: Option Default Description --dataset analysis/dataset/ Path to the dataset directory --max 0 (all files) Maximum number of files to process Output CSVs are written to analysis/results/csv/. Collect Model Metadata: modelStats.sh computes structural metrics for every .als file: lines of code, number of signatures, facts, flat facts, and commands. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/modelStats.sh Output: analysis/results/csv/modelStats.csv Detect Global Redundancy: checkGlobal.sh finds constraints that are redundant across all commands in a model. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/checkGlobal.sh Output: analysis/results/csv/checkGlobal.csv Detect Local Redundancy: checkLocal.sh finds constraints that are redundant within each individual command. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/checkLocal.sh Output: analysis/results/csv/checkLocal.csv Check SAT/UNSAT Status: checkUnsat.sh runs each command in every model and records whether the result is SAT or UNSAT. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/checkUnsat.sh Output: analysis/results/csv/checkUnsat.csv Filter Higher-Order Failures: checkHigherOrderFail.sh identifies models that cannot be analyzed due to higher-order quantification that Alloy cannot skolemize. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/checkHigherOrderFail.sh Output: analysis/results/csv/higherOrderFail.csv Compute Maximal Redundant Set (Global): maxRedSetGlobal.sh computes the largest set of constraints that are jointly redundant, considering all commands globally. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/maxRedSetGlobal.sh Output: analysis/results/csv/maxRedSetGlobal.csv Compute Maximal Redundant Set (Local): maxRedSetLocal.sh computes the maximal redundant set per command. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/maxRedSetLocal.sh Output: analysis/results/csv/maxRedSetLocal.csv Explain Redundancy (SAT4J): explainGlobal.sh reads maxRedSetGlobal.csv and uses DDMin with SAT4J to find a minimal explanation for each globally redundant constraint. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/explainGlobal.sh Output: analysis/results/csv/explainGlobal.csv Explain Redundancy (MiniSat Native): explainNativeGlobal.sh performs the same explanation task as Step 8, but uses MiniSat with UNSAT core extraction. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/explainNativeGlobal.sh Output: analysis/results/csv/explainNativeGlobal.csv Measure Solving Overhead: checkOverhead.sh reads maxRedSetLocal.csv and compares solving time and SAT variable counts with and without redundant constraints. # Run from /alloy-redundancy (Docker container) ./analysis/scripts/checkOverhead.sh Output: analysis/results/csv/checkOverhead.csv Generate Paper Figures and Tables: paper.py reads all result CSVs and produces the tables, statistics, and figures used in the paper. # Run from /alloy-redundancy (Docker container) python ./analysis/scripts/paper.py Output figures are saved to analysis/results/figures/ and the tables are shown in the terminal: Figure File Content Maximal redundant set sizes maxRedSet-Sizes.pdf Figure 2 Constraint lengths maxRedSet-len.pdf Figure 3 Explanation sizes expl-sizes.pdf Figure 4 Explanation lengths expl-len.pdf Figure 5