diff --git a/CMakeLists.txt b/CMakeLists.txt index 85968256d..fd37f01f5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -49,7 +49,11 @@ MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL) option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF) mark_as_advanced(USE_SMTRAT) option(USE_HYPRO "Sets whether HyPro should be included." OFF) -mark_as_advanced(USE_HYPRO) +option(STORM_FORCE_LTL_SUPPORT "Sets whether support for LTL model checking needs to be included." OFF) +option(STORM_USE_SPOT "Sets whether Spot should be included." ON) +MARK_AS_ADVANCED(STORM_USE_SPOT) +option(STORM_FORCE_SHIPPED_SPOT "Sets whether the Spot sources should be downloaded and installed." OFF) +MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_SPOT) option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON) option(FORCE_COLOR "Force color output" OFF) mark_as_advanced(FORCE_COLOR) @@ -71,6 +75,8 @@ set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optiona set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(CUDA_ROOT "" CACHE STRING "The hint to the root directory of CUDA (optional).") set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).") +set(SPOT_ROOT "" CACHE STRING "The hint to the root directory of Spot (optional).") +MARK_AS_ADVANCED(SPOT_ROOT) option(STORM_LOAD_QVBS "Sets whether the Quantitative Verification Benchmark Set (QVBS) should be downloaded." OFF) set(STORM_QVBS_ROOT "" CACHE STRING "The root directory of the Quantitative Verification Benchmark Set (QVBS) in case it should not be downloaded (optional).") MARK_AS_ADVANCED(STORM_QVBS_ROOT) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 50a220135..cdc18db60 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -514,6 +514,15 @@ endif() include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake) + +############################################################# +## +## Spot +## +############################################################# + +include(${STORM_3RDPARTY_SOURCE_DIR}/include_spot.cmake) + ############################################################# ## ## Sylvan diff --git a/resources/3rdparty/include_SPOT.cmake b/resources/3rdparty/include_SPOT.cmake new file mode 100644 index 000000000..0332bdd4e --- /dev/null +++ b/resources/3rdparty/include_SPOT.cmake @@ -0,0 +1,64 @@ +set(STORM_HAVE_SPOT OFF) + + +if (STORM_FORCE_SHIPPED_SPOT AND NOT STORM_USE_SPOT) + message(FATAL_ERROR "Storm - Incompatible cmake options: STORM_FORCE_SHIPPED_SPOT=ON and STORM_USE_SPOT=OFF.") +endif() + +if (STORM_FORCE_LTL_SUPPORT AND NOT STORM_USE_SPOT) + message(FATAL_ERROR "Storm - Incompatible cmake options: STORM_FORCE_LTL_SUPPORT=ON and STORM_USE_SPOT=OFF. LTL support requires Spot.") +endif() + +if(STORM_USE_SPOT AND NOT STORM_SHIPPED_SPOT AND NOT STORM_FORCE_SHIPPED_SPOT) + + # try to find Spot on the system + if (NOT "${SPOT_ROOT}" STREQUAL "") + message(STATUS "Storm - searching for Spot in ${SPOT_ROOT}") + find_package(SPOT QUIET PATHS ${SPOT_ROOT} NO_DEFAULT_PATH) + endif() + if (NOT SPOT_FOUND) + find_package(SPOT QUIET) + endif() + + if (SPOT_FOUND) + message(STATUS "Storm - Linking with shipped Spot ${SPOT_VERSION} (include: ${SPOT_INCLUDE_DIR}, library: ${SPOT_LIBRARIES}).") + set(STORM_HAVE_SPOT ON) + elseif(NOT STORM_FORCE_LTL_SUPPORT) + message (WARNING "Storm - Could not find Spot. Model checking of LTL formulas (beyond PCTL) will not be supported. You may want to set cmake option STORM_FORCE_LTL_SUPPORT to install Spot automatically. If you already installed Spot, consider setting cmake option SPOT_ROOT") + endif() +elseif() +endif() + +set(STORM_SHIPPED_SPOT OFF) +if(STORM_FORCE_SHIPPED_SPOT OR (STORM_FORCE_LTL_SUPPORT AND NOT STORM_HAVE_SPOT)) + + # download and install shipped Spot + ExternalProject_Add(spot + URL http://www.lrde.epita.fr/dload/spot/spot-2.9.6.tar.gz # When updating, also change version output below + DOWNLOAD_NO_PROGRESS TRUE + DOWNLOAD_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src + SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/spot_src + PREFIX ${STORM_3RDPARTY_BINARY_DIR}/spot + CONFIGURE_COMMAND ${STORM_3RDPARTY_BINARY_DIR}/spot_src/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/spot --disable-python + BUILD_COMMAND make -j + INSTALL_COMMAND make install + LOG_CONFIGURE ON + LOG_BUILD ON + LOG_INSTALL ON + BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT} + ) + add_dependencies(resources spot) + set(SPOT_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/include/") + set(SPOT_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/") + set(SPOT_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT}) + set(STORM_HAVE_SPOT ON) + set(STORM_SHIPPED_SPOT ON) + + message(STATUS "Storm - Linking with shipped Spot 2.9.6 (include: ${SPOT_INCLUDE_DIR}, library ${SPOT_LIBRARIES}).") + +endif() + +if (STORM_HAVE_SPOT) + include_directories("${SPOT_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${SPOT_LIBRARIES}) +endif() diff --git a/resources/cmake/find_modules/FindSPOT.cmake b/resources/cmake/find_modules/FindSPOT.cmake new file mode 100644 index 000000000..383793a09 --- /dev/null +++ b/resources/cmake/find_modules/FindSPOT.cmake @@ -0,0 +1,42 @@ +# - Try to find libspot +# Once done this will define +# SPOT_FOUND - System has glpk +# SPOT_INCLUDE_DIR - The glpk include directory +# SPOT_LIBRARIES - The libraries needed to use glpk +# SPOT_VERSION - The version of spot + +# use pkg-config to get the directories and then use these values +message(STATUS "FIND SPOT") + +# in the find_path() and find_library() calls +find_package(PkgConfig QUIET) +PKG_CHECK_MODULES(PC_SPOT QUIET spot) + +find_path(SPOT_INCLUDE_DIR NAMES spot/misc/_config.h + HINTS + ${PC_SPOT_INCLUDEDIR} + ${PC_SPOT_INCLUDE_DIRS} + ) + +find_library(SPOT_LIBRARIES NAMES spot + HINTS + ${PC_SPOT_LIBDIR} + ${PC_SPOT_LIBRARY_DIRS} + ) + +if(PC_SPOT_VERSION) + set(SPOT_VERSION ${PC_SPOT_VERSION}) +elseif(SPOT_INCLUDE_DIR AND EXISTS "${SPOT_INCLUDE_DIR}/spot/misc/_config.h") + file(STRINGS "${SPOT_INCLUDE_DIR}/spot/misc/_config.h" SPOT_VERSION + REGEX "^#define[\t ]+SPOT_VERSION[\t ]+\".+\"") + string(REGEX REPLACE "^#define[\t ]+SPOT_VERSION[\t ]+\"(.+)\"" "\\1" SPOT_VERSION "${SPOT_VERSION}") +endif() + +# handle the QUIETLY and REQUIRED arguments and set SPOT_FOUND to TRUE if +# all listed variables are TRUE +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(SPOT + REQUIRED_VARS SPOT_LIBRARIES SPOT_INCLUDE_DIR + VERSION_VAR SPOT_VERSION) + +mark_as_advanced(SPOT_INCLUDE_DIR SPOT_LIBRARIES) diff --git a/storm-config.h.in b/storm-config.h.in index 78164aa05..d1da99a22 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -85,6 +85,14 @@ #cmakedefine STORM_HAVE_XERCES +// Whether Spot is available and to be used +#cmakedefine STORM_HAVE_SPOT + +// Whether LTL model checking shall be enabled +#ifdef STORM_HAVE_SPOT + #define STORM_HAVE_LTL_MODELCHECKING_SUPPORT +#endif // STORM_HAVE_SPOT + // Whether smtrat is available and to be used. #cmakedefine STORM_HAVE_SMTRAT