I tried to install und use nuSMV and nuXmv on the new Apple MacBook with M2. But apparently both model checkers only run on x86.
Any suggestions what to do?
Kind regards
We’re working on a new release and hopefully we find the time to make it all work on the Apple Mx processors.
1 Like
For nuXmv, we won’t be able to solve this issue ourselves as it is proprietary.
NuSMV is free software so we could theoretically compile an M2 version ourselves (well, as long as one of us owns an Apple with M2).
In any cases, I will ask the nuXmv/NuSMV developers whether they would agree to issue an M2-compatible version themselves.
We can rebuild Apple on Github Actions now, also for M1 which should cover m2. Just hoping I have the time to get this to work or someone else does the work.
1 Like
I installed NuSMV from this disabled homebrew formula and Alloy from VSCode detected it. I tested the unbounded restore_after_delete of the Trash model from the book and it works.
To install the disabled formula, I needed to first edit it to comment out the disable line
brew edit nu-smv
then I needed to tell homebrew to use the formula instead of the API
HOMEBREW_NO_INSTALL_FROM_API=1 brew install nu-smv
If homebrew is not installed and you only need the binaries, you can get the urls to the pre-compiled binaries provided by homebrew (called “bottles”) from the homebrew API
curl https://formulae.brew.sh/api/formula/nu-smv.json | jq '.bottle.stable.files'
1 Like
Hi,
Alberto Griggio from the FBK team managed to build M1 versions of both NuSMV and nuXmv but needs people to check that they work as he doesn’t own an M1 himself. Here is an excerpt form his message:
I have put the binaries (just the
binaries) on the web, it would be great if you could try them out and
let us know if they work as expected. Here are the download links:https://nuxmv.fbk.eu/downloads/test/NuSMV.xz
https://nuxmv.fbk.eu/downloads/test/nuXmv.xz(Note you need to uncompress them).
Please someone tell me whether this works or not, so that I can answer him.
Hi,
I can start nuxmv and nuSMV in a terminal and I get a message like
*** This version of nuXmv is linked to NuSMV 2.6.0.
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@fbk.eu>.
*** Copyright (C) 2010-2024, Fondazione Bruno Kessler
...
But if I use nuxmv or nuSMV as solver in the Alloy Analyzer I get the following error message:
Option Solver changed to Electrod/NuSMV
Executing "Check EchoComesBack for 1.. steps, 5 Node"
Solver=NuSMV Steps=1..2147483647 Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 Mode=batch
No translation information available. 396ms.
Solving...
.
Unknown exception occurred: kodkod.engine.AbortedException:
Electrod exit code: 1.
Thanks Burkhardt. I suppose NuSMV and nuXmv are in your PATH?
I think so. If nu*mv is not in the path, one cannot choose them as solver in the analyzer, n’est ce pas?
Should be, yes. One way to be sure is to issue which NuSMV.
But… now I’m thinking that Electrod (the binary shipped with Alloy is calle electrod and electrod.exe in the JAR, depending on the target architecture) is probably not compiled for M1 itself (I don’t handle this part of the build)! One way to check would be to extract if from the JAR and then try to run it from the command line, would you try?
Hi,
which nuSMV => /Users/br/bin/nuSMV
That’s the folder I installed the binaries and that I used with sudo launchctrl config user path
After extraction the binary electrod from the jar of Alloy, I launched it in a terminal: The result was
electrod: required argument ELECTROD_FILE is missing
Usage: electrod [OPTION]... ELECTROD_FILE
Try `electrod --help' for more information.
So I could start electrod. I don’t now if this means that electrod runs on M2.
Good to know. Can you try running electrod.exe -v spantree-badliveness-3.elo, with this .elo file? In principle, you should obtain something like:
electrod (C) 2016-2020 ONERA 1.0.0-1-geb0b02e
[INFO] Processing file: test/case-studies/spantree-badliveness-3.elo
[INFO] Parsing done
[INFO] Static analysis done
[INFO] Simplification done
[INFO] Conversion done in 5.891ms
[INFO] SMV file (size: 26KB) generated in 1.781ms
[INFO] Starting analysis: nuXmv -source test/case-studies/electrod-dba14d.scr test/case-studies/spantree-badliveness-3.elo-b354ac.smv
[INFO] Analysis done in 347ms
[INFO] Removing files:
test/case-studies/electrod-dba14d.scr
test/case-studies/spantree-badliveness-3.elo-b354ac.smv
Specification is: SAT
[INFO] Outcome:
Int##next | {} | -==- | -==-
----------------------+-------------------------------------+------+------
this##_ActNotRoot | {_ActNotRoot$0} | -==- | -==-
----------------------+-------------------------------------+------+------
ordering##Ord | {ordering##Ord$0} | -==- | -==-
----------------------+-------------------------------------+------+------
this##_Nop | {_Nop$0} | -==- | -==-
----------------------+-------------------------------------+------+------
ordering##Ord#First | {Lvl$0} | -==- | -==-
----------------------+-------------------------------------+------+------
this##_E | {_E$0} | -==- | -==-
----------------------+-------------------------------------+------+------
String | {} | -==- | -==-
----------------------+-------------------------------------+------+------
ordering##Ord#Next | {(Lvl$0 Lvl$1) (Lvl$1 Lvl$2)} | -==- | -==-
----------------------+-------------------------------------+------+------
this##Process#lvl | {} | -==- | -==-
----------------------+-------------------------------------+------+------
this##_ActRoot | {_ActRoot$0} | -==- | -==-
----------------------+-------------------------------------+------+------
this##_Dummy | {_Dummy$0} | -==- | -==-
----------------------+-------------------------------------+------+------
this##_E#_event | {(_Nop$0 _Dummy$0)} | -==- | -==-
----------------------+-------------------------------------+------+------
this##Root | {Process$2} | -==- | -==-
----------------------+-------------------------------------+------+------
this##Process | {Process$1 Process$2} | -==- | -==-
----------------------+-------------------------------------+------+------
this##Lvl | {Lvl$0 Lvl$1 Lvl$2} | -==- | -==-
----------------------+-------------------------------------+------+------
this##Process#parent | {} | -==- | -==-
----------------------+-------------------------------------+------+------
ordering##Ord#Last | {Lvl$2} | -==- | -==-
----------------------+-------------------------------------+------+------
this##Process#adj | {(Process$1 Process$2) (Process$2 | -==- | -==-
| Process$1)} | |
----------------------+-------------------------------------+------+------
seq##Int | {} | -==- | -==-
----------------------+-------------------------------------+------+------
ints | {} | -==- | -==-
----------------------+-------------------------------------+------+------
| LOOP | |
[INFO] Total allocated memory: 0.023GB
[INFO] Elapsed (wall-clock) time: 359ms
1006 ~/tmp/Alloy.app/Contents/Resources/org.alloytools.alloy/x86-mac % ./electrod -v spantree-badliveness-3.elo
electrod (C) 2016-2020 ONERA 1.0.0
[INFO] Processing file: spantree-badliveness-3.elo
[INFO] Parsing done
[INFO] Static analysis done
[INFO] Simplification done
[INFO] Conversion done in 9.722ms
[INFO] SMV file (size: 26KB) generated in 3.596ms
[INFO] Starting analysis: nuXmv -source ./electrod-cbd661.scr ./spantree-badliveness-3.elo-9de75d.smv
[E022] nuXmv failed with error code -5 and error output:
Script and model files kept at "./electrod-cbd661.scr" and
"./spantree-badliveness-3.elo-9de75d.smv", remember to remove them.
Aborting (56.361ms).
I have a suspicion, please cat ./electrod-cbd661.scr.
cat ./electrod-cbd661.scr
set default_trace_plugin 1;
set on_failure_script_quits 1;
read_model;
flatten_hierarchy;
build_flat_model;
encode_variables;
build_boolean_model;
check_ltlspec_ic3;
quit -x
Sigh, it’s not what I thought… But the issue is on the nuXmv side apparently. If I can bother you again, would you please show the complete output of nuXmv -source ./electrod-cbd661.scr ./spantree-badliveness-3.elo-9de75d.smv in case not everything is captured by electrod?
1008 ~/tmp/Alloy.app/Contents/Resources/org.alloytools.alloy/x86-mac % nuXmv -source ./electrod-cbd661.scr ./spantree-badliveness-3.elo-9de75d.smv
*** This is nuXmv 2.0.0 (compiled on Thu Jan 18 21:56:22 2024)
*** Copyright (c) 2014-2024, Fondazione Bruno Kessler
*** For more information on nuXmv see https://nuxmv.fbk.eu
*** or email to <nuxmv@fbk.eu>.
*** Please report bugs at https://nuxmv.fbk.eu/bugs
*** (click on "Login Anonymously" to access)
*** Alternatively write to <nuxmv@fbk.eu>.
*** This version of nuXmv is linked to NuSMV 2.6.0.
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@fbk.eu>.
*** Copyright (C) 2010-2024, Fondazione Bruno Kessler
*** This version of nuXmv is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of nuXmv is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
*** This version of nuXmv is linked to MathSAT
*** Copyright (C) 2009-2019 by Fondazione Bruno Kessler
*** Copyright (C) 2009-2019 by University of Trento and others
*** See http://mathsat.fbk.eu
-- no proof or counterexample found with bound 4
-- LTL specification F (((((G-f -> !((E-f-f | ((E-f-f | (E-e-f & E-f-e)) | (E-d-f & E-f-d))) | ((((E-f-f | ((E-f-f | (E-e-f & E-f-e)) | (E-d-f & E-f-d))) & (E-f-f | ((E-f-f | (E-e-f & E-f-e)) | (E-d-f & E-f-d)))) | ((E-e-f | (((E-f-f & E-e-f) | (E-e-f & E-e-e)) | (E-d-f & E-e-d))) & (E-f-e | (((E-f-e & E-f-f) | (E-e-e & E-f-e)) | (E-d-e & E-f-d))))) | ((E-d-f | (((E-f-f & E-d-f) | (E-e-f & E-d-e)) | (E-d-f & E-d-d))) & (E-f-d | (((E-f-d & E-f-f) | (E-e-d & E-f-e)) | (E-d-d & E-f-d))))))) & (G-e -> !((E-e-e | (((E-f-e & E-e-f) | E-e-e) | (E-d-e & E-e-d))) | ((((E-f-e | (((E-f-e & E-f-f) | (E-e-e & E-f-e)) | (E-d-e & E-f-d))) & (E-e-f | (((E-f-f & E-e-f) | (E-e-f & E-e-e)) | (E-d-f & E-e-d)))) | ((E-e-e | (((E-f-e & E-e-f) | E-e-e) | (E-d-e & E-e-d))) & (E-e-e | (((E-f-e & E-e-f) | E-e-e) | (E-d-e & E-e-d))))) | ((E-d-e | (((E-f-e & E-d-f) | (E-e-e & E-d-e)) | (E-d-e & E-d-d))) & (E-e-d | (((E-f-d & E-e-f) | (E-e-d & E-e-e)) | (E-d-d & E-e-d)))))))) & (G-d -> !((E-d-d | (((E-f-d & E-d-f) | (E-e-d & E-d-e)) | E-d-d)) | ((((E-f-d | (((E-f-d & E-f-f) | (E-e-d & E-f-e)) | (E-d-d & E-f-d))) & (E-d-f | (((E-f-f & E-d-f) | (E-e-f & E-d-e)) | (E-d-f & E-d-d)))) | ((E-e-d | (((E-f-d & E-e-f) | (E-e-d & E-e-e)) | (E-d-d & E-e-d))) & (E-d-e | (((E-f-e & E-d-f) | (E-e-e & E-d-e)) | (E-d-e & E-d-d))))) | ((E-d-d | (((E-f-d & E-d-f) | (E-e-d & E-d-e)) | E-d-d)) & (E-d-d | (((E-f-d & E-d-f) | (E-e-d & E-d-e)) | E-d-d))))))) & (((G-f -> (((!E-f-d & !E-f-e) & !E-f-f) | (((E-f-f & (!E-f-e & !E-f-d)) | (E-f-e & (!E-f-f & !E-f-d))) | (E-f-d & (!E-f-f & !E-f-e))))) & (G-e -> (((!E-e-d & !E-e-e) & !E-e-f) | (((E-e-f & (!E-e-e & !E-e-d)) | (E-e-e & (!E-e-f & !E-e-d))) | (E-e-d & (!E-e-f & !E-e-e)))))) & (G-d -> (((!E-d-d & !E-d-e) & !E-d-f) | (((E-d-f & (!E-d-e & !E-d-d)) | (E-d-e & (!E-d-f & !E-d-d))) | (E-d-d & (!E-d-f & !E-d-e))))))) & (((!(((!E-d-d & !E-d-e) & !E-d-f) & G-d) & !(((!E-e-d & !E-e-e) & !E-e-f) & G-e)) & !(((!E-f-d & !E-f-e) & !E-f-f) & G-f)) | ((((((!E-f-d & !E-f-e) & !E-f-f) & G-f) & (!(((!E-e-d & !E-e-e) & !E-e-f) & G-e) & !(((!E-d-d & !E-d-e) & !E-d-f) & G-d))) | ((((!E-e-d & !E-e-e) & !E-e-f) & G-e) & (!(((!E-f-d & !E-f-e) & !E-f-f) & G-f) & !(((!E-d-d & !E-d-e) & !E-d-f) & G-d)))) | ((((!E-d-d & !E-d-e) & !E-d-f) & G-d) & (!(((!E-f-d & !E-f-e) & !E-f-f) & G-f) & !(((!E-e-d & !E-e-e) & !E-e-f) & G-e)))))) is false
-- as demonstrated by the following execution sequence
Trace Description: IC3 counterexample
Trace Type: Counterexample
-- Loop starts here
-> State: 1.1 <-
G-f = TRUE
C-f-d = FALSE
G-d = FALSE
C-f-e = TRUE
G-e = TRUE
C-f-f = FALSE
C-d-f = FALSE
C-e-f = TRUE
C-e-e = FALSE
C-d-e = FALSE
C-e-d = FALSE
C-d-d = FALSE
H-d = FALSE
H-f = TRUE
H-e = FALSE
L-d-a = FALSE
L-d-b = FALSE
L-d-c = FALSE
E-f-d = FALSE
E-f-e = FALSE
E-f-f = FALSE
E-e-d = FALSE
E-e-e = FALSE
E-e-f = FALSE
E-d-d = FALSE
E-d-e = FALSE
E-d-f = FALSE
I-h-d = FALSE
I-i-d = FALSE
L-e-a = FALSE
L-e-b = FALSE
L-e-c = FALSE
I-h-e = FALSE
I-i-e = FALSE
L-f-a = FALSE
L-f-b = FALSE
L-f-c = FALSE
I-h-f = FALSE
I-i-f = FALSE
I-g-j = TRUE
-- Loop starts here
-> State: 1.2 <-
G-f = TRUE
C-f-d = FALSE
G-d = FALSE
C-f-e = TRUE
G-e = TRUE
C-f-f = FALSE
C-d-f = FALSE
C-e-f = TRUE
C-e-e = FALSE
C-d-e = FALSE
C-e-d = FALSE
C-d-d = FALSE
H-d = FALSE
H-f = TRUE
H-e = FALSE
L-d-a = FALSE
L-d-b = FALSE
L-d-c = FALSE
E-f-d = FALSE
E-f-e = FALSE
E-f-f = FALSE
E-e-d = FALSE
E-e-e = FALSE
E-e-f = FALSE
E-d-d = FALSE
E-d-e = FALSE
E-d-f = FALSE
I-h-d = FALSE
I-i-d = FALSE
L-e-a = FALSE
L-e-b = FALSE
L-e-c = FALSE
I-h-e = FALSE
I-i-e = FALSE
L-f-a = FALSE
L-f-b = FALSE
L-f-c = FALSE
I-h-f = FALSE
I-i-f = FALSE
I-g-j = TRUE
-- Loop starts here
-> State: 1.3 <-
G-f = TRUE
C-f-d = FALSE
G-d = FALSE
C-f-e = TRUE
G-e = TRUE
C-f-f = FALSE
C-d-f = FALSE
C-e-f = TRUE
C-e-e = FALSE
C-d-e = FALSE
C-e-d = FALSE
C-d-d = FALSE
H-d = FALSE
H-f = TRUE
H-e = FALSE
L-d-a = FALSE
L-d-b = FALSE
L-d-c = FALSE
E-f-d = FALSE
E-f-e = FALSE
E-f-f = FALSE
E-e-d = FALSE
E-e-e = FALSE
E-e-f = FALSE
E-d-d = FALSE
E-d-e = FALSE
E-d-f = FALSE
I-h-d = FALSE
I-i-d = FALSE
L-e-a = FALSE
L-e-b = FALSE
L-e-c = FALSE
I-h-e = FALSE
I-i-e = FALSE
L-f-a = FALSE
L-f-b = FALSE
L-f-c = FALSE
I-h-f = FALSE
I-i-f = FALSE
I-g-j = TRUE
-> State: 1.4 <-
G-f = TRUE
C-f-d = FALSE
G-d = FALSE
C-f-e = TRUE
G-e = TRUE
C-f-f = FALSE
C-d-f = FALSE
C-e-f = TRUE
C-e-e = FALSE
C-d-e = FALSE
C-e-d = FALSE
C-d-d = FALSE
H-d = FALSE
H-f = TRUE
H-e = FALSE
L-d-a = FALSE
L-d-b = FALSE
L-d-c = FALSE
E-f-d = FALSE
E-f-e = FALSE
E-f-f = FALSE
E-e-d = FALSE
E-e-e = FALSE
E-e-f = FALSE
E-d-d = FALSE
E-d-e = FALSE
E-d-f = FALSE
I-h-d = FALSE
I-i-d = FALSE
L-e-a = FALSE
L-e-b = FALSE
L-e-c = FALSE
I-h-e = FALSE
I-i-e = FALSE
L-f-a = FALSE
L-f-b = FALSE
L-f-c = FALSE
I-h-f = FALSE
I-i-f = FALSE
I-g-j = TRUE
Thanks for you help! A last demand: please run the same command again and then immediately echo $? (on zsh, it yields the return code of the previous command, I suppose it’ll work on Mac).
The return code of the statement is 0.
So, given the same exact command, Electrod got a -5 error code when running it itself, but you (and I, on my machine) get the intended 0. I have no idea why.
Additionally, nuXmv shows yields a trace with several loop states instead of a single one (a behaviour we already witnessed long ago).
I’m a but stuck here, I need to think about this… Thanks again for your help Burkhardt.