Open Ramneet-Singh opened 2 months ago
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:
--ddlib cudd
).--sylvan:threads 1
). Note: this sometimes significantly slower.
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: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