CMAKE: Added option to include and link against Spot

Conflicts:
	CMakeLists.txt

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)

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

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()

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)

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