# NuSMV in Alloy 6/Electrum

**URL:** <https://alloytools.discourse.group/t/nusmv-in-alloy-6-electrum/168>\
**Category:** Uncategorized\
**Created:** [June 29, 2021, 9:53am UTC](https://alloytools.discourse.group/t/nusmv-in-alloy-6-electrum/168 "2021-06-29T09:53:57Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**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:** [June 29, 2021, 9:53am UTC](https://alloytools.discourse.group/t/nusmv-in-alloy-6-electrum/168/1 "2021-06-29T09:53:57Z")

</div>

In [Tutorial · haslab/Electrum Wiki · GitHub](https://github.com/haslab/Electrum/wiki/Tutorial) a method is described how to do unbounded model checking with Electrum:

“Now that we feel our specification is correct, we can check our properties _without taking the `Time` scope into account_ . In the _Options \> SAT Solver_ menu, check either `Electrod/NuSMV` or `Electrod/nuXmv` .”

I could not find the option 'Electrod/NuSMV in “Options \> Solver” in Alloy 6/Electrum. How can I use NuSMV with Electrum?

Kind regards  
Burkhardt Renz

---

<div class="post-metadata">

**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 29, 2021, 1:23pm UTC](https://alloytools.discourse.group/t/nusmv-in-alloy-6-electrum/168/2 "2021-06-29T13:23:26Z")

</div>

Hi Burkhardt,  
For complete analysis, Electrum relies on the Electrod backend as well as NuSMV or nuXmv as model checkers.

Starting with Electrum v2.1+, the Electrum JAR already comprises the Electrod backend.

On the other hand, we do not ship NuSMV nor nuXmv in the Electrum JAR. You must retrieve and install them yourself from their respective web sites (and put them in your PATH).

Also, notice that the tutorial your’re refering to is a bit outdated. I’m going to update it for Electrum v2.1/Alloy 6 right now. EDIT: done.

---

<div class="post-metadata">

**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:** [June 29, 2021, 3:27pm UTC](https://alloytools.discourse.group/t/nusmv-in-alloy-6-electrum/168/3 "2021-06-29T15:27:43Z")

</div>

Hi David,

On my Mac i did the following steps:

1. install nuSMV with “brew install nu-smv”
2. add the path to nu-smv’s bin to .zprofile
3. create app in automator executing a zsh script with

```auto
source ~/.zprofile
exec java -Duser.language=en -Xdock:name="Electrum" -Xdock:icon=~/bin/icons/Alloy.icns -jar ~/bin/electrum.jar

```

Works fine now