I am very excited to announce officially that Alloy 6 is available!
You can download it here, see a list of changes here, and read the revised language spec here.
Alloy 6 brings dynamic analysis natively to Alloy. Until now, if you wanted some time-varying behavior in your model, you had to represent time explicitly. That was nice in some ways, and it let you roll your own model of time (which can be handy occasionally)—and that’s all still there if you want it. But it was pretty annoying too, because you had to extend relations with a time column, and add boilerplate code just to get traces.
With Alloy 6, none of this is necessary. Traces are built in, and using the new keyword var, you mark the relations that can change over time. Even better, Alloy 6 brings new temporal logic quantifiers, which are beautifully integrated into the language, so you can use them (like regular quantifiers) both in the model and in the properties you want to check, and you can mix-and-match them freely with the standard quantifiers, saying things like eventually all n: Node | ... (eventually all nodes have some property, which is subtly different from all n: Node | eventually... !). Alloy’s visualization capability has been extended for the new dynamics, with some great new features (such as seeing adjacent states in the same frame).
Kudos to the Electrum team for this wonderful contribution: Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo. And thank you to Peter Kriens for his help with the deployment. Looking forward to lots of exciting new models and analysis discoveries!
I discovered I’m able to avoid the “javax” error if I start up Alloy directly from the jar file (using a recent JRE) instead of using the image from the .dmg installer.
% java --version
java 22.214.171.124 2022-04-22
Java™ SE Runtime Environment (build 126.96.36.199+2-6)
Java HotSpot™ 64-Bit Server VM (build 188.8.131.52+2-6, mixed mode, sharing)
% java -jar org.alloytools.alloy.dist.jar
Mac classes not there
The Electrod/NuSMV solver seems to be working, at least for some models, but it appears to dislike integers:
Invalid specification for complete backend.
Invalid formula: (this/S.i = Int)
Yes, this is, in the current version. Sorry about that. We’re going to make a new, feature complete version of the translation but it’s only in the beginning so don’t hold your breath.