sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'master' into counterexample_improvements

main
Sebastian Junges 7 years ago
parent
8478352030 dfc0141894
commit
73a1911a53
13 changed files with 64 additions and 31 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      .travis.yml
  2. 14
      CMakeLists.txt
  3. 23
      resources/3rdparty/CMakeLists.txt
  4. 4
      resources/3rdparty/carl/CMakeLists.txt
  5. 2
      src/storm-dft/CMakeLists.txt
  6. 2
      src/storm-parsers/CMakeLists.txt
  7. 2
      src/storm-pgcl/CMakeLists.txt
  8. 21
      src/storm/adapters/Z3ExpressionAdapter.cpp
  9. 2
      src/storm/solver/stateelimination/DynamicStatePriorityQueue.h
  10. 4
      src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
  11. 4
      src/test/storm/utility/KSPTest.cpp
  12. 7
      storm-config.h.in
  13. 5
      travis/generate_travis.py

5
.travis.yml
View File

@ -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

14
CMakeLists.txt
View File

@ -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

23
resources/3rdparty/CMakeLists.txt
View File

@ -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
@ -239,16 +248,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 +266,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

4
resources/3rdparty/carl/CMakeLists.txt
View File

@ -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.")

2
src/storm-dft/CMakeLists.txt
View File

@ -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})

2
src/storm-parsers/CMakeLists.txt
View File

@ -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.

2
src/storm-pgcl/CMakeLists.txt
View File

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

21
src/storm/adapters/Z3ExpressionAdapter.cpp
View File

@ -1,5 +1,7 @@
#include "storm/adapters/Z3ExpressionAdapter.h"
#include <cstdint>
#include "storm/storage/expressions/Expressions.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/utility/macros.h"
@ -12,6 +14,15 @@ namespace storm {
namespace adapters {
#ifdef STORM_HAVE_Z3
#ifdef STORM_Z3_API_USES_STANDARD_INTEGERS
typedef int64_t Z3_SIGNED_INTEGER;
typedef uint64_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 +144,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<storm::RationalNumber>((int_fast64_t) num) / storm::utility::convertNumber<storm::RationalNumber>((int_fast64_t) den));
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(static_cast<int_fast64_t>(num)) / storm::utility::convertNumber<storm::RationalNumber>(static_cast<int_fast64_t>(den)));
} else {
return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(std::string(Z3_get_numeral_string(expr.ctx(), expr))));
}
@ -304,7 +315,7 @@ namespace storm {
return cacheIt->second;
}
z3::expr result = context.int_val(static_cast<long long>(expression.getValue()));
z3::expr result = context.int_val(static_cast<Z3_SIGNED_INTEGER>(expression.getValue()));
expressionCache.emplace(&expression, result);
return result;

2
src/storm/solver/stateelimination/DynamicStatePriorityQueue.h
View File

@ -17,7 +17,7 @@ namespace storm {
namespace stateelimination {
struct PriorityComparator {
bool operator()(std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& first, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& second) {
bool operator()(std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& first, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& second) const {
return (first.second < second.second) || (first.second == second.second && first.first < second.first) ;
}
};

4
src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp
View File

@ -148,7 +148,7 @@ TEST(MaximalEndComponentDecomposition, Example1) {
storm::storage::MaximalEndComponentDecomposition<double> 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<double> 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});

4
src/test/storm/utility/KSPTest.cpp
View File

@ -81,7 +81,7 @@ TEST(KSPTest, kspStateSet) {
storm::utility::ksp::ShortestPathsGenerator<double> 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<double> 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};

7
storm-config.h.in
View File

@ -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

5
travis/generate_travis.py
View File

@ -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"

Write Preview
Loading…
Cancel
Save