# 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:** 4
**Page:** 2
### Author:  [@mica](https://alloytools.discourse.group/u/mica)
#### Post date: [January 26, 2024, 8:57am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/21 "2024-01-26T08:57:02Z")
> [@esb-dev](#):
>
> I don’t now if this means that electrod runs on M2.
`file` command can tell you the architecture of an executable. For example, the `nusmv` from Homebrew is an arm64 binary:
```sh
file $(which nusmv)
/opt/homebrew/bin/nusmv: Mach-O 64-bit executable arm64
```
But the FBK binaries are universal:
```sh
file ./nuXmv
./nuXmv: Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit executable x86_64] [arm64]
./nuXmv (for architecture x86_64): Mach-O 64-bit executable x86_64
./nuXmv (for architecture arm64): Mach-O 64-bit executable arm64
```
```sh
file ./NuSMV
./NuSMV: Mach-O universal binary with 2 architectures: [x86_64:Mach-O 64-bit executable x86_64] [arm64]
./NuSMV (for architecture x86_64): Mach-O 64-bit executable x86_64
./NuSMV (for architecture arm64): Mach-O 64-bit executable arm64
```
I supposed that maybe for some reason Alloy is running it in x86\_64 mode, so I `mv`’d the original executable to `NuSMV-universal` and made a wrapper `NuSMV` to force it to run in arm64:
```sh
#!/bin/sh
arch -arm64 NuSMV-universal "$@"
```
It worked!
```txt
Option Solver changed to Electrod/NuSMV
Executing "Check restore_after_delete"
Solver=NuSMV Steps=1..10 Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 Mode=batch
No translation information available. 39ms.
No counterexample found. Assertion may be valid. 1097ms.
```
---
### Author:  [@mica](https://alloytools.discourse.group/u/mica)
#### Post date: [January 26, 2024, 9:38am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/22 "2024-01-26T09:38:57Z")
Extracted and checked `electrod` and it is indeed a x86\_64 binary:
```sh
file ./electrod
./electrod: Mach-O 64-bit executable x86_64
```
---
### Author:  [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)
#### Post date: [January 26, 2024, 5:07pm UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/23 "2024-01-26T17:07:53Z")
Thanks for the investigation. I’m not completely sure to follow the end of your reasoning though, as I don’t really master the intricacies of various Mac architectures (the only Mac I have ever used was the first one 😉 ). Do you suggest that the issue when running nuXmv from electrod would be the difference of target architecture between the two? Currently, the latter is built by Github or by @nmacedo (can’t remember). I suppose we should try to build a universal (if possible) or arm64 (at worst) version of electrod?
---
### Author:  [@mica](https://alloytools.discourse.group/u/mica)
#### Post date: [January 30, 2024, 9:15am UTC](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327/24 "2024-01-30T09:15:09Z")
> [@grayswandyr](#):
>
> Do you suggest that the issue when running nuXmv from electrod would be the difference of target architecture between the two?
No. I would have had suspected that if I didn’t already succeed in running the arm64 `nusmv` from homebrew. I am quite surprised by the mix of architectures here:
1. Alloy runs in arm64 Java11 JVM (by Zulu)
2. `electrod`, an x86\_64 binary, is invoked from arm64 JVM
3. `nusmv`, an arm64 binary, is invoked from x86\_64 `electrod`
If the mix of architecture is a problem I expect step 2 to fail already. Or that step 3 would fail with an arm64 binary. But bizarrely this sandwich of a mixture works.
x86\_64 binaries on M1 macOS runs via Rosetta translation. According to [Apple documentation](https://developer.apple.com/documentation/apple-silicon/about-the-rosetta-translation-environment):
> Rosetta translates all `x86_64` instructions, but it doesn’t support the execution of some newer instruction sets and processor features, such as AVX, AVX2, and AVX512 vector instructions. If you include these newer instructions in your code, execute them only after verifying that they are available.
Maybe the x86\_64 version makes use of advanced instruction sets?
> [@grayswandyr](#):
>
> I suppose we should try to build a universal (if possible) or arm64 (at worst) version of electrod?
Yes, a universal or arm64 `electrod` is likely to fix it. The arm64 JVM should invoke the arm64 version in the universal `electrod`, which should then invoke the arm64 version in the universal `NuSMV`.
Until then, a quick workaround can be to distribute a wrapper along with the universal, to launch the proper binary depending on hardware information:
```sh
#!/bin/sh
case "$(sysctl machdep.cpu.brand_string)" in
*"Apple"*) arch -arm64 NuSMV-universal "$@" ;;
*) NuSMV-universal "$@" ;;
esac
```
[Previous page](https://alloytools.discourse.group/t/nusmv-and-nuxmv-on-apple-m2/327.md?page=1)