diff --git a/CMakeLists.txt b/CMakeLists.txt index 411de9dca..46cf1eaaf 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -20,6 +20,7 @@ include(ExternalProject) ############################################################# option(STORM_DEVELOPER "Sets whether the development mode is used" OFF) option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) +MARK_AS_ADVANCED(STORM_USE_POPCNT) option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON) option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF) option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF) @@ -29,8 +30,10 @@ option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) option(USE_CARL "Sets whether carl should be included." ON) option(USE_XERCES "Sets whether xerces should be used." OFF) option(FORCE_COLOR "Force color output" OFF) +mark_as_advanced(FORCE_COLOR) option(STORM_PYTHON "Builds the API for Python" OFF) -option(STORM_COMPILE_WITH_CCACHE "Compile using CCache" ON) +option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON) +mark_as_advanced(STORM_COMPILE_WITH_CCACHE) option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF) set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") @@ -40,6 +43,12 @@ set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (option set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") + +# Set some CMAKE Variables as advanced +mark_as_advanced(CMAKE_OSX_ARCHITECTURES) +mark_as_advanced(CMAKE_OSX_SYSROOT) +mark_as_advanced(CMAKE_OSX_DEPLOYMENT_TARGET) + # If the STORM_DEVELOPER option was turned on, we will target a debug version. if (STORM_DEVELOPER) message(STATUS "StoRM - Using development mode") @@ -50,6 +59,7 @@ message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.") if(STORM_COMPILE_WITH_CCACHE) find_program(CCACHE_FOUND ccache) + mark_as_advanced(CCACHE_FOUND) if(CCACHE_FOUND) message(STATUS "StoRM - Using ccache") set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache) @@ -116,7 +126,9 @@ if(CMAKE_COMPILER_IS_GNUCC) add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas") set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations") - + if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0) + message(FATAL_ERROR "GCC version must be at least 5.0!") + endif() # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") @@ -147,6 +159,19 @@ else(CLANG) set (CLANG ON) # Set standard flags for clang set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3") + + if(UNIX AND NOT APPLE) + if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 3.2) + message(FATAL_ERROR "Clang version must be at least 3.2!") + endif() + endif() + + if(UNIX AND APPLE) + if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3) + message(FATAL_ERROR "Clang version must be at least 7.3!") + endif() + endif() + if(UNIX AND NOT APPLE AND NOT USE_LIBCXX) set(CLANG_STDLIB libstdc++) message(STATUS "StoRM - Linking against libstdc++") @@ -176,6 +201,7 @@ else(CLANG) set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing ") endif() + if(CCACHE_FOUND) set(STORM_COMPILED_BY "${STORM_COMPILED_BY} (ccache)") endif() @@ -198,517 +224,8 @@ message(STATUS "StoRM - Using Compiler Configuration: ${STORM_COMPILED_BY}") # In 3rdparty, targets are being defined that can be used # in the the system does not have a library -add_subdirectory(resources/3rdparty) - -############################################################# -## -## l3pp -## -############################################################# - -# l3pp is set up as external project -include_directories(${l3pp_INCLUDE}) -add_dependencies(resources l3pp) - -############################################################# -## -## gmm -## -############################################################# - -# Add the shipped version of GMM to the include pathes -set(GMMXX_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-5.0/include") -include_directories(${GMMXX_INCLUDE_DIR}) - -############################################################# -## -## Eigen -## -############################################################# - -# Add the shipped version of Eigen to the include pathes -set(EIGEN_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1") -include_directories(${EIGEN_INCLUDE_DIR}) - -############################################################# -## -## gmp -## -############################################################# - -# GMP is optional (unless MathSAT is used, see below) -find_package(GMP QUIET) - -############################################################# -## -## Boost -## -############################################################# - -# Boost Option variables -set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES}) -set(Boost_USE_MULTITHREADED ON) -set(Boost_USE_STATIC_RUNTIME OFF) - -find_package(Boost 1.56.0 QUIET REQUIRED) - -if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) - set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") -endif () -link_directories(${Boost_LIBRARY_DIRS}) - -include_directories(${Boost_INCLUDE_DIRS}) -list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES}) -message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})") -#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}") -#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}") - -############################################################# -## -## ExprTk -## -############################################################# - -# Use the shipped version of ExprTK -message (STATUS "StoRM - Including ExprTk") -include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk") - -############################################################# -## -## ModernJSON -## -############################################################# +include(resources/3rdparty/CMakeLists.txt) -#use the shipped version of modernjson -message (STATUS "StoRM - Including ModernJSON") -include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/") - -############################################################# -## -## Z3 (optional) -## -############################################################# - -find_package(Z3 QUIET) - -# Z3 Defines -set(STORM_HAVE_Z3 ${Z3_FOUND}) - -if(Z3_FOUND) - message (STATUS "StoRM - Linking with Z3") - include_directories(${Z3_INCLUDE_DIRS}) - list(APPEND STORM_LINK_LIBRARIES ${Z3_LIBRARIES}) -endif(Z3_FOUND) - -############################################################# -## -## glpk -## -############################################################# - -find_package(GLPK QUIET) -if(GLPK_FOUND) - message (STATUS "StoRM - Using system version of GLPK") -else() - message (STATUS "StoRM - Using shipped version of GLPK") - set(GLPK_LIBRARIES ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/lib/libglpk${DYNAMIC_EXT}) - set(GLPK_INCLUDE_DIR ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/include) - set(GLPK_VERSION_STRING 4.57) - add_dependencies(resources glpk) -endif() - -# Since there is a shipped version, always use GLPK -set(STORM_HAVE_GLPK ON) -message (STATUS "StoRM - Linking with glpk ${GLPK_VERSION_STRING}") -include_directories(${GLPK_INCLUDE_DIR}) -list(APPEND STORM_LINK_LIBRARIES ${GLPK_LIBRARIES}) - -############################################################# -## -## Gurobi (optional) -## -############################################################# - -if (STORM_USE_GUROBI) - find_package(Gurobi QUIET REQUIRED) - set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) - if (GUROBI_FOUND) - message (STATUS "StoRM - Linking with Gurobi") - include_directories(${GUROBI_INCLUDE_DIRS}) - list(APPEND STORM_LINK_LIBRARIES ${GUROBI_LIBRARY}) - #link_directories("${GUROBI_ROOT}/lib") - else() - #message(FATAL_ERROR "StoRM - Gurobi was requested, but not found!") - endif() -else() - set(STORM_HAVE_GUROBI OFF) -endif() - -############################################################# -## -## CUDD -## -############################################################# - -# Do not use system CUDD, StoRM has a modified version -set(CUDD_INCLUDE_DIR ${CMAKE_BINARY_DIR}/resources/3rdparty/cudd-3.0.0/include) -set(CUDD_SHARED_LIBRARY ${CMAKE_BINARY_DIR}/resources/3rdparty/cudd-3.0.0/lib/libcudd${DYNAMIC_EXT}) -set(CUDD_STATIC_LIBRARY ${CMAKE_BINARY_DIR}/resources/3rdparty/cudd-3.0.0/lib/libcudd${STATIC_EXT}) -set(CUDD_VERSION_STRING 3.0.0) -list(APPEND STORM_LINK_LIBRARIES ${CUDD_SHARED_LIBRARY}) -add_dependencies(resources cudd3) - -message(STATUS "StoRM - Linking with CUDD ${CUDD_VERSION_STRING}") -#message("StoRM - CUDD include dir: ${CUDD_INCLUDE_DIR}") -include_directories(${CUDD_INCLUDE_DIR}) - -############################################################# -## -## CLN -## -############################################################# - -find_package(CLN QUIET) - - -set(STORM_USE_CLN_NUMBERS OFF) -if(CLN_FOUND) - set(STORM_HAVE_CLN ON) - set(STORM_USE_CLN_NUMBERS ON) - message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") - include_directories("${CLN_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) -else() - set(STORM_HAVE_CLN OFF) - if(NOT GMP_FOUND) - message(FATAL_ERROR "StoRM - Neither CLN nor GMP found") - endif() -endif() - -############################################################# -## -## carl -## -############################################################# - -set(STORM_HAVE_CARL OFF) -if(USE_CARL) - find_package(carl QUIET REQUIRED) - if(carl_FOUND) - set(STORM_HAVE_CARL ON) - message(STATUS "StoRM - Linking with carl ${carl_VERSION_STRING}") - include_directories("${carl_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES}) - else() - message(FATAL_ERROR "StoRM - CARL was requested but not found") - endif() -endif() - -############################################################# -## -## SMT-RAT -## -############################################################# - -# No find routine yet -#find_package(smtrat QUIET) -# Not yet supported -set(smtrat_FOUND OFF) -set(STORM_HAVE_SMTRAT OFF) -if(smtrat_FOUND) - set(STORM_HAVE_SMTRAT ON) - message(STATUS "StoRM - Linking with smtrat.") - include_directories("${smtrat_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES}) -endif() - -############################################################# -## -## GiNaC -## -############################################################# - -find_package(GiNaC QUIET) - -if(GINAC_FOUND) - set(STORM_HAVE_GINAC ON) - message(STATUS "StoRM - Linking with GiNaC ${GINAC_VERSION_STRING}") - # Right now only link with GiNaC for carl - #include_directories("${GINAC_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES ${GINAC_LIBRARIES}) -else() - set(STORM_HAVE_GINAC OFF) - #TODO: Check if CARL actually requires the use of GiNaC -endif() - -############################################################# -## -## MathSAT (optional) -## -############################################################# - -if ("${MSAT_ROOT}" STREQUAL "") - set(ENABLE_MSAT OFF) -else() - set(ENABLE_MSAT ON) -endif() - -# MathSAT Defines -set(STORM_HAVE_MSAT ${ENABLE_MSAT}) -if (ENABLE_MSAT) - message (STATUS "StoRM - Linking with MathSAT") - link_directories("${MSAT_ROOT}/lib") - include_directories("${MSAT_ROOT}/include") - list(APPEND STORM_LINK_LIBRARIES "mathsat") - if(GMP_FOUND) - include_directories("${GMP_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES "gmp") - elseif(MPIR_FOUND) - include_directories("${GMP_INCLUDE_DIR}") - list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx") - else(GMP_FOUND) - message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") - endif(GMP_FOUND) -endif(ENABLE_MSAT) - -############################################################# -## -## Xerces -## -############################################################# - - find_package(Xerces QUIET REQUIRED) - if(XERCES_FOUND) - message(STATUS "StoRM - Use system version of xerces") - else() - message(STATUS "StoRM - Use shipped version of xerces") - set(XERCES_ROOT ${CMAKE_BINARY_DIR}/resources/3rdparty/xercesc-3.1.2) - set(XERCESC_INCLUDE ${XERCES_ROOT}/include) - set(XERCES_LIBRARY_PATH ${XERCES_ROOT}/lib) - set(XERCESC_LIBRARIES ${XERCES_LIBRARY_PATH}/libxerces-c.a) - - add_dependencies(resources xercesc) - endif() - - message (STATUS "StoRM - Linking with xercesc") - set(STORM_HAVE_XERCES ON) - include_directories(${XERCESC_INCLUDE}) - list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES}) - - -############################################################# -## -## Sylvan -## -############################################################# - -message(STATUS "StoRM - Using shipped version of sylvan") -message(STATUS "StoRM - Linking with sylvan") -include_directories("${Sylvan_INCLUDE_DIR}") -list(APPEND STORM_LINK_LIBRARIES ${Sylvan_LIBRARY}) -add_dependencies(resources sylvan) - -if(${OPERATING_SYSTEM} MATCHES "Linux") - find_package(Hwloc QUIET REQUIRED) - if(Hwloc_FOUND) - message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") - list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) - else() - message(FATAL_ERROR "HWLOC is required but was not found.") - endif() -endif() - -############################################################# -## -## Google Test gtest -## -############################################################# - -add_dependencies(test-resources googletest) -list(APPEND STORM_TEST_LINK_LIBRARIES ${GTEST_LIBRARIES}) - -############################################################# -## -## Intel Threading Building Blocks (optional) -## -############################################################# - -set(STORM_HAVE_INTELTBB OFF) -if (STORM_USE_INTELTBB) - # Point to shipped TBB directory - set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb42_20140122_merged-win-lin-mac") - find_package(TBB QUIET REQUIRED) - - if (TBB_FOUND) - message(STATUS "StoRM - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") - message(STATUS "StoRM - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") - set(STORM_HAVE_INTELTBB ON) - link_directories(${TBB_LIBRARY_DIRS}) - include_directories(${TBB_INCLUDE_DIRS}) - list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc) - else(TBB_FOUND) - message(FATAL_ERROR "StoRM - TBB was requested, but not found!") - endif(TBB_FOUND) -endif(STORM_USE_INTELTBB) - -############################################################# -## -## Threads -## -############################################################# - -find_package(Threads QUIET REQUIRED) -if (NOT Threads_FOUND) - message(FATAL_ERROR "StoRM - Threads was requested, but not found!") -endif() -include_directories(${THREADS_INCLUDE_DIRS}) -list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT}) -if (STORM_USE_COTIRE) - target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT}) -endif(STORM_USE_COTIRE) - -if (MSVC) - # Add the DebugHelper DLL - set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib") - target_link_libraries(storm "Dbghelp.lib") -endif(MSVC) - -############################################################# -## -## CUDA Library generation -## -############################################################# - - -if ("${CUDA_ROOT}" STREQUAL "") - set(ENABLE_CUDA OFF) -else() - set(ENABLE_CUDA ON) -endif() - -# CUDA Defines -if (ENABLE_CUDA) - set(STORM_CPP_CUDA_DEF "define") -else() - set(STORM_CPP_CUDA_DEF "undef") -endif() - - -# CUDA Defines -set(STORM_CPP_CUDAFORSTORM_DEF "undef") - - -if(ENABLE_CUDA) - - # Test for type alignment - try_run(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT - ${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp" - COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR - ) - if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT) - message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") - elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0) - message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.") - else() - message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") - endif() - - # Test for Float 64bit Alignment - try_run(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT - ${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp" - COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR - ) - if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT) - message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") - elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2) - message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.") - set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define") - elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3) - message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.") - set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef") - else() - message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})") - endif() - # - # Make a version file containing the current version from git. - # - include(GetGitRevisionDescription) - git_describe_checkout(STORM_GIT_VERSION_STRING) - # Parse the git Tag into variables - string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CUDAPLUGIN_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_MINOR "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_PATCH "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_HASH "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CUDAPLUGIN_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}") - if ("${STORM_CUDAPLUGIN_VERSION_APPENDIX}" MATCHES "^.*dirty.*$") - set(STORM_CUDAPLUGIN_VERSION_DIRTY 1) - else() - set(STORM_CUDAPLUGIN_VERSION_DIRTY 0) - endif() - message(STATUS "StoRM (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})") - - - # Configure a header file to pass some of the CMake settings to the source code - configure_file ( - "${PROJECT_SOURCE_DIR}/cuda/storm-cudaplugin-config.h.in" - "${PROJECT_BINARY_DIR}/include/storm-cudaplugin-config.h" - ) - - #create library - find_package(CUDA REQUIRED) - set(CUSP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/resources/3rdparty/cusplibrary") - find_package(Cusp REQUIRED) - find_package(Thrust REQUIRED) - - set(STORM_CUDA_LIB_NAME "storm-cuda") - - file(GLOB_RECURSE STORM_CUDA_KERNEL_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.cu) - file(GLOB_RECURSE STORM_CUDA_HEADER_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.h) - - source_group(kernels FILES ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES}) - include_directories(${PROJECT_SOURCE_DIR}/cuda/kernels/) - - #set(CUDA_PROPAGATE_HOST_FLAGS OFF) - set(CUDA_NVCC_FLAGS "-arch=sm_30") - - ############################################################# - ## - ## CUSP - ## - ############################################################# - if(CUSP_FOUND) - include_directories(${CUSP_INCLUDE_DIR}) - cuda_include_directories(${CUSP_INCLUDE_DIR}) - message(STATUS "StoRM (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}") - else() - message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find CUSP!") - endif() - - ############################################################# - ## - ## Thrust - ## - ############################################################# - if(THRUST_FOUND) - include_directories(${THRUST_INCLUDE_DIR}) - cuda_include_directories(${THRUST_INCLUDE_DIR}) - message(STATUS "StoRM (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}") - else() - message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find Thrust! Check your CUDA installation.") - endif() - - include_directories(${CUDA_INCLUDE_DIRS}) - include_directories(${ADDITIONAL_INCLUDE_DIRS}) - - cuda_add_library(${STORM_CUDA_LIB_NAME} - ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES} - ) - - message (STATUS "StoRM - Linking with CUDA") - list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME}) - include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") -endif() ############################################################# ## @@ -746,7 +263,7 @@ endif(LINK_LIBCXXABI) ## ############################################################# -find_package(Doxygen REQUIRED) +find_package(Doxygen) # Add a target to generate API documentation with Doxygen if(DOXYGEN_FOUND) set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") @@ -795,7 +312,7 @@ configure_file ( "${PROJECT_SOURCE_DIR}/src/utility/storm-version.cpp" ) -set(STORM_GENERATED_SOURCES "${PROJECT_SOURCE_DIR}/src/utility/storm-version.cpp") +set(STORM_GENERATED_SOURCES "${PROJECT_BINARY_DIR}/src/utility/storm-version.cpp") # Add the binary dir include directory for storm-config.h include_directories("${PROJECT_BINARY_DIR}/include") diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 88263eaad..c93b5fa7a 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -1,96 +1,552 @@ add_custom_target(resources) add_custom_target(test-resources) -ExternalProject_Add( - xercesc - SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/xercesc-3.1.2 - CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/xercesc-3.1.2/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2 --libdir=${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} CFLAGS=-O3 CXXFLAGS=-O3 - PREFIX ${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2 - BUILD_COMMAND make - BUILD_IN_SOURCE 0 - LOG_CONFIGURE ON - LOG_BUILD ON - LOG_INSTALL ON -) +set(STORM_3RDPARTY_SOURCE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty) +set(STORM_3RDPARTY_BINARY_DIR ${PROJECT_BINARY_DIR}/resources/3rdparty) + +#### +#### Find autoreconf for cudd update step +find_program(AUTORECONF autoreconf) +mark_as_advanced(AUTORECONF) + +############################################################# +## +## l3pp +## +############################################################# + -ExternalProject_Add( - glpk - DOWNLOAD_COMMAND "" - PREFIX ${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57 - SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57 - CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57 --libdir=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER} - BUILD_COMMAND make "CFLAGS=-O2 -w" - INSTALL_COMMAND make install - BUILD_IN_SOURCE 0 - LOG_CONFIGURE ON - LOG_BUILD ON - LOG_INSTALL ON -) ExternalProject_Add( - cudd3 - DOWNLOAD_COMMAND "" - SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0 - PREFIX ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 - UPDATE_COMMAND autoreconf - CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 --libdir=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} - BUILD_COMMAND make "CFLAGS=-O2 -w" - INSTALL_COMMAND make install - BUILD_IN_SOURCE 0 - LOG_CONFIGURE ON - LOG_BUILD ON - LOG_INSTALL ON + l3pp + GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git + GIT_TAG master + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/l3pp + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND "" + LOG_INSTALL ON ) +ExternalProject_Get_Property(l3pp source_dir) +set(l3pp_INCLUDE "${source_dir}/") +include_directories(${l3pp_INCLUDE}) +add_dependencies(resources l3pp) + +############################################################# +## +## gmm +## +############################################################# + +# Add the shipped version of GMM to the include pathes +set(GMMXX_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-5.0/include") +include_directories(${GMMXX_INCLUDE_DIR}) + +############################################################# +## +## Eigen +## +############################################################# + +# Add the shipped version of Eigen to the include pathes +set(EIGEN_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1") +include_directories(${EIGEN_INCLUDE_DIR}) + +############################################################# +## +## gmp +## +############################################################# + +# GMP is optional (unless MathSAT is used, see below) +find_package(GMP QUIET) + +############################################################# +## +## Boost +## +############################################################# + +# Boost Option variables +set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES}) +set(Boost_USE_MULTITHREADED ON) +set(Boost_USE_STATIC_RUNTIME OFF) + +find_package(Boost 1.56.0 QUIET REQUIRED) + +if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL "")) + set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib") +endif () +link_directories(${Boost_LIBRARY_DIRS}) + +include_directories(${Boost_INCLUDE_DIRS}) +list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES}) +message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})") +#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}") +#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}") + +############################################################# +## +## ExprTk +## +############################################################# + +# Use the shipped version of ExprTK +message (STATUS "StoRM - Including ExprTk") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk") + +############################################################# +## +## ModernJSON +## +############################################################# + +#use the shipped version of modernjson +message (STATUS "StoRM - Including ModernJSON") +include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/") + +############################################################# +## +## Z3 (optional) +## +############################################################# + +find_package(Z3 QUIET) + +# Z3 Defines +set(STORM_HAVE_Z3 ${Z3_FOUND}) + +if(Z3_FOUND) + message (STATUS "StoRM - Linking with Z3") + include_directories(${Z3_INCLUDE_DIRS}) + list(APPEND STORM_LINK_LIBRARIES ${Z3_LIBRARIES}) +endif(Z3_FOUND) + +############################################################# +## +## glpk +## +############################################################# + +include(${STORM_3RDPARTY_SOURCE_DIR}/include_glpk.cmake) + +############################################################# +## +## Gurobi (optional) +## +############################################################# + +if (STORM_USE_GUROBI) + find_package(Gurobi QUIET REQUIRED) + set(STORM_HAVE_GUROBI ${GUROBI_FOUND}) + if (GUROBI_FOUND) + message (STATUS "StoRM - Linking with Gurobi") + include_directories(${GUROBI_INCLUDE_DIRS}) + list(APPEND STORM_LINK_LIBRARIES ${GUROBI_LIBRARY}) + #link_directories("${GUROBI_ROOT}/lib") + else() + #message(FATAL_ERROR "StoRM - Gurobi was requested, but not found!") + endif() +else() + set(STORM_HAVE_GUROBI OFF) +endif() + +############################################################# +## +## CUDD +## +############################################################# +include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake) + +############################################################# +## +## CLN +## +############################################################# + +find_package(CLN QUIET) + +if(CLN_FOUND) + set(STORM_HAVE_CLN ON) + message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}") + include_directories("${CLN_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES}) +else() + set(STORM_HAVE_CLN OFF) + if(NOT GMP_FOUND) + message(FATAL_ERROR "StoRM - Neither CLN nor GMP found") + endif() +endif() + +############################################################# +## +## carl +## +############################################################# + +set(STORM_HAVE_CARL OFF) +if(USE_CARL) + find_package(carl QUIET) + if(carl_FOUND) + set(STORM_HAVE_CARL ON) + message(STATUS "StoRM - Use system version of carl") + message(STATUS "StoRM - Linking with carl ${carl_VERSION_STRING}") + include_directories("${carl_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES}) + else() + message(STATUS "StoRM - Using shipped version of carl") + # + ExternalProject_Add( + carl + GIT_REPOSITORY https://github.com/smtrat/carl + GIT_TAG master + INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/carl + CMAKE_ARGS -DCXX=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl + BUILD_IN_SOURCE 0 + BUILD_COMMAND make lib_carl + INSTALL_COMMAND make install + LOG_UPDATE ON + LOG_CONFIGURE ON + LOG_BUILD ON + LOG_INSTALL ON + ) + + include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include) + list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) + set(STORM_HAVE_CARL ON) + endif() +endif() + +############################################################# +## +## SMT-RAT +## +############################################################# + +# No find routine yet +#find_package(smtrat QUIET) +# Not yet supported +set(smtrat_FOUND OFF) +set(STORM_HAVE_SMTRAT OFF) +if(smtrat_FOUND) + set(STORM_HAVE_SMTRAT ON) + message(STATUS "StoRM - Linking with smtrat.") + include_directories("${smtrat_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES}) +endif() + +############################################################# +## +## GiNaC +## +############################################################# + +find_package(GiNaC QUIET) + +if(GINAC_FOUND) + set(STORM_HAVE_GINAC ON) + message(STATUS "StoRM - Linking with GiNaC ${GINAC_VERSION_STRING}") + # Right now only link with GiNaC for carl + #include_directories("${GINAC_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${GINAC_LIBRARIES}) +else() + set(STORM_HAVE_GINAC OFF) + #TODO: Check if CARL actually requires the use of GiNaC +endif() + +############################################################# +## +## MathSAT (optional) +## +############################################################# + +if ("${MSAT_ROOT}" STREQUAL "") + set(ENABLE_MSAT OFF) +else() + set(ENABLE_MSAT ON) +endif() + +# MathSAT Defines +set(STORM_HAVE_MSAT ${ENABLE_MSAT}) +if (ENABLE_MSAT) + message (STATUS "StoRM - Linking with MathSAT") + link_directories("${MSAT_ROOT}/lib") + include_directories("${MSAT_ROOT}/include") + list(APPEND STORM_LINK_LIBRARIES "mathsat") + if(GMP_FOUND) + include_directories("${GMP_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES "gmp") + elseif(MPIR_FOUND) + include_directories("${GMP_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx") + else(GMP_FOUND) + message(FATAL_ERROR "GMP is required for MathSAT, but was not found!") + endif(GMP_FOUND) +endif(ENABLE_MSAT) + +############################################################# +## +## Xerces +## +############################################################# + +include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake) + +############################################################# +## +## Sylvan +## +############################################################# ExternalProject_Add( - sylvan - DOWNLOAD_COMMAND "" - PREFIX "sylvan" - SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/sylvan - CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release - BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" - INSTALL_COMMAND "" - INSTALL_DIR "${PROJECT_BINARY_DIR}/sylvan" + sylvan + DOWNLOAD_COMMAND "" + PREFIX "sylvan" + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan + CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release + BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan" + BUILD_IN_SOURCE 0 + INSTALL_COMMAND "" + INSTALL_DIR "${STORM_3RDPARTY_BINARY_DIR}/sylvan" + LOG_CONFIGURE ON + LOG_BUILD ON ) ExternalProject_Get_Property(sylvan source_dir) ExternalProject_Get_Property(sylvan binary_dir) -set(Sylvan_INCLUDE_DIR "${source_dir}/src" PARENT_SCOPE) -set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a" PARENT_SCOPE) +set(Sylvan_INCLUDE_DIR "${source_dir}/src") +set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a") + + +message(STATUS "StoRM - Using shipped version of sylvan") +message(STATUS "StoRM - Linking with sylvan") +include_directories("${Sylvan_INCLUDE_DIR}") +list(APPEND STORM_LINK_LIBRARIES ${Sylvan_LIBRARY}) +add_dependencies(resources sylvan) + +if(${OPERATING_SYSTEM} MATCHES "Linux") + find_package(Hwloc QUIET REQUIRED) + if(Hwloc_FOUND) + message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") + list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) + else() + message(FATAL_ERROR "HWLOC is required but was not found.") + endif() +endif() + +############################################################# +## +## Google Test gtest +## +############################################################# ExternalProject_Add( googletest #For downloads (may be useful later!) #SVN_REPOSITORY http://googletest.googlecode.com/svn/trunk/ #TIMEOUT 10 DOWNLOAD_COMMAND "" - SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/gtest-1.7.0" + SOURCE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/gtest-1.7.0" # Force the same output paths for debug and release builds so that # we know in which place the binaries end up when using the Xcode generator - CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 + CMAKE_ARGS -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 # Disable install step INSTALL_COMMAND "" - BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0" - INSTALL_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0" + BINARY_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0" + INSTALL_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0" # Wrap download, configure and build steps in a script to log output LOG_CONFIGURE ON LOG_BUILD ON) # Specify include dir ExternalProject_Get_Property(googletest source_dir) -set(GTEST_INCLUDE_DIR ${source_dir}/include PARENT_SCOPE) +set(GTEST_INCLUDE_DIR ${source_dir}/include) # Specify MainTest's link libraries ExternalProject_Get_Property(googletest binary_dir) -set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a PARENT_SCOPE) +set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a) -ExternalProject_Add( - l3pp - GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git - GIT_TAG master - SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/l3pp - CONFIGURE_COMMAND "" - BUILD_COMMAND "" - INSTALL_COMMAND "" - LOG_INSTALL ON -) -ExternalProject_Get_Property(l3pp source_dir) -set(l3pp_INCLUDE "${source_dir}/" PARENT_SCOPE) +add_dependencies(test-resources googletest) +list(APPEND STORM_TEST_LINK_LIBRARIES ${GTEST_LIBRARIES}) + +############################################################# +## +## Intel Threading Building Blocks (optional) +## +############################################################# + +set(STORM_HAVE_INTELTBB OFF) +if (STORM_USE_INTELTBB) + # Point to shipped TBB directory + set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb42_20140122_merged-win-lin-mac") + find_package(TBB QUIET REQUIRED) + + if (TBB_FOUND) + message(STATUS "StoRM - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.") + message(STATUS "StoRM - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.") + set(STORM_HAVE_INTELTBB ON) + link_directories(${TBB_LIBRARY_DIRS}) + include_directories(${TBB_INCLUDE_DIRS}) + list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc) + else(TBB_FOUND) + message(FATAL_ERROR "StoRM - TBB was requested, but not found!") + endif(TBB_FOUND) +endif(STORM_USE_INTELTBB) + +############################################################# +## +## Threads +## +############################################################# + +find_package(Threads QUIET REQUIRED) +if (NOT Threads_FOUND) + message(FATAL_ERROR "StoRM - Threads was requested, but not found!") +endif() +include_directories(${THREADS_INCLUDE_DIRS}) +list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT}) +if (STORM_USE_COTIRE) + target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT}) +endif(STORM_USE_COTIRE) + +if (MSVC) + # Add the DebugHelper DLL + set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib") + target_link_libraries(storm "Dbghelp.lib") +endif(MSVC) + +############################################################# +## +## CUDA Library generation +## +############################################################# + + +if ("${CUDA_ROOT}" STREQUAL "") + set(ENABLE_CUDA OFF) +else() + set(ENABLE_CUDA ON) +endif() + +# CUDA Defines +if (ENABLE_CUDA) + set(STORM_CPP_CUDA_DEF "define") +else() + set(STORM_CPP_CUDA_DEF "undef") +endif() + + +# CUDA Defines +set(STORM_CPP_CUDAFORSTORM_DEF "undef") + + +if(ENABLE_CUDA) + + # Test for type alignment + try_run(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT + ${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp" + COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR + ) + if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT) + message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") + elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0) + message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.") + else() + message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})") + endif() + + # Test for Float 64bit Alignment + try_run(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT + ${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp" + COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR + ) + if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT) + message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}") + elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2) + message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.") + set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define") + elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3) + message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.") + set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef") + else() + message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})") + endif() + # + # Make a version file containing the current version from git. + # + include(GetGitRevisionDescription) + git_describe_checkout(STORM_GIT_VERSION_STRING) + # Parse the git Tag into variables + string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CUDAPLUGIN_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}") + string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_MINOR "${STORM_GIT_VERSION_STRING}") + string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_PATCH "${STORM_GIT_VERSION_STRING}") + string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}") + string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_HASH "${STORM_GIT_VERSION_STRING}") + string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CUDAPLUGIN_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}") + if ("${STORM_CUDAPLUGIN_VERSION_APPENDIX}" MATCHES "^.*dirty.*$") + set(STORM_CUDAPLUGIN_VERSION_DIRTY 1) + else() + set(STORM_CUDAPLUGIN_VERSION_DIRTY 0) + endif() + message(STATUS "StoRM (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})") + + + # Configure a header file to pass some of the CMake settings to the source code + configure_file ( + "${PROJECT_SOURCE_DIR}/cuda/storm-cudaplugin-config.h.in" + "${PROJECT_BINARY_DIR}/include/storm-cudaplugin-config.h" + ) + + #create library + find_package(CUDA REQUIRED) + set(CUSP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/resources/3rdparty/cusplibrary") + find_package(Cusp REQUIRED) + find_package(Thrust REQUIRED) + + set(STORM_CUDA_LIB_NAME "storm-cuda") + + file(GLOB_RECURSE STORM_CUDA_KERNEL_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.cu) + file(GLOB_RECURSE STORM_CUDA_HEADER_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.h) + + source_group(kernels FILES ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES}) + include_directories(${PROJECT_SOURCE_DIR}/cuda/kernels/) + + #set(CUDA_PROPAGATE_HOST_FLAGS OFF) + set(CUDA_NVCC_FLAGS "-arch=sm_30") + + ############################################################# + ## + ## CUSP + ## + ############################################################# + if(CUSP_FOUND) + include_directories(${CUSP_INCLUDE_DIR}) + cuda_include_directories(${CUSP_INCLUDE_DIR}) + message(STATUS "StoRM (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}") + else() + message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find CUSP!") + endif() + + ############################################################# + ## + ## Thrust + ## + ############################################################# + if(THRUST_FOUND) + include_directories(${THRUST_INCLUDE_DIR}) + cuda_include_directories(${THRUST_INCLUDE_DIR}) + message(STATUS "StoRM (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}") + else() + message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find Thrust! Check your CUDA installation.") + endif() + + include_directories(${CUDA_INCLUDE_DIRS}) + include_directories(${ADDITIONAL_INCLUDE_DIRS}) + + cuda_add_library(${STORM_CUDA_LIB_NAME} + ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES} + ) + + message (STATUS "StoRM - Linking with CUDA") + list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME}) + include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/") +endif() \ No newline at end of file diff --git a/resources/3rdparty/carl b/resources/3rdparty/carl new file mode 160000 index 000000000..d67f98622 --- /dev/null +++ b/resources/3rdparty/carl @@ -0,0 +1 @@ +Subproject commit d67f986226cf846ba6366cdbe2abc21dff375542 diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake new file mode 100644 index 000000000..d63e855d3 --- /dev/null +++ b/resources/3rdparty/include_cudd.cmake @@ -0,0 +1,31 @@ +if(NOT AUTORECONF) + message(ERROR "Cannot find autoreconf, cannot compile cudd3") +endif() + + +ExternalProject_Add( + cudd3 + DOWNLOAD_COMMAND "" + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0 + PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 + UPDATE_COMMAND ${AUTORECONF} + CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} + BUILD_COMMAND make "CFLAGS=-O2 -w" + INSTALL_COMMAND make install + BUILD_IN_SOURCE 0 + LOG_CONFIGURE ON + LOG_BUILD ON + LOG_INSTALL ON +) + +# Do not use system CUDD, StoRM has a modified version +set(CUDD_INCLUDE_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/include) +set(CUDD_SHARED_LIBRARY ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib/libcudd${DYNAMIC_EXT}) +set(CUDD_STATIC_LIBRARY $${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/cudd-3.0.0/lib/libcudd${STATIC_EXT}) +set(CUDD_VERSION_STRING 3.0.0) +list(APPEND STORM_LINK_LIBRARIES ${CUDD_SHARED_LIBRARY}) +add_dependencies(resources cudd3) + +message(STATUS "StoRM - Linking with CUDD ${CUDD_VERSION_STRING}") +#message("StoRM - CUDD include dir: ${CUDD_INCLUDE_DIR}") +include_directories(${CUDD_INCLUDE_DIR}) \ No newline at end of file diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake new file mode 100644 index 000000000..2ac870b3d --- /dev/null +++ b/resources/3rdparty/include_glpk.cmake @@ -0,0 +1,28 @@ +find_package(GLPK QUIET) +if(GLPK_FOUND) + message (STATUS "StoRM - Using system version of GLPK") +else() + message (STATUS "StoRM - Using shipped version of GLPK") + ExternalProject_Add(glpk + DOWNLOAD_COMMAND "" + PREFIX ${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57 + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/glpk-4.57 + CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/glpk-4.57/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57 --libdir=${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER} + BUILD_COMMAND make "CFLAGS=-O2 -w" + INSTALL_COMMAND make install + BUILD_IN_SOURCE 0 + LOG_CONFIGURE ON + LOG_BUILD ON + LOG_INSTALL ON + ) + set(GLPK_LIBRARIES ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/lib/libglpk${DYNAMIC_EXT}) + set(GLPK_INCLUDE_DIR ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/include) + set(GLPK_VERSION_STRING 4.57) + add_dependencies(resources glpk) +endif() + +# Since there is a shipped version, always use GLPK +set(STORM_HAVE_GLPK ON) +message (STATUS "StoRM - Linking with glpk ${GLPK_VERSION_STRING}") +include_directories(${GLPK_INCLUDE_DIR}) +list(APPEND STORM_LINK_LIBRARIES ${GLPK_LIBRARIES}) diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake new file mode 100644 index 000000000..da33b18c7 --- /dev/null +++ b/resources/3rdparty/include_xerces.cmake @@ -0,0 +1,31 @@ +if(USE_XERCES) + find_package(Xerces QUIET REQUIRED) + if(XERCES_FOUND) + message(STATUS "StoRM - Use system version of xerces") + else() + message(STATUS "StoRM - Use shipped version of xerces") + ExternalProject_Add( + xercesc + SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/xercesc-3.1.2 + CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/xercesc-3.1.2/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2 --libdir=${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} CFLAGS=-O3 CXXFLAGS=-O3 + PREFIX ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2 + BUILD_COMMAND make + BUILD_IN_SOURCE 0 + LOG_CONFIGURE ON + LOG_BUILD ON + LOG_INSTALL ON + ) + + set(XERCES_ROOT ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2) + set(XERCESC_INCLUDE ${XERCES_ROOT}/include) + set(XERCES_LIBRARY_PATH ${XERCES_ROOT}/lib) + set(XERCESC_LIBRARIES ${XERCES_LIBRARY_PATH}/libxerces-c.a) + + add_dependencies(resources xercesc) + endif() + + message (STATUS "StoRM - Linking with xercesc") + set(STORM_HAVE_XERCES ON) + include_directories(${XERCESC_INCLUDE}) + list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES}) +endif(USE_XERCES) \ No newline at end of file diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 88e0a396f..f3c05d51a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -9,8 +9,10 @@ file(GLOB_RECURSE STORM_HEADERS_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) +file(GLOB_RECURSE STORM_DFT_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm-dyftee.cpp) file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) +file(GLOB_RECURSE STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp) file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp) @@ -20,6 +22,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_HELPER_FILES ${PROJECT_SOURCE_DIR}/sr file(GLOB STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp) +file(GLOB_RECURSE STORM_MODELCHECKER_EXPLORATION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp) file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) @@ -31,9 +34,16 @@ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOUR file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp) file(GLOB STORM_SETTINGS_MODULES_FILES ${PROJECT_SOURCE_DIR}/src/settings/modules/*.h ${PROJECT_SOURCE_DIR}/src/settings/modules/*.cpp) -file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) +file(GLOB STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp) +file(GLOB STORM_SOLVER_STATEELIMINATION_FILES ${PROJECT_SOURCE_DIR}/src/solver/stateelimination/*.h ${PROJECT_SOURCE_DIR}/src/solver/stateelimination/*.cpp) file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) -file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) +file(GLOB STORM_STORAGE_JANI_FILES ${PROJECT_SOURCE_DIR}/src/storage/jani/*.h ${PROJECT_SOURCE_DIR}/src/storage/jani/*.cpp) +file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp) +file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) +file(GLOB STORM_STORAGE_DFT_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/*.cpp) +file(GLOB STORM_STORAGE_DFT_ELEMENTS_FILES ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.h ${PROJECT_SOURCE_DIR}/src/storage/dft/elements/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_DD_CUDD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/cudd/*.cpp) +file(GLOB_RECURSE STORM_STORAGE_DD_SYLVAN_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/sylvan/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) @@ -48,12 +58,15 @@ list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_CLI}) set(STORM_LIB_HEADERS ${STORM_HEADERS}) list(REMOVE_ITEM STORM_LIB_HEADERS ${STORM_HEADERS_CLI}) set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE}) +set(STORM_DFT_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_DFT_MAIN_FILE}) set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI}) # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) +source_group(dft FILES ${STORM_DYFTTEE_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) +source_group(generator FILES ${STORM_GENERATOR_FILES}) source_group(cli FILES ${STORM_CLI_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(logic FILES ${STORM_LOGIC_FILES}) @@ -63,6 +76,7 @@ source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES}) source_group(modelchecker\\prctl\\helper FILES ${STORM_MODELCHECKER_PRCTL_HELPER_FILES}) source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES}) source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FILES}) +source_group(modelchecker\\exploration FILES ${STORM_MODELCHECKER_EXPLORATION_FILES}) source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES}) source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES}) source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES}) @@ -76,11 +90,18 @@ source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(settings FILES ${STORM_SETTINGS_FILES}) source_group(settings\\modules FILES ${STORM_SETTINGS_MODULES_FILES}) source_group(solver FILES ${STORM_SOLVER_FILES}) +source_group(solver\\stateelimination FILES ${STORM_SOLVER_STATEELIMINATION_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) +source_group(storage\\bisimulation FILES ${STORM_STORAGE_BISIMULATION_FILES}) source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) +source_group(storage\\dd\\cudd FILES ${STORM_STORAGE_DD_CUDD_FILES}) +source_group(storage\\dd\\sylvan FILES ${STORM_STORAGE_DD_SYLVAN_FILES}) source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) +source_group(storage\\jani FILES ${STORM_STORAGE_JANI_FILES}) +source_group(storage\\dft FILES ${STORM_STORAGE_DFT_FILES}) +source_group(storage\\dft\\elements FILES ${STORM_STORAGE_DFT_ELEMENTS_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) # Add custom additional include or link directories @@ -100,18 +121,22 @@ endif(ADDITIONAL_LINK_DIRS) ## All link_directories() calls MUST be made before this point # ## # ############################################################################### -add_library(storm ${STORM_LIB_SOURCES} ${STORM_LIB_HEADERS} ${STORM_GENERATED_SOURCES}) # Adding headers for xcode -add_dependencies(storm xercesc) +add_library(storm SHARED ${STORM_LIB_SOURCES} ${STORM_LIB_HEADERS}) # Adding headers for xcode +add_dependencies(storm sylvan) +add_dependencies(storm resources) add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) target_link_libraries(storm-main storm) # Adding headers for xcode set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm") +add_executable(storm-dft-main ${STORM_DFT_MAIN_SOURCES} ${STORM_MAIN_HEADERS}) +target_link_libraries(storm-dft-main storm) # Adding headers for xcode +set_target_properties(storm-dft-main PROPERTIES OUTPUT_NAME "storm-dft") target_link_libraries(storm ${STORM_LINK_LIBRARIES}) -INSTALL(TARGETS storm-main +INSTALL(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib ARCHIVE DESTINATION lib diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 30a4157cd..1a49b56c1 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -4,8 +4,11 @@ #include #include + #include +#define BOOST_VARIANT_USE_RELAXED_GET_BY_DEFAULT + #include "src/storage/expressions/Expression.h" #include "src/storage/BitVectorHashMap.h" #include "src/storage/expressions/ExpressionEvaluator.h" diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 7817dc644..90f858756 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -72,7 +72,7 @@ namespace storm { std::vector bMarkovian(markovianNonGoalStates.getNumberOfSetBits()); // Compute the two fixed right-hand side vectors, one for Markovian states and one for the probabilistic ones. - std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowSumVector(probabilisticNonGoalStates, goalStates); + std::vector bProbabilisticFixed = transitionMatrix.getConstrainedRowGroupSumVector(probabilisticNonGoalStates, goalStates); std::vector bMarkovianFixed; bMarkovianFixed.reserve(markovianNonGoalStates.getNumberOfSetBits()); for (auto state : markovianNonGoalStates) { diff --git a/src/utility/sylvan.h b/src/utility/sylvan.h index ccaffe097..babdc22fd 100644 --- a/src/utility/sylvan.h +++ b/src/utility/sylvan.h @@ -7,9 +7,13 @@ #pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" #pragma clang diagnostic ignored "-Wdeprecated-register" #pragma clang diagnostic ignored "-Wc99-extensions" +#pragma clang diagnostic ignored "-Wunknown-pragmas" +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Wpedantic" #include "sylvan_obj.hpp" +#pragma GCC diagnostic pop #pragma clang diagnostic pop #endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */ \ No newline at end of file