From efeeea0d54b0850f2a8593fcd1799e436e21ac69 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 4 Aug 2021 16:33:07 +0200 Subject: [PATCH] Spot: re-iterated cmake interface to hopefully make it more clean. Added documentation on how to update spot --- .github/workflows/buildtest.yml | 4 ++-- CHANGELOG.md | 2 +- CMakeLists.txt | 5 ++--- doc/update_resources.md | 4 ++++ resources/3rdparty/include_spot.cmake | 18 ++++-------------- 5 files changed, 13 insertions(+), 20 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index b183c985d..a231f2430 100644 --- a/.github/workflows/buildtest.yml +++ b/.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" diff --git a/CHANGELOG.md b/CHANGELOG.md index d0c6f96ff..575df222b 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/CMakeLists.txt b/CMakeLists.txt index 5442379a6..c10d4f292 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/doc/update_resources.md b/doc/update_resources.md index 2c5f10dbe..5db30a8c2 100644 --- a/doc/update_resources.md +++ b/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`. \ No newline at end of file diff --git a/resources/3rdparty/include_spot.cmake b/resources/3rdparty/include_spot.cmake index e64bad090..eaca6bc5a 100644 --- a/resources/3rdparty/include_spot.cmake +++ b/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