Alloy 4 is a self-contained executable, which includes the 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.
To execute, simply double-click on the jar file, or type
java -jar alloy4.jar in a console.
|FAQ||Frequently asked questions about Alloy|
|reference||Download language reference for Alloy 4 (PDF)|
|comparisons||Comparisons to Z, B, VDM and OCL (PDF)|
|grammar||A grammar for Alloy 4 in plain text (TXT), also see the cup file|
|quick guide||Overview of new features in Alloy 4|
|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|