NuSMV in Alloy 6/Electrum

1

In Tutorial · haslab/Electrum Wiki · GitHub 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

2

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.

3

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
source ~/.zprofile
exec java -Duser.language=en -Xdock:name="Electrum" -Xdock:icon=~/bin/icons/Alloy.icns -jar ~/bin/electrum.jar

Works fine now