Alloy 6

Alloy 6 is a self-contained executable that includes an extended version of the Kodkod model finder, various SAT solvers (including native solvers like minisat, lingeling/plingeling, and glucose, as well as the cross-platform Sat4j), the standard Alloy library, and tutorial examples.

Beyond being a standalone tool, the same JAR file can be incorporated into other applications to use Alloy as an API. It also includes the project's source code.

The workspace is divided into several specialized projects:

• cnf: Setup directory. Dependencies are defined in cnf/central.xml using Maven POM layout.
• org.alloytools.alloy.application: Main application code (parser, AST, visualiser, and application logic).
• org.alloytools.alloy.dist: Project responsible for creating the distribution executable JAR.
• org.alloytools.alloy.extra: Models and examples.
• org.alloytools.pardinus: A Kodkod extension without native code.
• org.alloytools.kodkod.nativesat: Native code libraries for Kodkod.

Bnd-specific files:

• cnf/build.bnd: Shared settings between projects.
• ./bnd.bnd: Project-specific settings that determine which code is included in a JAR.
• cnf/central.mvn: Dependencies from Maven Central.

If your build environment requires a proxy, pass the following arguments to ./gradlew (replacing XXXXX with your actual settings):

./gradlew -Dhttps.proxyHost=XXXXX -Dhttp.proxyHost=XXXXX -Dhttp.proxyPort=XXXXX \
     -Dhttps.proxyPort=XXXXX -Dhttp.proxyUser=XXXXX -Dhttp.proxyPassword=XXXXX \
     -Dhttps.proxyUser=XXXXX -Dhttps.proxyPassword=XXXXX \
     build

Alloy requires a recent JVM (Java 17 or later) to run on any operating system.

java -version # requires Java 17

The workspace uses a bnd workspace setup with a Maven layout, making it compatible with Eclipse and the Bndtools plugin.

1. Download and install Eclipse.
2. Install the Bndtools plugin from the Eclipse Marketplace.
3. Import the existing projects from the Git workspace. Bndtools will handle continuous creation of the final executable and automatic updates when downstream projects change.

Native builds are handled differently depending on the target platform:

• Darwin (macOS): Requires a Mac with either amd64 or arm64 architecture. The build is managed by a Makefile located in the satsolvers directory. Note that the Makefile builds all supported Darwin natives in a single invocation for performance reasons.
• Linux and Windows: These can be built using dockcross via Docker containers. The dockcross_windows file provides guidance on using these toolchains.

Important Notes:

• Do not attempt to build for darwin/arm64e.
• The Makefile in satsolvers is designed to handle irregularities and should not be heavily refactored to be 'cleaner', as it allows for necessary exceptions in the build process.

To build Alloy and run the GUI, clone the repository recursively, build using the included Gradle wrapper, and execute the resulting distribution JAR.

Note on Proxies: If you are behind a proxy, gradlew may fail. You can pass proxy settings using -D flags for https.proxyHost, http.proxyHost, http.proxyPort, https.proxyPort, http.proxyUser, http.proxyPassword, https.proxyUser, and https.proxyPassword.

git clone --recursive https://github.com/AlloyTools/org.alloytools.alloy.git
cd org.alloytools.alloy
./gradlew build
java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar

The --output flag controls where results are stored:

• Default: A directory named after the source file stem.
• Specific Directory: If a name is provided, a directory is created. Files inside are named using the pattern {command}-{index}.{extension}.
• Console: Use - to send all calculated solutions or transformed files directly to the console.
• Timestamped: Appending + to the output name (e.g., my-output+) creates a directory with a timestamp (e.g., my-output-20260611T12-00-00).
• Force Overwrite: Use --force to delete and recreate the output directory if it already contains files.

The --type option determines the format of the generated solution files. Supported types are:

• none: No output files generated.
• text: Plain text representation of the solution.
• table: Markdown formatted tables (useful for temporal traces and skolem values).
• json: Structured JSON data (includes SolutionDTO).
• xml: XML representation of the solution instance.

# Example: Output solutions as JSON
alloy model.als --type json

The SimpleReporter class is a CLI-oriented implementation of the A4Reporter interface. It is used to capture and format diagnostic information from the Alloy solver during execution.

Key behaviors include:

• Warnings: Formats ErrorWarning messages by combining the position (pos) and the message (msg).
• Solver Metadata: Captures solver configuration details such as bitwidth, max sequence, symmetry settings, and strategy via the translate method.
• Solving Statistics: Reports the number of variables (total and primary) and clauses during the solve step.
• SAT/UNSAT Results: Logs whether a solution was found (SAT!) or not (UNSAT!) to the CLI.
• Trace Logging: Uses the cli.trace method to output low-level details like CNF file paths.