Installing storm 1.8.1 on Apple M2; error due to Spot installation

[abadithela]

Hi, I have spot installed on my machine for a different project.

When I follow the build steps for Storm 1.8.1 on Apple silicon, I'm getting the following error:

[ 43%] Building CXX object src/storm/CMakeFiles/storm.dir/automata/LTL2DeterministicAutomaton.cpp.o
In file included from /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/src/storm/automata/LTL2DeterministicAutomaton.cpp:15:
/Users/apurvabadithela/software/spot-2.11.5/spot/twaalgos/hoa.hh:29:10: fatal error: 'bddx.h' file not found
#include <bddx.h>
         ^~~~~~~~
1 error generated.
make[2]: *** [src/storm/CMakeFiles/storm.dir/automata/LTL2DeterministicAutomaton.cpp.o] Error 1
make[1]: *** [src/storm/CMakeFiles/storm.dir/all] Error 2
make: *** [all] Error 2

Could you please let me know if there is something that I am missing? I'd prefer not to mess with the spot installation since it is working for some of my other projects. I have not had this issue previously when I used to install storm because I did not have spot installed.

Thanks!

[sjunges]

Hi Apurva, all,

Hope you are doing well.

The missing file is part of Buddy. Our script is actually handling this situation, but appearantly not correctly. This could be because you may have installed spot for use x86/via rosetta.

What would really help is if you would include the output of running cmake .. in an empty build directory.

Best,
Sebastian

[abadithela]

Hi Sebastian,

I'm doing well; hope are you too! Please let me know if the following is what you need or if I should try something else:

I deleted the old build folder inside storm and created an empty one. Then, I ran the following command to use the ARM compiled CMAKE binary: /opt/homebrew/bin/cmake .. which results in the following output:

CMake Deprecation Warning at CMakeLists.txt:3 (cmake_policy):
  Compatibility with CMake < 3.5 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.


-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- The C compiler identification is AppleClang 14.0.3.14030022
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Storm - CMake install dir: /usr/local/lib/CMake/storm
-- Storm - Building RELEASE version.
-- Storm - Could not find ccache.
-- Storm - Detected operating system Mac OS.
-- Storm - Detected that target system uses Apple Silicon.
CMake Warning at CMakeLists.txt:194 (message):
  Compiling natively on Apple Silicon is experimental.  Please report issues
  to support@stormchecker.org.  For more information visit
  https://www.stormchecker.org/documentation/obtain-storm/apple-silicon.html


CMake Warning at CMakeLists.txt:197 (message):
  CLN and GiNaC are currently not supported on Apple Silicon-based
  architectures.  Disabling Storm and carl usage of the libraries.


-- Storm - Assuming extension for shared libraries: .dylib
-- Storm - Assuming extension for static libraries: .a
-- Storm - Build static libraries.
CMake Warning at CMakeLists.txt:247 (message):
  Disabling stack checks for AppleClang version 11.0.0 or higher.


-- Storm - Enabling link-time optimizations.
-- Performing Test COMPILER_C_WORKS
-- Performing Test COMPILER_C_WORKS - Success
-- Performing Test COMPILER_CXX_WORKS
-- Performing Test COMPILER_CXX_WORKS - Success
-- Storm - Using compiler configuration AppleClang 14.0.3.14030022.
-- Storm - Building external resources with 6 job(s) in parallel.
-- Storm - Including Eigen 3.4.0 commit b0eded878d5d162d61583a286c0d8a45406ad1bc.
-- Storm - Using workaround for Boost >= 1.81
-- Storm - Using boost 108200 (library version 1_82).
-- Storm - Including ExprTk.
-- Storm - Including Parallel Hashmap.
-- Storm - Including cpphoafparser 0.99.2
-- Storm - Including ModernJSON.
-- Storm - Linking with Z3 (version 4.12.2). (Z3 version supports optimization)
-- Storm - Using system version of glpk.
-- Storm - Linking with glpk 5.0
CMake Warning at resources/3rdparty/include_cudd.cmake:39 (message):
  There are some known issues compiling CUDD on some setups.  We implemented
  a workaround that mostly works, but if you still have problems compiling
  CUDD, especially if you do not use the default compiler of your system,
  please contact the Storm developers.
