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
I could not find the option 'Electrod/NuSMV in “Options > Solver” in Alloy 6/Electrum. How can I use NuSMV with Electrum?