Alloy 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. See the release notes for details of new
features. To execute, simply double-click on the jar file, or type
java -jar org.alloytools.alloy.dist.jar in a console.
|Latest build||Alloy 5 (includes the version for macOS High Sierra)|
Many of these releases no longer work on MacOS out of the box.
|alloy4.2.jar||Alloy 4.2 (platform independent). Requires Java 6.|
|alloy4.2.dmg||Alloy 4.2 (for OS X). Requires Java 6.|
|alloy4.jar||Alloy 4.1 (platform independent). Requires Java 5.|
|alloy4.dmg||Alloy 4.1 (for OS X). Requires Java 5.|
- Public web page: http://haslab.github.io/Electrum
- Authors: Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha
- Synopsis: Electrum extends Alloy with mutable signatures and fields as well as connectives from Linear Temporal Logic (with Past), it is well suited to model systems featuring both structural and behavioral aspects. Verification relies on bounded and unbounded model-checking; and the Visualizer is extended to allow interactive exploration of traces.
- Public web page: https://sterling-js.github.io/
- Authors: Tristan Dyer, John Baugh