From adaa55a61664725c8010bf56b5bb74bc88f5249f Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 Feb 2017 08:59:03 +0100 Subject: [PATCH 1/7] Fixed the printing of two warnings --- src/storm/solver/Z3LpSolver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index 95b061f70..e49845eef 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)); } From fd24a2586c0d47909178b5a300d5b9b989e84613 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 22 Feb 2017 18:52:24 +0100 Subject: [PATCH 2/7] added implementation for Z3LpSolver::getValue() when z3_optimize is not available --- src/storm/solver/Z3LpSolver.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index e49845eef..45ffbd7be 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -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."; From a22ec04f10415f2d2997be1ea8dde0bb7c6ba4d4 Mon Sep 17 00:00:00 2001 From: Tom Janson Date: Fri, 24 Feb 2017 22:57:51 +0100 Subject: [PATCH 3/7] fix old KSP test include actually still works fine --- src/test/utility/GraphTest.cpp | 1 - src/test/utility/KSPTest.cpp | 8 +------- 2 files changed, 1 insertion(+), 8 deletions(-) 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); } From 1c322737089d61573491a31dced8e3a70d0e2202 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 3 Mar 2017 14:19:57 +0100 Subject: [PATCH 4/7] made storm_developer not override build_type if one was explicitly set --- CMakeLists.txt | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index ee5bf36be..02e32c8ad 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -72,23 +72,25 @@ 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) 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.") if(STORM_COMPILE_WITH_CCACHE) From e5404a27e9289aeea7c42782bfb379a4cfb62e74 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 5 Mar 2017 19:58:59 +0100 Subject: [PATCH 5/7] Implemented parsing for UnaryNumericalFunctionExpression --- .../storage/expressions/ToRationalFunctionVisitor.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) 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 From 0b6c481cf20d7c4777fef85af537bcccca2ce495 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 7 Mar 2017 20:17:10 +0100 Subject: [PATCH 6/7] fix for sparse mdp model checker: computing cumulative rewards did one step too much --- .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 2db593ac9..fc1649d19 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -226,13 +226,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(); - } 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); From b3a02b6e8af3ffb1ae9d0741aa6dd39ef7feab7b Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 8 Mar 2017 11:25:54 +0100 Subject: [PATCH 7/7] fix in sparse ctmc model checker: bounded until returned empty result in case there are no non-prob0-states --- src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 2 ++ .../modelchecker/results/ExplicitQuantitativeCheckResult.cpp | 1 + 2 files changed, 3 insertions(+) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 10995f9b7..1dff5b454 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -186,6 +186,8 @@ namespace storm { } } } + } else { + result = std::vector(numberOfStates, storm::utility::zero()); } return result; diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 5ea662a57..f9231a22c 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -61,6 +61,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]);