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!
WARNING TO OTHERS
Modifying user path can seriously destabilize your system in hard-to-diagnose ways!
@DanielJackson You need to reboot when modifying launchctl config this way. I just verified it by repairing my own installation of nu-smv.
It didn’t work at first for me because homebrew installs to a different prefix on M1 macs. It should also be noted that the version segment of the path my vary over time.
$ brew --prefix > /opt/homebrew
Install NuSMV $ brew install nu-smv
Check the Monterey system path. If your homebrew bin is there, skip the rest. $ launchctl getenv PATH
Modify the Monterey system path, adding the homebrew prefix. $ sudo launchctl config user path $(brew --prefix)/bin:$(launchctl getenv PATH)
Reboot the machine and restart Alloy6.1. In the menu Options → Solver you will have the option Electrod/NuSMV.
I’m trying to use NuSMV in Alloy 6.1.0 as a backend solver on an M1 MacBook Air (Monterey), and I get an error like this:
Unknown exception occurred:
javax.xml.parsers.FactoryConfigurationError: Provider
com.sun.org.apache.xerces.internal.jaxp.DocumentBuilderFactoryImpl
not found
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 18.0.1.1 2022-04-22
Java™ SE Runtime Environment (build 18.0.1.1+2-6)
Java HotSpot™ 64-Bit Server VM (build 18.0.1.1+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[0])
Hi John
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.
Best
David
