diff --git a/CMakeLists.txt b/CMakeLists.txt index ee5bf36be..57e94b8b8 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -18,7 +18,7 @@ include(imported) ############################################################# ## -## CMake options of storm +## CMake options of Storm ## ############################################################# option(STORM_DEVELOPER "Sets whether the development mode is used." OFF) @@ -44,7 +44,7 @@ option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON) mark_as_advanced(STORM_COMPILE_WITH_CCACHE) option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF) option(STORM_USE_CLN_NUMBERS "Sets whether CLN or GMP numbers should be used" ON) -option(BUILD_SHARED_LIBS "Build the storm library dynamically" OFF) +option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF) set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).") set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") @@ -55,11 +55,6 @@ set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the li set(USE_XERCESC ${XML_SUPPORT}) mark_as_advanced(USE_XERCESC) -# Sets the source from which storm is obtained. Can be either "git" or "archive". This -# influences, among other things, the version information. -set(STORM_SOURCE "git" CACHE STRING "The source from which storm is obtained: either 'git' or 'archive'.") -mark_as_advanced(STORM_SOURCE) - # Set some CMAKE Variables as advanced mark_as_advanced(CMAKE_OSX_ARCHITECTURES) mark_as_advanced(CMAKE_OSX_SYSROOT) @@ -72,34 +67,36 @@ set(LIB_INSTALL_DIR lib/ CACHE PATH "Installation directory for libraries") set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables") -# By default, we build a release version. -if (NOT CMAKE_BUILD_TYPE) - set(CMAKE_BUILD_TYPE "RELEASE") -endif() -# Install dir for cmake files (info for other libraries that include storm) +# Install dir for cmake files (info for other libraries that include Storm) set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm") set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH "Installation directory for CMake files") message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}") -# If the STORM_DEVELOPER option was turned on, we target a debug version. +# If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version. if (STORM_DEVELOPER) - set(CMAKE_BUILD_TYPE "DEBUG") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTORM_DEV") + if (NOT CMAKE_BUILD_TYPE) + set(CMAKE_BUILD_TYPE "DEBUG") + endif() + add_definitions(-DSTORM_DEV) else() set(STORM_LOG_DISABLE_DEBUG ON) + if (NOT CMAKE_BUILD_TYPE) + set(CMAKE_BUILD_TYPE "RELEASE") + endif() endif() -message(STATUS "storm - Building ${CMAKE_BUILD_TYPE} version.") + +message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.") if(STORM_COMPILE_WITH_CCACHE) find_program(CCACHE_FOUND ccache) mark_as_advanced(CCACHE_FOUND) if(CCACHE_FOUND) - message(STATUS "storm - Using ccache") + message(STATUS "Storm - Using ccache") set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache) set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache) else() - message(STATUS "storm - Could not find ccache.") + message(STATUS "Storm - Could not find ccache.") endif() endif() @@ -125,7 +122,7 @@ else() set(OPERATING_SYSTEM "Linux") set(LINUX 1) ENDIF() -message(STATUS "storm - Detected operating system ${OPERATING_SYSTEM}.") +message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.") set(DYNAMIC_EXT ".so") set(STATIC_EXT ".a") @@ -303,12 +300,12 @@ if ("${CMAKE_GENERATOR}" STREQUAL "Xcode") endif() # Display information about build configuration. -message(STATUS "storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.") +message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.") if (STORM_DEVELOPER) - message(STATUS "storm - CXX Flags: ${CMAKE_CXX_FLAGS}") - message(STATUS "storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}") - message(STATUS "storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}") - message(STATUS "storm - Build type: ${CMAKE_BUILD_TYPE}") + message(STATUS "Storm - CXX Flags: ${CMAKE_CXX_FLAGS}") + message(STATUS "Storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}") + message(STATUS "Storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}") + message(STATUS "Storm - Build type: ${CMAKE_BUILD_TYPE}") endif() ############################################################# @@ -348,50 +345,40 @@ endif(DOXYGEN_FOUND) ############################################################# ## -## CMake-generated Config File for storm +## CMake-generated Config File for Storm ## ############################################################# -# If storm is built from an archive, we need to skip the version detection based on git. -if (STORM_SOURCE STREQUAL "archive") - if (NOT DEFINED STORM_VERSION_MAJOR OR NOT DEFINED STORM_VERSION_MINOR OR NOT DEFINED STORM_VERSION_PATCH) - message(FATAL_ERROR "storm - building from archive requires setting a version via cmake.") - endif() - message(STATUS "storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (building from archive).") - set(STORM_VERSION_COMMITS_AHEAD boost::none) - set(STORM_VERSION_GIT_HASH boost::none) +# try to obtain the current version from git. +include(GetGitRevisionDescription) +get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH) +git_describe_checkout(STORM_GIT_VERSION_STRING) + +# parse the git tag into variables +string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}") +string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_MINOR "${STORM_GIT_VERSION_STRING}") +string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_PATCH "${STORM_GIT_VERSION_STRING}") +string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}") +string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_VERSION_TAG_HASH "${STORM_GIT_VERSION_STRING}") +string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}") + +# now check whether the git version lookup failed +if (STORM_VERSION_MAJOR STREQUAL "HEAD-HASH-NOTFOUND") + set(STORM_VERSION_MAJOR 1) + set(STORM_VERSION_MINOR 0) + set(STORM_VERSION_PATCH 0) + set(STORM_VERSION_GIT_HASH "") + set(STORM_VERSION_COMMITS_AHEAD 0) set(STORM_VERSION_DIRTY boost::none) + + message(WARNING "Storm - git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") else() - if (DEFINED STORM_VERSION_MAJOR OR DEFINED STORM_VERSION_MINOR OR DEFINED STORM_VERSION_PATCH) - message(FATAL_ERROR "storm - building from git does not support setting a version via cmake.") - endif() - - # Make a version file containing the current version from git. - include(GetGitRevisionDescription) - get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH) - - git_describe_checkout(STORM_GIT_VERSION_STRING) - # Parse the git Tag into variables - string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_MINOR "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_PATCH "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_VERSION_TAG_HASH "${STORM_GIT_VERSION_STRING}") - string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}") if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$") - set(STORM_VERSION_DIRTY 1) + set(STORM_VERSION_DIRTY "true") else() - set(STORM_VERSION_DIRTY 0) + set(STORM_VERSION_DIRTY "false") endif() - if (STORM_VERSION_DIRTY) - set(STORM_VERSION_DIRTY_STR "yes") - else() - set(STORM_VERSION_DIRTY_STR "no") - endif() - message(STATUS "storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (${STORM_VERSION_COMMITS_AHEAD} commits ahead of tag), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY_STR}).") - - # proper type conversion so we can assign it to an optional - set(STORM_VERSION_GIT_HASH "std::string(\"${STORM_VERSION_GIT_HASH}\")") + message(STATUS "Storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (${STORM_VERSION_COMMITS_AHEAD} commits ahead of tag), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") endif() # Configure a header file to pass some of the CMake settings to the source code @@ -400,7 +387,7 @@ configure_file ( "${PROJECT_BINARY_DIR}/include/storm-config.h" ) -# Configure a source file to pass the storm version to the source code +# Configure a source file to pass the Storm version to the source code configure_file ( "${PROJECT_SOURCE_DIR}/storm-version.cpp.in" "${PROJECT_SOURCE_DIR}/src/storm/utility/storm-version.cpp" diff --git a/resources/3rdparty/exprtk/exprtk.hpp b/resources/3rdparty/exprtk/exprtk.hpp index 04f37d9a1..079ee1b6f 100755 --- a/resources/3rdparty/exprtk/exprtk.hpp +++ b/resources/3rdparty/exprtk/exprtk.hpp @@ -97,7 +97,11 @@ namespace exprtk inline bool is_letter(const char_t c) { return (('a' <= c) && (c <= 'z')) || - (('A' <= c) && (c <= 'Z')) ; + (('A' <= c) && (c <= 'Z')) +#ifdef MODIFICATION + || ('.' == c) || ('_' == c) +#endif + ; } inline bool is_digit(const char_t c) diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index c018108ec..0f0aa68fa 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -80,7 +80,7 @@ void analyzeWithSMT(std::string filename) { * Initialize the settings manager. */ void initializeSettings() { - storm::settings::mutableManager().setName("storm-DyFTeE", "storm-dft"); + storm::settings::mutableManager().setName("Storm-DyFTeE", "storm-dft"); // Register all known settings modules. storm::settings::addModule(); @@ -118,7 +118,7 @@ void initializeSettings() { int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::cli::printHeader("storm-DyFTeE", argc, argv); + storm::cli::printHeader("Storm-DyFTeE", argc, argv); initializeSettings(); bool optionsCorrect = storm::cli::parseOptions(argc, argv); @@ -251,10 +251,10 @@ int main(const int argc, const char** argv) { storm::utility::cleanUp(); return 0; } catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused storm-DyFTeE to terminate. The message of the exception is: " << exception.what()); + STORM_LOG_ERROR("An exception caused Storm-DyFTeE to terminate. The message of the exception is: " << exception.what()); return 1; } catch (std::exception const& exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused storm-DyFTeE to terminate. The message of this exception is: " << exception.what()); + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-DyFTeE to terminate. The message of this exception is: " << exception.what()); return 2; } } diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index bbff2c9cc..ff1723ff3 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -40,7 +40,7 @@ * Initialize the settings manager. */ void initializeSettings() { - storm::settings::mutableManager().setName("storm-GSPN", "storm-gspn"); + storm::settings::mutableManager().setName("Storm-GSPN", "storm-gspn"); // Register all known settings modules. storm::settings::addModule(); @@ -75,7 +75,7 @@ std::unordered_map parseCapacitiesList(std::string const& int main(const int argc, const char **argv) { try { storm::utility::setUp(); - storm::cli::printHeader("storm-GSPN", argc, argv); + storm::cli::printHeader("Storm-GSPN", argc, argv); initializeSettings(); bool optionsCorrect = storm::cli::parseOptions(argc, argv); @@ -147,10 +147,10 @@ int main(const int argc, const char **argv) { storm::utility::cleanUp(); return 0; } catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what()); + STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what()); return 1; } catch (std::exception const& exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what()); + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what()); return 2; } } diff --git a/src/storm-gspn/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp index cf5c698f0..b92b6f006 100644 --- a/src/storm-gspn/parser/GspnParser.cpp +++ b/src/storm-gspn/parser/GspnParser.cpp @@ -81,7 +81,7 @@ namespace storm { delete errHandler; xercesc::XMLPlatformUtils::Terminate(); #else - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "storm is not compiled with XML support: " << filename << " can not be parsed"); + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Storm is not compiled with XML support: " << filename << " can not be parsed"); #endif } } diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index 2fa9385a2..6e0f03dca 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -25,7 +25,7 @@ * Initialize the settings manager. */ void initializeSettings() { - storm::settings::mutableManager().setName("storm-PGCL", "storm-pgcl"); + storm::settings::mutableManager().setName("Storm-PGCL", "storm-pgcl"); // Register all known settings modules. storm::settings::addModule(); @@ -56,7 +56,7 @@ void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) { int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::cli::printHeader("storm-PGCL", argc, argv); + storm::cli::printHeader("Storm-PGCL", argc, argv); initializeSettings(); bool optionsCorrect = storm::cli::parseOptions(argc, argv); @@ -93,10 +93,10 @@ int main(const int argc, const char** argv) { } }catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused storm-PGCL to terminate. The message of the exception is: " << exception.what()); + STORM_LOG_ERROR("An exception caused Storm-PGCL to terminate. The message of the exception is: " << exception.what()); return 1; } catch (std::exception const& exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused storm-PGCL to terminate. The message of this exception is: " << exception.what()); + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-PGCL to terminate. The message of this exception is: " << exception.what()); return 2; } } diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 1a722e207..18ac14200 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -20,11 +20,11 @@ set(STORM_MAIN_SOURCES ${STORM_MAIN_FILE}) # Add custom additional include or link directories if (ADDITIONAL_INCLUDE_DIRS) - message(STATUS "storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}") + message(STATUS "Storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}") include_directories(${ADDITIONAL_INCLUDE_DIRS}) endif(ADDITIONAL_INCLUDE_DIRS) if (ADDITIONAL_LINK_DIRS) - message(STATUS "storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}") + message(STATUS "Storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}") link_directories(${ADDITIONAL_LINK_DIRS}) endif(ADDITIONAL_LINK_DIRS) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index efdb54d42..314afa700 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -93,7 +93,7 @@ namespace storm { #endif #ifdef STORM_HAVE_CARL // TODO get version string - STORM_PRINT("Linked with CARL." << std::endl); + STORM_PRINT("Linked with CArL." << std::endl); #endif #ifdef STORM_HAVE_CUDA diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 67ece142a..da7ac1862 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -102,6 +102,24 @@ namespace storm { return static_cast(bound); } + 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."); + return bound; + } + + template <> + uint64_t BoundedUntilFormula::getNonStrictUpperBound() const { + int_fast64_t bound = getUpperBound(); + if (isUpperBoundStrict()) { + STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + return bound - 1; + } else { + return bound; + } + } + void BoundedUntilFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h index 862871796..5dc2a3889 100644 --- a/src/storm/logic/BoundedUntilFormula.h +++ b/src/storm/logic/BoundedUntilFormula.h @@ -40,6 +40,9 @@ namespace storm { template ValueType getUpperBound() const; + + template + ValueType getNonStrictUpperBound() const; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 05bf0353b..36c82856c 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -64,6 +64,24 @@ namespace storm { return value; } + template <> + double CumulativeRewardFormula::getNonStrictBound() const { + double bound = getBound(); + STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + return bound; + } + + template <> + uint64_t CumulativeRewardFormula::getNonStrictBound() const { + int_fast64_t bound = getBound(); + if (isBoundStrict()) { + STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound."); + return bound - 1; + } else { + return bound; + } + } + void CumulativeRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index ad9d5e3c0..fce825271 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -35,6 +35,9 @@ namespace storm { template ValueType getBound() const; + template + ValueType getNonStrictBound() const; + private: static void checkNoVariablesInBound(storm::expressions::Expression const& bound); diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index fc221147b..f59273480 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -77,7 +77,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } @@ -98,7 +98,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 4d6e9407f..1f5c9ee0d 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -67,7 +67,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } @@ -108,7 +108,7 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 4aef07d8d..03789fe53 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -61,7 +61,7 @@ namespace storm { lowerBound = pathFormula.getLowerBound(); } if (pathFormula.hasUpperBound()) { - upperBound = pathFormula.getUpperBound(); + upperBound = pathFormula.getNonStrictUpperBound(); } else { upperBound = storm::utility::infinity(); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 9ddaea7b8..1dff5b454 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -49,10 +49,7 @@ namespace storm { storm::storage::BitVector statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 & ~psiStates; STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNumberOfSetBits() << " 'maybe' states."); - if (statesWithProbabilityGreater0NonPsi.empty()) { - result = std::vector(numberOfStates, storm::utility::zero()); - - } else { + if (!statesWithProbabilityGreater0NonPsi.empty()) { if (storm::utility::isZero(upperBound)) { // In this case, the interval is of the form [0, 0]. result = std::vector(numberOfStates, storm::utility::zero()); @@ -189,6 +186,8 @@ namespace storm { } } } + } else { + result = std::vector(numberOfStates, storm::utility::zero()); } return result; diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 1936e60bd..ebbb34e99 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -76,14 +76,14 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index d42de45dd..ff1785db4 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -95,7 +95,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); } template @@ -103,7 +103,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ll), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index b94f22c92..a6a68522e 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -48,7 +48,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; } @@ -86,7 +86,7 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index b505734ed..08de02dc8 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -64,7 +64,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -125,7 +125,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index c52307315..b7d163f62 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } @@ -84,7 +84,7 @@ namespace storm { std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); } diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 2ac26509a..e077fbb26 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -76,7 +76,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *this->linearEquationSolverFactory); } template @@ -84,7 +84,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *this->linearEquationSolverFactory); } template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 4e440e698..5c79cd3c5 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -249,13 +249,8 @@ namespace storm { // Compute the reward vector to add in each step based on the available reward models. std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); - // Initialize result to either the state rewards of the model or the null vector. - std::vector result; - if (rewardModel.hasStateRewards()) { - result = rewardModel.getStateRewardVector(); // Whyyy? - } else { - result.resize(transitionMatrix.getRowGroupCount()); - } + // Initialize result to the zero vector. + std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); solver->repeatedMultiply(dir, result, &totalRewardVector, stepBound); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index c2f84b652..2614ef459 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -66,6 +66,7 @@ namespace storm { if (this->isResultForAllStates()) { map_type newMap; + for (auto const& element : filterTruthValues) { STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results."); newMap.emplace(element, this->getValueVector()[element]); diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 826c8075b..d743d9ced 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -237,12 +237,12 @@ namespace storm { } } } - STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "storm does not allow to accumulate over both time and steps"); + STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps"); if (propertyStructure.count("step-instant") > 0) { storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context); - STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant step-instants"); + STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant step-instants"); int64_t stepInstant = stepInstantExpr.evaluateAsInt(); STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed"); if(!accTime && !accSteps) { @@ -262,7 +262,7 @@ namespace storm { } } else if (propertyStructure.count("time-instant") > 0) { storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context); - STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant time-instants"); + STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant time-instants"); double timeInstant = timeInstantExpr.evaluateAsDouble(); STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed"); if(!accTime && !accSteps) { @@ -284,7 +284,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); } - //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "storm only allows accumulation if a step- or time-bound is given."); + //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); @@ -328,9 +328,9 @@ namespace storm { } if (propertyStructure.count("step-bounds") > 0) { storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds")); - STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports step-bounded until with an upper bound"); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound"); if(pi.hasLowerBound()) { - STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "storm only supports step-bounded until without a (non-trivial) lower-bound"); + STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound"); } int64_t upperBound = pi.upperBound.evaluateAsInt(); if(pi.upperBoundStrict) { @@ -340,7 +340,7 @@ namespace storm { return std::make_shared(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps); } else if (propertyStructure.count("time-bounds") > 0) { storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); - STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports time-bounded until with an upper bound."); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); double lowerBound = 0.0; if(pi.hasLowerBound()) { lowerBound = pi.lowerBound.evaluateAsDouble(); diff --git a/src/storm/parser/SpiritErrorHandler.h b/src/storm/parser/SpiritErrorHandler.h index 53a73c9e3..34280e422 100644 --- a/src/storm/parser/SpiritErrorHandler.h +++ b/src/storm/parser/SpiritErrorHandler.h @@ -19,7 +19,7 @@ namespace storm { std::stringstream stream; stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl; - stream << "\t" << line << std::endl << "\t"; + stream << "\t" << line << std::endl; auto caretColumn = boost::spirit::get_column(lineStart, where); stream << "\t" << std::string(caretColumn - 1, ' ') << "^" << std::endl; diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp index d7501ad53..9b6f7da2b 100644 --- a/src/storm/solver/MathsatSmtSolver.cpp +++ b/src/storm/solver/MathsatSmtSolver.cpp @@ -107,7 +107,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_push_backtrack_point(env); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -115,7 +115,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_pop_backtrack_point(env); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -123,7 +123,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT SmtSolver::pop(n); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -132,7 +132,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_reset_env(env); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -141,7 +141,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_assert_formula(env, expressionAdapter->translateExpression(e)); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -162,7 +162,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -190,7 +190,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -219,7 +219,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } #endif @@ -230,7 +230,7 @@ namespace storm { STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return this->convertMathsatModelToValuation(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -239,7 +239,7 @@ namespace storm { STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return std::shared_ptr(new MathsatModelReference(this->getManager(), env, *expressionAdapter)); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -279,7 +279,7 @@ namespace storm { this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); return valuations; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -379,7 +379,7 @@ namespace storm { this->pop(); return static_cast(numberOfModels); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -405,7 +405,7 @@ namespace storm { this->pop(); return static_cast(numberOfModels); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -426,7 +426,7 @@ namespace storm { return unsatAssumptions; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -440,7 +440,7 @@ namespace storm { } msat_set_itp_group(env, groupIter->second); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } @@ -462,7 +462,7 @@ namespace storm { return this->expressionAdapter->translateExpression(interpolant); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support."); #endif } } diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index fdac47809..3a8ae9e26 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -73,7 +73,7 @@ namespace storm { #ifdef STORM_HAVE_CUDA return basicValueIteration_mvReduce_uint64_double_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support."); #endif } template <> @@ -92,7 +92,7 @@ namespace storm { #ifdef STORM_HAVE_CUDA return basicValueIteration_mvReduce_uint64_float_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support."); #endif } @@ -116,7 +116,7 @@ namespace storm { #ifdef STORM_HAVE_CUDA return basicValueIteration_mvReduce_uint64_double_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support."); #endif } template <> @@ -135,7 +135,7 @@ namespace storm { #ifdef STORM_HAVE_CUDA return basicValueIteration_mvReduce_uint64_float_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without CUDA support."); #endif } diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index 95b061f70..45ffbd7be 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -24,7 +24,7 @@ namespace storm { #ifdef STORM_HAVE_Z3_OPTIMIZE Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir) { - STORM_LOG_WARN_COND(name != "", "Z3 does not support names for solvers"); + STORM_LOG_WARN_COND(name == "", "Z3 does not support names for solvers"); z3::config config; config.set("model", true); context = std::unique_ptr(new z3::context(config)); @@ -120,7 +120,7 @@ namespace storm { void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); - STORM_LOG_WARN_COND(name != "", "Z3 does not support names for constraints"); + STORM_LOG_WARN_COND(name == "", "Z3 does not support names for constraints"); solver->add(expressionAdapter->translateExpression(constraint)); } @@ -188,7 +188,7 @@ namespace storm { z3::expr z3Var = this->expressionAdapter->translateExpression(variable); return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true)); } - + double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { storm::expressions::Expression value = getValue(variable); if(value.getBaseExpression().isIntegerLiteralExpression()) { @@ -398,6 +398,10 @@ namespace storm { bool Z3LpSolver::isOptimal() const { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } + + storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; diff --git a/src/storm/solver/Z3SmtSolver.cpp b/src/storm/solver/Z3SmtSolver.cpp index cb291bcb9..cff81e5e7 100644 --- a/src/storm/solver/Z3SmtSolver.cpp +++ b/src/storm/solver/Z3SmtSolver.cpp @@ -19,7 +19,7 @@ namespace storm { z3::expr z3ExprValuation = model.eval(z3Expr, true); return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -30,7 +30,7 @@ namespace storm { z3::expr z3ExprValuation = model.eval(z3Expr, true); return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -41,7 +41,7 @@ namespace storm { z3::expr z3ExprValuation = model.eval(z3Expr, true); return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -68,7 +68,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 this->solver->push(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -77,7 +77,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 this->solver->pop(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -86,7 +86,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 this->solver->pop(static_cast(n)); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -95,7 +95,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 this->solver->reset(); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -104,7 +104,7 @@ namespace storm { #ifdef STORM_HAVE_Z3 this->solver->add(expressionAdapter->translateExpression(assertion)); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -125,7 +125,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -152,7 +152,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -180,7 +180,7 @@ namespace storm { } return this->lastResult; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } #endif @@ -190,7 +190,7 @@ namespace storm { STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return this->convertZ3ModelToValuation(this->solver->get_model()); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -199,7 +199,7 @@ namespace storm { STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable."); return std::shared_ptr(new Z3ModelReference(this->getManager(), this->solver->get_model(), *this->expressionAdapter)); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -234,7 +234,7 @@ namespace storm { this->allSat(important, static_cast>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; })); return valuations; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -276,7 +276,7 @@ namespace storm { this->pop(); return numberOfModels; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -317,7 +317,7 @@ namespace storm { this->pop(); return numberOfModels; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -335,7 +335,7 @@ namespace storm { return unsatAssumptions; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -346,7 +346,7 @@ namespace storm { solver->set(paramObject); return true; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } @@ -357,7 +357,7 @@ namespace storm { solver->set(paramObject); return true; #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without Z3 support."); #endif } diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp index 6fa620157..870014f60 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp @@ -94,8 +94,15 @@ namespace storm { } template - boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const&, boost::any const&) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + boost::any ToRationalFunctionVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + RationalFunctionType operandAsRationalFunction = boost::any_cast(expression.getOperand()->accept(*this, data)); + switch (expression.getOperatorType()) { + case UnaryNumericalFunctionExpression::OperatorType::Minus: + return -operandAsRationalFunction; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function."); + } + return boost::any(); } template diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp index 52dbad648..1dbca4cdf 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneEnumeration.cpp @@ -113,7 +113,6 @@ namespace storm { relevantMatrix = EigenMatrix(); relevantVector = EigenVector(); } - STORM_LOG_DEBUG("Invoked generateVerticesFromHalfspaces with " << hPoly.getMatrix().rows() << " hyperplanes and " << resultVertices.size() << " vertices and " << relevantMatrix.rows() << " relevant hyperplanes. Dimension is " << hPoly.dimension()); } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index c39a6b79b..fc5346c0d 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -183,7 +183,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm currently does not support translating cummulative reward formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cumulative reward formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp index 73c5a8a15..20126f488 100644 --- a/src/storm/storm.cpp +++ b/src/storm/storm.cpp @@ -17,8 +17,8 @@ int main(const int argc, const char** argv) { try { storm::utility::Stopwatch totalTimer(true); storm::utility::setUp(); - storm::cli::printHeader("storm", argc, argv); - storm::settings::initializeAll("storm", "storm"); + storm::cli::printHeader("Storm", argc, argv); + storm::settings::initializeAll("Storm", "storm"); bool optionsCorrect = storm::cli::parseOptions(argc, argv); if (!optionsCorrect) { return -1; @@ -36,10 +36,10 @@ int main(const int argc, const char** argv) { } return 0; } catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what()); + STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what()); return 1; } catch (std::exception const& exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what()); + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what()); return 2; } } diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h index 2cd72c00b..cfe705304 100644 --- a/src/storm/utility/storm-version.h +++ b/src/storm/utility/storm-version.h @@ -19,13 +19,13 @@ namespace storm { const static unsigned versionPatch; /// The short hash of the git commit this build is based on - const static boost::optional gitRevisionHash; + const static std::string gitRevisionHash; /// How many commits passed since the tag was last set. - const static boost::optional commitsAhead; + const static unsigned commitsAhead; - /// 0 iff there no files were modified in the checkout, 1 otherwise. - const static boost::optional dirty; + /// 0 iff there no files were modified in the checkout, 1 otherwise. If none, no information about dirtyness is given. + const static boost::optional dirty; /// The system which has compiled Storm. const static std::string systemName; @@ -48,14 +48,22 @@ namespace storm { static std::string longVersionString() { std::stringstream sstream; sstream << "Version " << versionMajor << "." << versionMinor << "." << versionPatch; - if (commitsAhead && commitsAhead.get() > 0) { - sstream << " (+" << commitsAhead.get() << " commits)"; + if (commitsAhead) { + sstream << " (+ " << commitsAhead << " commits)"; } - if (gitRevisionHash) { - sstream << " build from revision " << gitRevisionHash.get(); + if (!gitRevisionHash.empty()) { + sstream << " build from revision " << gitRevisionHash; + } else { + sstream << " built from archive"; } - if (dirty && dirty.get() == 1) { - sstream << " (dirty)"; + if (dirty) { + if (dirty.get()) { + sstream << " (dirty)"; + } else { + sstream << " (clean)"; + } + } else { + sstream << " (potentially dirty)"; } return sstream.str(); } diff --git a/src/test/storm-test.cpp b/src/test/storm-test.cpp index a88084304..7f33be83a 100644 --- a/src/test/storm-test.cpp +++ b/src/test/storm-test.cpp @@ -2,7 +2,7 @@ #include "storm/settings/SettingsManager.h" int main(int argc, char **argv) { - storm::settings::initializeAll("storm (Functional) Testing Suite", "test"); + storm::settings::initializeAll("Storm (Functional) Testing Suite", "test"); ::testing::InitGoogleTest(&argc, argv); return RUN_ALL_TESTS(); } diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 051612984..ac646d99a 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -12,7 +12,6 @@ #include "storm/builder/DdPrismModelBuilder.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/utility/graph.h" -#include "storm/utility/shortestPaths.cpp" #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/storage/dd/DdManager.h" diff --git a/src/test/utility/KSPTest.cpp b/src/test/utility/KSPTest.cpp index 3d28ccae6..df8b4f212 100644 --- a/src/test/utility/KSPTest.cpp +++ b/src/test/utility/KSPTest.cpp @@ -6,15 +6,13 @@ #include "storm/parser/PrismParser.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/graph.h" -#include "storm/utility/shortestPaths.cpp" +#include "storm/utility/shortestPaths.h" // NOTE: The KSPs / distances of these tests were generated by the // KSP-Generator itself and checked for gross implausibility, but no // more than that. // An independent verification of the values would be really nice ... -// FIXME: (almost) all of these fail; the question is: is there actually anything wrong or does the new parser yield a different order of states? - std::shared_ptr> buildExampleModel() { std::string prismModelPath = STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"; storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath); @@ -61,16 +59,12 @@ TEST(KSPTest, groupTarget) { auto groupTarget = std::vector{50, 90}; auto spg = storm::utility::ksp::ShortestPathsGenerator(*model, groupTarget); - // FIXME comments are outdated (but does it even matter?) - // this path should lead to 90 double dist1 = spg.getDistance(8); EXPECT_DOUBLE_EQ(0.00018449245583999996, dist1); - // this one to 50 double dist2 = spg.getDistance(9); EXPECT_DOUBLE_EQ(0.00018449245583999996, dist2); - // this one to 90 again double dist3 = spg.getDistance(12); EXPECT_DOUBLE_EQ(7.5303043199999984e-06, dist3); } diff --git a/storm-version.cpp.in b/storm-version.cpp.in index 23a993169..61d9b4bc5 100644 --- a/storm-version.cpp.in +++ b/storm-version.cpp.in @@ -1,4 +1,4 @@ -//AUTO GENERATED -- DO NOT CHANGE +//AUTO GENERATED -- DO NOT CHANGE // TODO resolve issues when placing this in the build order directly. #include "storm/utility/storm-version.h" @@ -8,9 +8,9 @@ namespace storm { const unsigned StormVersion::versionMajor = @STORM_VERSION_MAJOR@; const unsigned StormVersion::versionMinor = @STORM_VERSION_MINOR@; const unsigned StormVersion::versionPatch = @STORM_VERSION_PATCH@; - const boost::optional StormVersion::gitRevisionHash = @STORM_VERSION_GIT_HASH@; - const boost::optional StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@; - const boost::optional StormVersion::dirty = @STORM_VERSION_DIRTY@; + const std::string StormVersion::gitRevisionHash = "@STORM_VERSION_GIT_HASH@"; + const unsigned StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@; + const boost::optional StormVersion::dirty = @STORM_VERSION_DIRTY@; const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@"; const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@"; const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@";