# Announcing Alloy 6! **URL:** \ **Category:** Alloy 6\ **Created:** [November 14, 2021, 7:06pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189 "2021-11-14T19:06:03Z")\ **Posts on this page:** 8\ **Page:** 1
**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\ **Post date:** [November 14, 2021, 7:06pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/1 "2021-11-14T19:06:03Z")
I am very excited to announce officially that Alloy 6 is available! You can download it [here](https://github.com/AlloyTools/org.alloytools.alloy/releases), see a list of changes [here](https://alloytools.org/alloy6.html), and read the revised language spec [here](https://alloytools.org/spec.html). 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 ---
**Author:** ![esb-dev](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/esb-dev/32/63_2.png) [@esb-dev](https://alloytools.discourse.group/u/esb-dev)\ **Post date:** [November 15, 2021, 10:23am UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/2 "2021-11-15T10:23:48Z")
Using NuSMV with the Mac App Alloy.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](https://haslab.github.io/formal-software-design/overview/index.html). ---
**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\ **Post date:** [November 16, 2021, 5:03pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/3 "2021-11-16T17:03:29Z")
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? ---
**Author:** ![carl-reverb](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/carl-reverb/32/125_2.png) [@carl-reverb](https://alloytools.discourse.group/u/carl-reverb)\ **Post date:** [March 8, 2022, 1:31pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/4 "2022-03-08T13:31:06Z")
**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` 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. ---
**Author:** ![jwbaugh](https://avatars.discourse-cdn.com/v4/letter/j/ba8739/32.png) [@jwbaugh](https://alloytools.discourse.group/u/jwbaugh)\ **Post date:** [June 14, 2022, 9:42pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/5 "2022-06-14T21:42:47Z")
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 Am I doing something silly? ![count-screenshot](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/1d6181b041a51c8842fe5deff43e5557f5178528.jpeg) John ---
**Author:** ![jwbaugh](https://avatars.discourse-cdn.com/v4/letter/j/ba8739/32.png) [@jwbaugh](https://alloytools.discourse.group/u/jwbaugh)\ **Post date:** [June 16, 2022, 7:52pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/6 "2022-06-16T19:52:40Z")
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]) ![count2-screenshot](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/63aa282fe4724d6a2312c659c45d942df9d55ae1.jpeg) Is this to be expected? John ---
**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Post date:** [June 16, 2022, 8:40pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/7 "2022-06-16T20:40:11Z")
> [@jwbaugh](#): > > 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. Best David ---
**Author:** ![jwbaugh](https://avatars.discourse-cdn.com/v4/letter/j/ba8739/32.png) [@jwbaugh](https://alloytools.discourse.group/u/jwbaugh)\ **Post date:** [June 16, 2022, 9:01pm UTC](https://alloytools.discourse.group/t/announcing-alloy-6/189/8 "2022-06-16T21:01:06Z")
Thank you, David. No worries. It’s helpful to know … I think we can work around it … Regards, John