# nuSMV and nuXmv on Apple M2

**URL:** <https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327>\
**Category:** Uncategorized\
**Created:** [April 2, 2023, 8:14am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327 "2023-04-02T08:14:35Z")\
**Posts on this page:** 20\
**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:** [April 2, 2023, 8:14am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/1 "2023-04-02T08:14:35Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [April 3, 2023, 6:39am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/2 "2023-04-03T06:39:23Z")

</div>

We’re working on a new release and hopefully we find the time to make it all work on the Apple Mx processors.

---

<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:** [April 3, 2023, 8:22am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/3 "2023-04-03T08:22:43Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [April 3, 2023, 8:39am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/4 "2023-04-03T08:39:38Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![mica](https://avatars.discourse-cdn.com/v4/letter/m/85e7bf/32.png) [@mica](https://alloytools.discourse.group/u/mica)\
**Post date:** [January 15, 2024, 7:53pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/5 "2024-01-15T19:53:45Z")

</div>

I installed NuSMV from [this disabled homebrew formula](https://formulae.brew.sh/formula/nu-smv) 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

```auto
brew edit nu-smv

```

then I needed to tell homebrew to use the formula instead of the API

```auto
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

```sh
curl https://formulae.brew.sh/api/formula/nu-smv.json | jq '.bottle.stable.files'

```

---

<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:** [January 22, 2024, 8:02am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/6 "2024-01-22T08:02:31Z")

</div>

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/NuSMV.xz)  
> [https://nuxmv.fbk.eu/downloads/test/nuXmv.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.

---

<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:** [January 22, 2024, 8:37am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/7 "2024-01-22T08:37:58Z")

</div>

Hi,

I can start nuxmv and nuSMV in a terminal and I get a message like

```auto
*** 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:

```auto
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.

```

---

<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:** [January 22, 2024, 9:12am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/8 "2024-01-22T09:12:36Z")

</div>

Thanks Burkhardt. I suppose NuSMV and nuXmv are in your PATH?

---

<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:** [January 22, 2024, 9:44am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/9 "2024-01-22T09:44:56Z")

</div>

I think so. If nu\*mv is not in the path, one cannot choose them as solver in the analyzer, n’est ce pas?

---

<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:** [January 22, 2024, 10:11am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/10 "2024-01-22T10:11:13Z")

</div>

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?

---

<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:** [January 22, 2024, 10:30am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/11 "2024-01-22T10:30:55Z")

</div>

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

```auto
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.

---

<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:** [January 22, 2024, 1:00pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/12 "2024-01-22T13:00:55Z")

</div>

Good to know. Can you try running `electrod.exe -v spantree-badliveness-3.elo`, with [this .elo file](https://raw.githubusercontent.com/grayswandyr/electrod/master/test/case-studies/spantree-badliveness-3.elo)? In principle, you should obtain something like:

```auto
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

```

---

<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:** [January 22, 2024, 1:20pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/13 "2024-01-22T13:20:13Z")

</div>

```auto
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).

```

---

<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:** [January 22, 2024, 1:28pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/14 "2024-01-22T13:28:56Z")

</div>

I have a suspicion, please `cat ./electrod-cbd661.scr`.

---

<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:** [January 22, 2024, 1:40pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/15 "2024-01-22T13:40:44Z")

</div>

```auto
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

```

---

<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:** [January 22, 2024, 1:50pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/16 "2024-01-22T13:50:08Z")

</div>

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?

---

<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:** [January 22, 2024, 2:03pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/17 "2024-01-22T14:03:12Z")

</div>

```auto
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

```

---

<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:** [January 22, 2024, 2:23pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/18 "2024-01-22T14:23:38Z")

</div>

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).

---

<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:** [January 22, 2024, 2:36pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/19 "2024-01-22T14:36:01Z")

</div>

The return code of the statement is `0`.

---

<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:** [January 22, 2024, 2:48pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/20 "2024-01-22T14:48:06Z")

</div>

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.

[Next page](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327.md?page=2)