From a9d6d80ef0e6e89a19b48a5fa75661884ce04b3d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 1 Jun 2017 13:20:40 +0200 Subject: [PATCH 1/3] Warning in cmake if Z3 is not found --- resources/3rdparty/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 9ede52524..bc4f11d84 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -155,6 +155,8 @@ if(Z3_FOUND) add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS}) list(APPEND STORM_DEP_TARGETS z3_SHARED) +else() + message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.") endif(Z3_FOUND) ############################################################# From b695dd48fb6bfc6b5d43b9ceae7cf592c2b7afcf Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 1 Jun 2017 14:24:44 +0200 Subject: [PATCH 2/3] Fixed assertion to allow timebound 0 --- src/storm/logic/BoundedUntilFormula.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index da7ac1862..10cd7f33e 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -105,7 +105,7 @@ namespace storm { template <> double BoundedUntilFormula::getNonStrictUpperBound() const { double bound = getUpperBound(); - STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + STORM_LOG_THROW(!isUpperBoundStrict() || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); return bound; } From b76ee0210a720809b191c4f4d2a4aff1b51f7e8e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 1 Jun 2017 14:38:54 +0200 Subject: [PATCH 3/3] Fixed setting cmake flags for building shipped carl --- resources/3rdparty/CMakeLists.txt | 2 +- resources/3rdparty/carl/CMakeLists.txt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index bc4f11d84..b7f1b436c 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -225,7 +225,7 @@ if(USE_CARL) message("START CARL CONFIG PROCESS") file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) execute_process( - COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DUSE_CLN_NUMBERS=ON" "-DUSE_GINAC=ON" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON" + COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index 749b561aa..6bbd09337 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -12,7 +12,7 @@ ExternalProject_Add(carl-config PREFIX here SOURCE_DIR source_dir BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl - CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=1 -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl + CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=1 -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl BUILD_IN_SOURCE 0 LOG_UPDATE OFF LOG_CONFIGURE OFF