Call Stack (most recent call first):
  resources/3rdparty/CMakeLists.txt:287 (include)
  CMakeLists.txt:473 (include)


-- Storm - Linking with CUDD 3.0.0.
-- Carl - Start of config process
CMake Warning (dev) at CMakeLists.txt:1 (project):
  cmake_minimum_required() should be called prior to this top-level project()
  call.  Please see the cmake-commands(7) manual for usage documentation of
  both commands.
This warning is for project developers.  Use -Wno-dev to suppress it.

CMake Deprecation Warning at CMakeLists.txt:2 (cmake_minimum_required):
  Compatibility with CMake < 3.5 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.


-- -- The C compiler identification is AppleClang 14.0.3.14030022
-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Check for working C compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/cc - skipped
-- Detecting C compile features
-- Detecting C compile features - done
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Carl-Storm - Storm 3rdparty binary dir: /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty
-- Carl-Storm - Finished configuration.
-- Configuring done (0.5s)
-- Generating done (0.0s)
-- Build files have been written to: /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty/carl_download

Cloning into 'source_dir'...
Already on 'master'
CMake Deprecation Warning at CMakeLists.txt:12 (cmake_minimum_required):
  Compatibility with CMake < 3.5 will be removed from a future version of
  CMake.

  Update the VERSION argument <min> value or use a ...<max> suffix to tell
  CMake that the project does not need compatibility with older versions.


CMake Warning at CMakeLists.txt:100 (message):
  Compiling natively on Apple Silicon is experimental.  Please report issues
  to support@stormchecker.org.  For more information visit
  https://www.stormchecker.org/documentation/obtain-storm/apple-silicon.html


CMake Warning at CMakeLists.txt:102 (message):
  CLN and GiNaC are currently not supported on Apple Silicon-based
  architectures.  Disabling usage of the libraries.


CMake Warning (dev) at /opt/homebrew/Cellar/cmake/3.27.7/share/cmake/Modules/ExternalProject.cmake:3136 (message):
  The DOWNLOAD_EXTRACT_TIMESTAMP option was not given and policy CMP0135 is
  not set.  The policy's OLD behavior will be used.  When using a URL
  download, the timestamps of extracted files should preferably be that of
  the time of extraction, otherwise code that depends on the extracted
  contents might not be rebuilt if the URL changes.  The OLD behavior
  preserves the timestamps from the archive instead, but this is usually not
  what you want.  Update your project to the NEW behavior or specify the
  DOWNLOAD_EXTRACT_TIMESTAMP option with a value of true to avoid this
  robustness issue.
Call Stack (most recent call first):
  /opt/homebrew/Cellar/cmake/3.27.7/share/cmake/Modules/ExternalProject.cmake:4345 (_ep_add_download_command)
  resources/gtest.cmake:1 (ExternalProject_Add)
  resources/resources.cmake:157 (include)
  CMakeLists.txt:164 (include)
This warning is for project developers.  Use -Wno-dev to suppress it.

