Tests Failing on Apple Silicon

[Ramneet-Singh]

Hi,

Thanks for developing Storm! I'm compiling the master branch on an Apple Silicon (M1) Mac as I was having issues compiling the stable version. When running make check after building, the following two tests are failing for me:

[ RUN      ] DdPrismModelBuilderTest_Sylvan.Mdp
/Users/ramneet/maverick-home/OneDriveIITD/iitd/sems/sem10/mdp-decomp/storm/src/test/storm/builder/DdPrismModelBuilderTest.cpp:210: Failure
Expected equality of these values:
  37ul
    Which is: 37
  mdp->getNumberOfStates()
    Which is: 35
/Users/ramneet/maverick-home/OneDriveIITD/iitd/sems/sem10/mdp-decomp/storm/src/test/storm/builder/DdPrismModelBuilderTest.cpp:211: Failure
Expected equality of these values:
  59ul
    Which is: 59
  mdp->getNumberOfTransitions()
    Which is: 55
/Users/ramneet/maverick-home/OneDriveIITD/iitd/sems/sem10/mdp-decomp/storm/src/test/storm/builder/DdPrismModelBuilderTest.cpp:212: Failure
Expected equality of these values:
  59ul
    Which is: 59
  mdp->getNumberOfChoices()
    Which is: 55
[  FAILED  ] DdPrismModelBuilderTest_Sylvan.Mdp (990 ms)
...
17/36 Test #17: run-test-modelchecker-prctl-dtmc .......Bus error***Exception: 243.89 sec

I haven't installed Spot, in case it matters. My goal is to benchmark MDP symbolic model building. I figured I didn't need to install Spot for that. Are these two test failures expected?

Thanks for your help!
Best,
Ramneet

[tquatmann]

Hi,

unfortunately, there are some issues when using Storm with Sylvan (MTBDD library for symbolic model building/checking) on Apple Silicon.
This will also likely affect symbolic model building benchmarks. We believe this is a concurrency issue either on the Storm or the Sylvan side that is somehow specific to ARM architectures. For the time being, I can suggest some possible workarounds:

• use an x86 machine.
• use the alternative BDD library cudd (command line --ddlib cudd).
• use sylvan in single threaded mode (command line --sylvan:threads 1). Note: this sometimes significantly slower.
• build an x86 version of Storm and emulate using Rosetta 2, see here for further but potentially outdated details.

[sjunges]

Hey,

After I recently updated my Macbook M1, I get a different bug that I think is related:

In particular, when running the tests on DtmcPrctlModelCheckerTest/24, where TypeParam = (anonymous namespace)::DdSylvanRationalSearchEnvironment
[ RUN ] DtmcPrctlModelCheckerTest/24.Crowds

I either get segfaults (sometimes) or infinite run time (mostly).

If I run things with LLDB, then I do not get any errors.

Potentially importantly, after updating, my compiler version is AppleClang 15.0.0.15000309, i.e., up to date.

All other tests seem to run fine.