Spot: re-iterated cmake interface to hopefully make it more clean. Added documentation on how to update spot

.github/workflows/buildtest.yml

@@ -19,8 +19,8 @@ env:
   NR_JOBS: "2"
 
   # cmake arguments
-  CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT=ON"
-  CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT=ON"
+  CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT_SHIPPED=ON"
+  CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_PORTABLE=ON -DSTORM_USE_SPOT_SHIPPED=ON"
 
   CARL_CMAKE_DEBUG: "-DCMAKE_BUILD_TYPE=Debug -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON"
   CARL_CMAKE_RELEASE: "-DCMAKE_BUILD_TYPE=Release -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DBUILD_ADDONS=ON -DBUILD_ADDON_PARSER=ON"

CHANGELOG.md

@@ -10,7 +10,7 @@ Version 1.6.x
 -------------
 ## Version 1.6.4 (20xx/xx)
 - Added support for model checking LTL properties in the sparse (and dd-to-sparse) engine. Requires building with Spot.
-- Added cmake options `STORM_USE_SPOT` and `STORM_FORCE_SHIPPED_SPOT` to facilitate building Storm with [Spot](https://spot.lrde.epita.fr/).
+- Added cmake options `STORM_USE_SPOT_SYSTEM` and `STORM_USE_SPOT_SHIPPED` to facilitate building Storm with [Spot](https://spot.lrde.epita.fr/).
 - Improved parsing of formulas in PRISM-style syntax.
 - Added export of schedulers that use memory (in particular optimizing schedulers for LTL properties)
 - Added support for PRISM models that use unbounded integer variables.

CMakeLists.txt

@@ -50,9 +50,8 @@ 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)
-option(STORM_FORCE_SHIPPED_SPOT "Sets whether the Spot sources should be downloaded and installed." OFF)
+option(STORM_USE_SPOT_SYSTEM "Sets whether the system version of Spot should be included (if found)." ON)
+option(STORM_USE_SPOT_SHIPPED "Sets whether Spot should be downloaded and installed (if system version is not available or not used)." 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)

doc/update_resources.md

@@ -26,3 +26,7 @@ grep GOOGLETEST_VERSION $STORM_DIR/resources/3rdparty/googletest/CMakeLists.txt
 ```
 
 We add some extra code to gtest located in `$STORM_DIR/src/test/storm_gtest.h`. Note that our code might not be compatible with future versions of gtest.
+
+## Spot
+
+To update (shipped version of Spot), just change the url in `$STORM_DIR/resources/3rdparty/include_spot.cmake`.

resources/3rdparty/include_spot.cmake

@@ -1,16 +1,6 @@
 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)
-
+if(STORM_USE_SPOT_SYSTEM)
     # try to find Spot on the system
     if (NOT "${SPOT_ROOT}" STREQUAL "")
         message(STATUS "Storm - searching for Spot in ${SPOT_ROOT}")
@@ -23,14 +13,14 @@ if(STORM_USE_SPOT AND NOT STORM_SHIPPED_SPOT AND NOT STORM_FORCE_SHIPPED_SPOT)
     if (SPOT_FOUND)
         message(STATUS "Storm - Using system version of 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")
+    elseif(NOT STORM_USE_SPOT_SHIPPED)
+        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_USE_SPOT_SHIPPED to install Spot automatically. If you already installed Spot, consider setting cmake option SPOT_ROOT. Unset STORM_USE_SPOT_SYSTEM to silence this warning.")
     endif()
 elseif()
 endif()
 
 set(STORM_SHIPPED_SPOT OFF)
-if(STORM_FORCE_SHIPPED_SPOT OR (STORM_FORCE_LTL_SUPPORT AND NOT STORM_HAVE_SPOT))
+if(STORM_USE_SPOT_SHIPPED AND NOT STORM_HAVE_SPOT)
 
     # download and install shipped Spot
     ExternalProject_Add(spot