Announcing Alloy 6!

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!

—Daniel Jackson


Using NuSMV with the Mac App on Mac OS Monterey:

  1. Install NuSMV
    brew install nu-smv
  2. Convince Monterey to use the path to nu-smv
    sudo launchctl config user path /usr/local/Cellar/nu-smv/2.6.0/bin
  3. Reboot the machine and restart Alloy6,
    now in menu Options>Solver you should have the option Electrod/NuSMV

This worked for me
Burkhardt Renz

P.S. Alloy6 is a fascinating advancement, thanks to Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo there is not only the program but also the online guide An overview of Alloy — Formal Software Design with Alloy 6.

1 Like

Thanks, Burkhardt! I forgot to mention that you can now use a model checker as the back end, and explore unbounded traces.

Not sure why you need to reboot?

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

  1. Install NuSMV
    $ brew install nu-smv
  2. Check the Monterey system path. If your homebrew bin is there, skip the rest.
    $ launchctl getenv PATH
  3. Modify the Monterey system path, adding the homebrew prefix. $ sudo launchctl config user path $(brew --prefix)/bin:$(launchctl getenv PATH)
  4. 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
not found

Am I doing something silly?


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 2022-04-22
Java™ SE Runtime Environment (build
Java HotSpot™ 64-Bit Server VM (build, 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])

Is this to be expected?


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.

Thank you, David. No worries. It’s helpful to know … I think we can work around it …