-- [ 12%] Creating directories for 'carl-config'
[ 25%] Performing download step (git clone) for 'carl-config'
Your branch is up to date with 'origin/master'.
[ 37%] Performing update step for 'carl-config'
[ 50%] No patch step for 'carl-config'
[ 62%] Performing configure step for 'carl-config'
-- The CXX compiler identification is AppleClang 14.0.3.14030022
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/c++ - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Using version 14.25.
-- Version: carl 14.25
-- Detected that target system uses Apple Silicon.
-- Using clang 14.0.3.14030022 on apple
-- CXX Flags:  -std=c++1y -stdlib=libc++ -pthread
-- CXX Debug Flags: -g -O1
-- CXX Release Flags: -O3 -DNDEBUG -O3 -fomit-frame-pointer -msse -msse2 -funroll-loops
-- Build type: RELEASE
-- Building static: no
-- cotire is disabled
-- GMP / GMPXX 6.3.0 was found at /opt/homebrew/include and /opt/homebrew/lib/libgmp.dylib
-- Boost 108200 was found at /opt/homebrew/include and Boost_filesystem_SHARED;Boost_system_SHARED;Boost_program_options_SHARED;Boost_regex_SHARED;Boost_unit_test_framework_SHARED
-- Eigen3 3.4.0 was found at /Users/apurvabadithela/software/eigen3
-- Bliss is disabled
-- CLN is disabled
-- CoCoA is disabled
-- GiNaC is disabled
-- GTest 1.8.0 was found at /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty/carl/resources/src/GTest-EP/googletest/include and /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty/carl/resources/src/GTest-EP-build/googlemock/gtest/libgtest_main.a
-- Doxygen 1.9.2 was found at /usr/local/bin/doxygen
-- Did not find clang-tidy, target tidy is disabled.
-- Did not find clang-format, target format is disabled.
-- Found LATEX: /Library/TeX/texbin/latex   
-- Registered with cmake
-- Configuring done (0.4s)
-- Generating done (0.1s)
-- Build files have been written to: /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty/carl
[ 75%] No build step for 'carl-config'
[ 87%] No install step for 'carl-config'
[100%] Completed 'carl-config'
[100%] Built target carl-config

-- Carl - End of config process
-- Storm - Using shipped version of carl.
-- Storm - Linking with shipped carl 14.25 (include: /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty/carl/include/, library /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build/resources/3rdparty/carl/lib/libcarl.dylib, CARL_USE_CLN_NUMBERS: OFF, CARL_USE_GINAC: OFF).
-- Storm - Use system version of xerces.
-- Storm (GSPN) - Linking with Xerces-c 3.2.4: /opt/homebrew/lib/libxerces-c.dylib
-- Storm - Using system version of Spot 2.11.5 (include: /Users/apurvabadithela/software/spot-2.11.5, library: /usr/local/lib/libspot.dylib;/usr/local/lib/libbddx.dylib).
-- Storm - Using shipped version of sylvan.
-- Storm - Linking with sylvan.
-- Found Doxygen: /usr/local/bin/doxygen (found version "1.9.2") found components: doxygen dot 
CMake Warning at CMakeLists.txt:509 (message):
  Storm - Git version information not available, statically assuming version
  1.8.1.


-- Storm - Version is 1.8.1 (version 1.8.1 + 0 commits), building from git: GITDIR-NOTFOUND (dirty: DirtyState::Unknown).
-- Registered with cmake
-- Configuring done (9.1s)
-- Generating done (0.5s)
-- Build files have been written to: /Users/apurvabadithela/software/prob_model_checking_software/storm-1.8.1/build

[sjunges]

Thanks, I am doing fine :-)

The output his helps.

In particular,

-- Storm - Using system version of Spot 2.11.5 (include: /Users/apurvabadithela/software/spot-2.11.5, library: /usr/local/lib/libspot.dylib;/usr/local/lib/libbddx.dylib).

is informative.

• First, the include dir and the library dirs do not seem to match, which may indicate that the system is somehow finding two version of the spot installation.
• Furthermore, I was expecting that the include dir for spot actually ends with /include.
  Could you check whether your folder /Users/apurvabadithela/software/spot-2.11.5 has an include folder and post that here?
• Finally, it may indeed be that your spot installation does not match the architecture for arm silicon. As a reference, I installed spot via home-brew, the spot include dir is then /opt/homebrew/spot/include. I understand you may not want to install a second version of spot in your system though.

While we are looking into this, you may want to set -DSTORM_USE_SPOT_SYSTEM=OFF when calling cmake. That should ensure that storm uses its own version of Spot (which should not interfere with the system version of spot).

[sjunges]

I assume that you made your way around the issue. I made a comment in the existing issue on Apple Silicon that should help to fail during config time if the version we find is not compiled for the same architecture.

Feel free to reopen, if the issue still persists.