Documentation Alloy 6
Alloy 6 is a self-contained executable, which includes the Pardinus/Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples. The same jar file can be incorporated into other applications to use Alloy as an API, and includes the source code.
You can download alloy from https://github.com/AlloyTools/org.alloytools.alloy/releases/tag/v6.0.0
To execute, simply double-click on the jar file, or type java -jar org.alloytools.alloy.dist.jar in a console. For MacOS users, there is a DMG file.
Since Alloy 6, the tool can also perform temporal model-checking. at the time of this writing, this relies on external tools NuSMV or nuXmv (preferred from an efficiency point of view) that should be installed by the user and mad available in the PATH.
| FAQ | Frequently asked questions about Alloy |
| reference | Language reference for Alloy 6 |
| grammar | Alloy Grammar in Java CUP |
| lex | Alloy Lexical tokens in flex |
| quick guide | Overview of new features in Alloy 4 |
| comparisons | Comparisons to Z, B, VDM and OCL (PDF) |
| Alloy API | Documentation for Alloy API |
| Alloy API Examples | examples of using the compiler, the ast, the evaluator |
| online tutorial | A step-by-step walkthrough and tutorial for Alloy 4 |
| tutorial slides | Slides for day-long tutorial by Rob Seater and Greg Dennis |
| digital humanities tutorial | A tutorial introducing Alloy for digital humanities work, by C. M. Sperberg-McQueen |