From 9e398ffaab09fec2bb4593d27982c4644371fdb4 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Jun 2018 15:07:42 +0200 Subject: [PATCH 1/5] Minor improvements for some CMake output --- CMakeLists.txt | 14 +++++++------- resources/3rdparty/CMakeLists.txt | 14 +++++++------- resources/3rdparty/carl/CMakeLists.txt | 4 ++-- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ca3b9b7e..ee6c1117c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -86,7 +86,7 @@ foreach(p LIB BIN INCLUDE CMAKE) endif() endforeach() -message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}") +message(STATUS "Storm - CMake install dir: ${CMAKE_INSTALL_DIR}") # If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version. if (STORM_DEVELOPER) @@ -153,15 +153,15 @@ elseif (WIN32) set(STATIC_EXT ".lib") set(LIB_PREFIX "") endif() -message(STATUS "Assuming extension for shared libraries: ${DYNAMIC_EXT}") -message(STATUS "Assuming extension for static libraries: ${STATIC_EXT}") +message(STATUS "Storm - Assuming extension for shared libraries: ${DYNAMIC_EXT}") +message(STATUS "Storm - Assuming extension for static libraries: ${STATIC_EXT}") if(BUILD_SHARED_LIBS) set(LIB_EXT ${DYNAMIC_EXT}) - message(STATUS "Build dynamic libraries.") + message(STATUS "Storm - Build dynamic libraries.") else() set(LIB_EXT ${STATIC_EXT}) - message(STATUS "Build static libraries.") + message(STATUS "Storm - Build static libraries.") endif() ############################################################# @@ -443,7 +443,7 @@ if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND") set(STORM_VERSION_SOURCE "VersionSource::Static") set(STORM_VERSION_COMMITS_AHEAD "boost::none") include(version.cmake) - message(WARNING "Storm - git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") + message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") endif() # check whether there is a label ('alpha', 'pre', etc.) @@ -473,7 +473,7 @@ endif() set(STORM_VERSION "${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_DEV_PATCH}") set(STORM_VERSION_STRING "${STORM_VERSION}${STORM_VERSION_LABEL_STRING}${STORM_VERSION_DEV_STRING}") -message(STATUS "Storm - version is ${STORM_VERSION_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}${STORM_VERSION_LABEL_STRING} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") +message(STATUS "Storm - Version is ${STORM_VERSION_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}${STORM_VERSION_LABEL_STRING} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") # Configure a header file to pass some of the CMake settings to the source code diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 5957f3b51..caaa2a0f1 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -239,16 +239,16 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) else() set(STORM_SHIPPED_CARL ON) # The first external project will be built at *configure stage* - message("START CARL CONFIG PROCESS") - file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) + message(STATUS "Carl - Start of 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}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) - + if(NOT carlconfig_result) - message("${carlconfig_out}") + message(STATUS "${carlconfig_out}") endif() execute_process( COMMAND ${CMAKE_COMMAND} --build . --target carl-config @@ -257,10 +257,10 @@ else() RESULT_VARIABLE carlconfig_result ) if(NOT carlconfig_result) - message("${carlconfig_out}") + message(STATUS "${carlconfig_out}") endif() - message("END CARL CONFIG PROCESS") - + message(STATUS "Carl - End of config process") + message(STATUS "Storm - Using shipped version of carl.") ExternalProject_Add( carl diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index 4b819682d..3bb50d1b1 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -4,7 +4,7 @@ include(ExternalProject) option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir") -message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR}) +message(STATUS "Carl - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}") ExternalProject_Add(carl-config GIT_REPOSITORY https://github.com/smtrat/carl @@ -22,4 +22,4 @@ ExternalProject_Add(carl-config add_custom_target(build-carl) add_dependencies(build-carl carl-config) -message("done") +message(STATUS "Carl - Finished configuration.") From afb0be124565e466ed9f5788e88fa34de82cb410 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Jun 2018 15:08:14 +0200 Subject: [PATCH 2/5] Fixed missing dependencies to storm-parsers --- src/storm-dft/CMakeLists.txt | 2 +- src/storm-parsers/CMakeLists.txt | 2 +- src/storm-pgcl/CMakeLists.txt | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index f191e537f..48a046238 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -17,7 +17,7 @@ set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-dft) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-dft PUBLIC storm storm-gspn ${STORM_DFT_LINK_LIBRARIES}) +target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-parsers ${STORM_DFT_LINK_LIBRARIES}) # Install storm headers to include directory. foreach(HEADER ${STORM_DFT_HEADERS}) diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt index d459345e4..24d9532b5 100644 --- a/src/storm-parsers/CMakeLists.txt +++ b/src/storm-parsers/CMakeLists.txt @@ -10,7 +10,7 @@ file(GLOB_RECURSE STORM_PARSER_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-parsers/* # Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm-parsers/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) -# Create storm-dft. +# Create storm-parsers. add_library(storm-parsers SHARED ${STORM_PARSER_SOURCES} ${STORM_PARSER_HEADERS}) # Remove define symbol for shared libstorm. diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt index 059bff395..7b86f73c3 100644 --- a/src/storm-pgcl/CMakeLists.txt +++ b/src/storm-pgcl/CMakeLists.txt @@ -10,7 +10,7 @@ file(GLOB_RECURSE STORM_PGCL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pgcl/*/*.h) # Create storm-pgcl. add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS}) -target_link_libraries(storm-pgcl storm) +target_link_libraries(storm-pgcl storm storm-parsers) # installation install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) From a6e6d5993f9b3c80db73a25661f3dfce067d158c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 13 Jun 2018 16:37:45 +0200 Subject: [PATCH 3/5] Travis: set unlimited clone depth to allow versioning with git describe --- .travis.yml | 5 ++++- travis/generate_travis.py | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 1074ba368..8a5dd952d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -9,6 +9,9 @@ sudo: required dist: trusty language: cpp +git: + depth: false + # Enable caching cache: timeout: 1000 @@ -25,7 +28,7 @@ notifications: on_failure: always on_success: change recipients: - secure: "BoMQTBWnkh4ZLIHEaKu0tAKDohhVmOQ2pz/fjc+ScKG8mtvXqtpx0TiyePOUV1MuYNZiAP7x4mwABcoid55SwZ4+LPjd8uxXNfOji9B9GW5YqbqRvAeh7Es7dx48MyLYPIezjoryHH9R3Q2zZ9gmxgtw5eirjURcLNTXpKAwq/oOsKvh+vhOx4Qierw98wEXjMV7ipBzE4cfkgUbbX7oxGh1nsAsCew+rRmNLijfmE9tctYdH5W0wE+zC9ik+12Xyk3FwsDIABirPHfeCcEl+b9I0h1a2vZSZIA+sCDkIGKTiv9pCnsthn5LJc9pMLX7B/Wf6xLGMzpSiw3P1ZzjXpOE026WuyhTMVXqZYvbl7cJoNZiLCfTYg3MQVq5NHkq0h0jInIH7QlZYd0hZPOGONwdy17O1QmnX2Weq6G+Ps9siLVKFba37+y5PfRYkiUatJvDf2f7Jdxye6TWrUmlxQkAvs65ioyr8doad7IT1/yaGr/rBpXeQqZp6zNoMYr/cCRAYX6nOrnSszgiIWEc8QMMx+G31v77Uvd++9VG4MG9gbdpexpfYRNzKAxDarSaYEOuaWm2Z6R87bpNcjA+tW0hnBHBzRx0NFYYqXyW0tpVO9+035A9CHrLDLz77r4jJttcRvrP2rTbTBiwuhpmiufRyk3BuWlgzU3yaSuQV3M=" + - secure: "VWnsiQkt1xjgRo1hfNiNQqvLSr0fshFmLV7jJlUixhCr094mgD0U2bNKdUfebm28Byg9UyDYPbOFDC0sx7KydKiL1q7FKKXkyZH0k04wUu8XiNw+fYkDpmPnQs7G2n8oJ/GFJnr1Wp/1KI3qX5LX3xot4cJfx1I5iFC2O+p+ng6v/oSX+pewlMv4i7KL16ftHHHMo80N694v3g4B2NByn4GU2/bjVQcqlBp/TiVaUa5Nqu9DxZi/n9CJqGEaRHOblWyMO3EyTZsn45BNSWeQ3DtnMwZ73rlIr9CaEgCeuArc6RGghUAVqRI5ao+N5apekIaILwTgL6AJn+Lw/+NRPa8xclgd0rKqUQJMJCDZKjKz2lmIs3bxfELOizxJ3FJQ5R95FAxeAZ6rb/j40YqVVTw2IMBDnEE0J5ZmpUYNUtPti/Adf6GD9Fb2y8sLo0XDJzkI8OxYhfgjSy5KYmRj8O5MXcP2MAE8LQauNO3MaFnL9VMVOTZePJrPozQUgM021uyahf960+QNI06Uqlmg+PwWkSdllQlxHHplOgW7zClFhtSUpnJxcsUBzgg4kVg80gXUwAQkaDi7A9Wh2bs+TvMlmHzBwg+2SaAfWDgjeJIeOaipDkF1uSGzC+EHAiiKYMLd4Aahoi8SuelJUucoyJyLAq00WdUFQIh/izVhM4Y=" # # Configurations diff --git a/travis/generate_travis.py b/travis/generate_travis.py index ac4e89417..49723a13c 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -44,6 +44,9 @@ if __name__ == "__main__": s += "dist: trusty\n" s += "language: cpp\n" s += "\n" + s += "git:\n" + s += " depth: false\n" + s += "\n" s += "# Enable caching\n" s += "cache:\n" s += " timeout: 1000\n" @@ -61,7 +64,7 @@ if __name__ == "__main__": s += " on_failure: always\n" s += " on_success: change\n" s += " recipients:\n" - s += ' secure: "BoMQTBWnkh4ZLIHEaKu0tAKDohhVmOQ2pz/fjc+ScKG8mtvXqtpx0TiyePOUV1MuYNZiAP7x4mwABcoid55SwZ4+LPjd8uxXNfOji9B9GW5YqbqRvAeh7Es7dx48MyLYPIezjoryHH9R3Q2zZ9gmxgtw5eirjURcLNTXpKAwq/oOsKvh+vhOx4Qierw98wEXjMV7ipBzE4cfkgUbbX7oxGh1nsAsCew+rRmNLijfmE9tctYdH5W0wE+zC9ik+12Xyk3FwsDIABirPHfeCcEl+b9I0h1a2vZSZIA+sCDkIGKTiv9pCnsthn5LJc9pMLX7B/Wf6xLGMzpSiw3P1ZzjXpOE026WuyhTMVXqZYvbl7cJoNZiLCfTYg3MQVq5NHkq0h0jInIH7QlZYd0hZPOGONwdy17O1QmnX2Weq6G+Ps9siLVKFba37+y5PfRYkiUatJvDf2f7Jdxye6TWrUmlxQkAvs65ioyr8doad7IT1/yaGr/rBpXeQqZp6zNoMYr/cCRAYX6nOrnSszgiIWEc8QMMx+G31v77Uvd++9VG4MG9gbdpexpfYRNzKAxDarSaYEOuaWm2Z6R87bpNcjA+tW0hnBHBzRx0NFYYqXyW0tpVO9+035A9CHrLDLz77r4jJttcRvrP2rTbTBiwuhpmiufRyk3BuWlgzU3yaSuQV3M="\n' + s += ' - secure: "VWnsiQkt1xjgRo1hfNiNQqvLSr0fshFmLV7jJlUixhCr094mgD0U2bNKdUfebm28Byg9UyDYPbOFDC0sx7KydKiL1q7FKKXkyZH0k04wUu8XiNw+fYkDpmPnQs7G2n8oJ/GFJnr1Wp/1KI3qX5LX3xot4cJfx1I5iFC2O+p+ng6v/oSX+pewlMv4i7KL16ftHHHMo80N694v3g4B2NByn4GU2/bjVQcqlBp/TiVaUa5Nqu9DxZi/n9CJqGEaRHOblWyMO3EyTZsn45BNSWeQ3DtnMwZ73rlIr9CaEgCeuArc6RGghUAVqRI5ao+N5apekIaILwTgL6AJn+Lw/+NRPa8xclgd0rKqUQJMJCDZKjKz2lmIs3bxfELOizxJ3FJQ5R95FAxeAZ6rb/j40YqVVTw2IMBDnEE0J5ZmpUYNUtPti/Adf6GD9Fb2y8sLo0XDJzkI8OxYhfgjSy5KYmRj8O5MXcP2MAE8LQauNO3MaFnL9VMVOTZePJrPozQUgM021uyahf960+QNI06Uqlmg+PwWkSdllQlxHHplOgW7zClFhtSUpnJxcsUBzgg4kVg80gXUwAQkaDi7A9Wh2bs+TvMlmHzBwg+2SaAfWDgjeJIeOaipDkF1uSGzC+EHAiiKYMLd4Aahoi8SuelJUucoyJyLAq00WdUFQIh/izVhM4Y="\n' s += "\n" s += "#\n" s += "# Configurations\n" From cdfa32846463872bfa51a87c86c09bd14e297879 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jun 2018 10:57:52 +0200 Subject: [PATCH 4/5] first attempt at adapting to Z3 interface change --- resources/3rdparty/CMakeLists.txt | 9 +++++++++ src/storm/adapters/Z3ExpressionAdapter.cpp | 19 ++++++++++++++----- .../DynamicStatePriorityQueue.h | 2 +- .../MaximalEndComponentDecompositionTest.cpp | 4 ++-- src/test/storm/utility/KSPTest.cpp | 4 ++-- storm-config.h.in | 7 +++++++ 6 files changed, 35 insertions(+), 10 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index caaa2a0f1..18a68a23f 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -168,6 +168,15 @@ else() message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.") endif(Z3_FOUND) +# split Z3 version into its components +string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION}) +list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR) +list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR) +list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH) +if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1") + set(STORM_Z3_API_USES_STANDARD_INTEGERS ON) +endif() + ############################################################# ## ## glpk diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index c7e27756d..fec9068b0 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -12,6 +12,15 @@ namespace storm { namespace adapters { #ifdef STORM_HAVE_Z3 + +#ifdef STORM_Z3_API_USES_STANDARD_INTEGERS + typedef int64_t Z3_SIGNED_INTEGER; + typedef int64_t Z3_UNSIGNED_INTEGER; +#else + typedef long long Z3_SIGNED_INTEGER; + typedef unsigned long long Z3_UNSIGNED_INTEGER; +#endif + Z3ExpressionAdapter::Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context) : manager(manager), context(context), additionalAssertions(), variableToExpressionMapping() { // Intentionally left empty. } @@ -133,17 +142,17 @@ namespace storm { case Z3_OP_ANUM: // Arithmetic numeral. if (expr.is_int() && expr.is_const()) { - long long value; + Z3_SIGNED_INTEGER value; if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) { return manager.integer(value); } else { STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer."); } } else if (expr.is_real() && expr.is_const()) { - long long num; - long long den; + Z3_SIGNED_INTEGER num; + Z3_SIGNED_INTEGER den; if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { - return manager.rational(storm::utility::convertNumber((int_fast64_t) num) / storm::utility::convertNumber((int_fast64_t) den)); + return manager.rational(storm::utility::convertNumber(static_cast(num)) / storm::utility::convertNumber(static_cast(den))); } else { return manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); } @@ -304,7 +313,7 @@ namespace storm { return cacheIt->second; } - z3::expr result = context.int_val(static_cast(expression.getValue())); + z3::expr result = context.int_val(static_cast(expression.getValue())); expressionCache.emplace(&expression, result); return result; diff --git a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h index 0ac38769d..4065ee265 100644 --- a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h +++ b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h @@ -17,7 +17,7 @@ namespace storm { namespace stateelimination { struct PriorityComparator { - bool operator()(std::pair const& first, std::pair const& second) { + bool operator()(std::pair const& first, std::pair const& second) const { return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; } }; diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index b30b5259b..ced1cd6b0 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -148,7 +148,7 @@ TEST(MaximalEndComponentDecomposition, Example1) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); - EXPECT_EQ(mecDecomposition.size(), 2); + EXPECT_EQ(2ull, mecDecomposition.size()); ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{3}); @@ -167,7 +167,7 @@ TEST(MaximalEndComponentDecomposition, Example2) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); - EXPECT_EQ(mecDecomposition.size(), 2); + EXPECT_EQ(2ull, mecDecomposition.size()); ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{4}); diff --git a/src/test/storm/utility/KSPTest.cpp b/src/test/storm/utility/KSPTest.cpp index dfe14e817..d584a7660 100644 --- a/src/test/storm/utility/KSPTest.cpp +++ b/src/test/storm/utility/KSPTest.cpp @@ -81,7 +81,7 @@ TEST(KSPTest, kspStateSet) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); auto bv = spg.getStates(7); - EXPECT_EQ(50, bv.getNumberOfSetBits()); + EXPECT_EQ(50ull, bv.getNumberOfSetBits()); // The result may sadly depend on the compiler/system, so checking a particular outcome is not feasible. // storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); @@ -97,7 +97,7 @@ TEST(KSPTest, kspPathAsList) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); auto list = spg.getPathAsList(7); - EXPECT_EQ(50, list.size()); + EXPECT_EQ(50ull, list.size()); // TODO: use path that actually has a loop or something to make this more interesting // auto reference = storm::utility::ksp::OrderedStateList{296, 288, 281, 272, 266, 260, 253, 245, 238, 230, 224, 218, 211, 203, 196, 188, 182, 176, 169, 161, 154, 146, 140, 134, 127, 119, 112, 104, 98, 92, 85, 77, 70, 81, 74, 65, 58, 52, 45, 37, 30, 22, 17, 12, 9, 6, 4, 2, 1, 0}; diff --git a/storm-config.h.in b/storm-config.h.in index b0290b751..55d2247d3 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -41,6 +41,13 @@ // Whether the optimization feature of Z3 is available and to be used (define/undef) #cmakedefine STORM_HAVE_Z3_OPTIMIZE +// Version of Z3 used by Storm. +#define STORM_Z3_VERSION_MAJOR @STORM_Z3_VERSION_MAJOR@ +#define STORM_Z3_VERSION_MINOR @STORM_Z3_VERSION_MINOR@ +#define STORM_Z3_VERSION_PATCH @STORM_Z3_VERSION_PATCH@ +#define STORM_Z3_VERSION @Z3_VERSION@ +#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS + // Whether MathSAT is available and to be used (define/undef) #cmakedefine STORM_HAVE_MSAT From dfc0141894c34a1b8c4014adee82677f0595bad5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jun 2018 13:25:21 +0200 Subject: [PATCH 5/5] minor fix to Z3 API modification --- src/storm/adapters/Z3ExpressionAdapter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index fec9068b0..8a7f55bf5 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -1,5 +1,7 @@ #include "storm/adapters/Z3ExpressionAdapter.h" +#include + #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" @@ -15,7 +17,7 @@ namespace storm { #ifdef STORM_Z3_API_USES_STANDARD_INTEGERS typedef int64_t Z3_SIGNED_INTEGER; - typedef int64_t Z3_UNSIGNED_INTEGER; + typedef uint64_t Z3_UNSIGNED_INTEGER; #else typedef long long Z3_SIGNED_INTEGER; typedef unsigned long long Z3_UNSIGNED_INTEGER;