From a994b80931f4f7af8c1a07ccd559b42db86748c1 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 18:58:36 +0200 Subject: [PATCH 1/5] getting rid of outdated carl simple constraint usage --- src/storm/adapters/Smt2ExpressionAdapter.h | 30 +++++----------------- src/storm/analysis/GraphConditions.h | 6 ++--- src/storm/solver/SmtlibSmtSolver.cpp | 27 ------------------- src/storm/solver/SmtlibSmtSolver.h | 12 +++------ 4 files changed, 13 insertions(+), 62 deletions(-) diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index c61566177..f1b96b71e 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -38,8 +38,7 @@ namespace storm { std::string translateExpression(storm::expressions::Expression const& ) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented"); } - -#ifdef STORM_HAVE_CARL + /*! * Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2. @@ -60,6 +59,7 @@ namespace storm { ") " + ")"; } + /*! * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2. @@ -67,31 +67,16 @@ namespace storm { * @param constraint * @return An equivalent expression for Smt2. */ - std::string translateExpression(storm::ArithConstraint const& constraint) { - std::stringstream ss; - ss << "(" << constraint.rel() << " " << - constraint.lhs().toString(false, useReadableVarNames) << " " << - "0 " << - ")"; - return ss.str(); - } - - /*! - * Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2. - - * @param constraint - * @return An equivalent expression for Smt2. - */ - std::string translateExpression(storm::ArithConstraint const& constraint) { + std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation) { std::stringstream ss; - ss << "(" << constraint.rel() << " " << - constraint.lhs().toString(false, useReadableVarNames) << " " << + ss << "(" << relation << " " << + leftHandSide.toString(false, useReadableVarNames) << " " << "0 " << ")"; return ss.str(); } -#endif + /*! * Translates the given variable to an equivalent expression for Smt2. * @@ -126,7 +111,7 @@ namespace storm { } -#ifdef STORM_HAVE_CARL + /*! Checks whether the variables in the given set are already declared and creates them if necessary * @param variables the set of variables to check */ @@ -167,7 +152,6 @@ namespace storm { } return result; } -#endif private: // The manager that can be used to build expressions. diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 48b4aee64..394f11b31 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -8,12 +8,12 @@ namespace storm { namespace analysis { - + template struct ConstraintType { - typedef storm::ArithConstraint val; + typedef void* val; }; - + template struct ConstraintType::value>::type> { typedef carl::Formula val; diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index 8dcd37ddc..69394ec8a 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -102,33 +102,6 @@ namespace storm { writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true); } - void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { - add(constraint.lhs(), constraint.rel()); - } - - void SmtlibSmtSolver::add(storm::ArithConstraint const& constraint) { - //if some of the occurring variables are not declared yet, we will have to. - std::set variables = constraint.lhs().gatherVariables(); - std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); - for (auto declaration : varDeclarations){ - writeCommand(declaration, true); - } - writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true); - } - - void SmtlibSmtSolver::add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint){ - STORM_LOG_THROW((guard.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a guarded constraint, but the guard is not of type bool."); - //if some of the occurring variables are not declared yet, we will have to (including the guard!). - std::set variables = constraint.lhs().gatherVariables(); - variables.insert(guard); - std::vector const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables); - for (auto declaration : varDeclarations){ - writeCommand(declaration, true); - } - std::string guardName= carl::VariablePool::getInstance().getName(guard, this->useReadableVarNames); - writeCommand("( assert (=> " + guardName + " " + expressionAdapter->translateExpression(constraint) + " ) )", true); - } - void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value){ STORM_LOG_THROW((variable.getType()==carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException, "Tried to add a constraint that consists of a non-boolean variable."); std::set variableSet; diff --git a/src/storm/solver/SmtlibSmtSolver.h b/src/storm/solver/SmtlibSmtSolver.h index 70e4c325f..6ae64eb92 100644 --- a/src/storm/solver/SmtlibSmtSolver.h +++ b/src/storm/solver/SmtlibSmtSolver.h @@ -51,12 +51,7 @@ namespace storm { //adds the constraint "leftHandSide relation rightHandSide" virtual void add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide=storm::RationalFunction(0)); - //adds the given carl constraint - void add(typename storm::ArithConstraint const& constraint); - void add(typename storm::ArithConstraint const& constraint); - - // adds the given carl constraint that is guarded by the given guard. The guard should have type 'bool' - void add(storm::RationalFunctionVariable const& guard, typename storm::ArithConstraint const& constraint); + // asserts that the given variable has the given value. The variable should have type 'bool' void add(storm::RationalFunctionVariable const& variable, bool value); @@ -65,10 +60,9 @@ namespace storm { virtual CheckResult check() override; virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; -#ifndef WINDOWS + virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; -#endif - + bool isNeedsRestart() const; //Todo: some of these might be added in the future From a27e7bdc82d7b9036ee5be080db6fb7f0ca1315c Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 13 Aug 2017 23:48:13 +0200 Subject: [PATCH 2/5] no longer use arithconstraint --- src/storm/adapters/RationalFunctionAdapter.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h index ba9858fe0..f403103f5 100644 --- a/src/storm/adapters/RationalFunctionAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -7,7 +7,6 @@ #include #include #include -#include #include namespace carl { @@ -58,5 +57,5 @@ namespace storm { typedef carl::RationalFunction RationalFunction; typedef carl::Interval Interval; - template using ArithConstraint = carl::SimpleConstraint; } + From 2b01e2fa61a2a2a8fc0e19c317fa71875786252f Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 14 Aug 2017 20:37:04 +0200 Subject: [PATCH 3/5] GraphConditions for any model type --- src/storm/analysis/GraphConditions.cpp | 31 ++++++++++++++++++-------- src/storm/analysis/GraphConditions.h | 18 +++++++-------- 2 files changed, 31 insertions(+), 18 deletions(-) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index bf3beeb0c..ef77a720b 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -1,4 +1,6 @@ +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Ctmc.h" #include "GraphConditions.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" @@ -9,8 +11,8 @@ namespace storm { template - ConstraintCollector::ConstraintCollector(storm::models::sparse::Dtmc const& dtmc) { - process(dtmc); + ConstraintCollector::ConstraintCollector(storm::models::sparse::Model const& model) { + process(model); } template @@ -50,10 +52,13 @@ namespace storm { } template - void ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { - for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { + void ConstraintCollector::process(storm::models::sparse::Model const& model) { + for(uint_fast64_t action = 0; action < model.getTransitionMatrix().getRowCount(); ++action) { ValueType sum = storm::utility::zero(); - for (auto const& transition : dtmc.getRows(state)) { + + for (auto transitionIt = model.getTransitionMatrix().begin(action); transitionIt != model.getTransitionMatrix().end(action); ++transitionIt) { + auto const& transition = *transitionIt; + std::cout << transition.getValue() << std::endl; sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { auto const& transitionVars = transition.getValue().gatherVariables(); @@ -90,9 +95,17 @@ namespace storm { // Assert: sum == 1 wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomialWithCoefficient(), storm::CompareRelation::EQ); } + } + if (model.getType() == storm::models::ModelType::Ctmc) { + auto const& exitRateVector = static_cast const&>(model).getExitRateVector(); + wellformedRequiresNonNegativeEntries(exitRateVector); + } else if (model.getType() == storm::models::ModelType::MarkovAutomaton) { + auto const& exitRateVector = static_cast const&>(model).getExitRates(); + wellformedRequiresNonNegativeEntries(exitRateVector); } - for(auto const& rewModelEntry : dtmc.getRewardModels()) { + + for(auto const& rewModelEntry : model.getRewardModels()) { if (rewModelEntry.second.hasStateRewards()) { wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateRewardVector()); } @@ -117,13 +130,13 @@ namespace storm { } } } - } + } template - void ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { - process(dtmc); + void ConstraintCollector::operator()(storm::models::sparse::Model const& model) { + process(model); } template class ConstraintCollector; diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 394f11b31..a901dfa68 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -38,12 +38,12 @@ namespace storm { void wellformedRequiresNonNegativeEntries(std::vector const&); public: /*! - * Constructs a constraint collector for the given DTMC. The constraints are built and ready for + * Constructs a constraint collector for the given Model. The constraints are built and ready for * retrieval after the construction. * - * @param dtmc The DTMC for which to create the constraints. + * @param model The Model for which to create the constraints. */ - ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); + ConstraintCollector(storm::models::sparse::Model const& model); /*! * Returns the set of wellformed-ness constraints. @@ -66,18 +66,18 @@ namespace storm { std::set const& getVariables() const; /*! - * Constructs the constraints for the given DTMC. + * Constructs the constraints for the given Model. * - * @param dtmc The DTMC for which to create the constraints. + * @param model The DTMC for which to create the constraints. */ - void process(storm::models::sparse::Dtmc const& dtmc); + void process(storm::models::sparse::Model const& model); /*! - * Constructs the constraints for the given DTMC by calling the process method. + * Constructs the constraints for the given Model by calling the process method. * - * @param dtmc The DTMC for which to create the constraints. + * @param model The Model for which to create the constraints. */ - void operator()(storm::models::sparse::Dtmc const& dtmc); + void operator()(storm::models::sparse::Model const& model); }; From 66cf4f1d28bad8f52b842e423e5ae5bd9a22d463 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 14 Aug 2017 20:37:27 +0200 Subject: [PATCH 4/5] Command line access to onlyconstraints for any model type --- src/storm-pars-cli/storm-pars.cpp | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 1ff2fabb6..5fa744c59 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -306,15 +306,8 @@ namespace storm { if (parSettings.onlyObtainConstraints()) { STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified."); - if (model->isOfType(storm::models::ModelType::Dtmc)) { - auto dtmc = model->template as>(); - storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*dtmc),parSettings.exportResultPath()); - return; - } else { - STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::NotImplementedException, "Constraints for MDPs and CTMCs not implemented."); - - } - + storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*(model->as>())), parSettings.exportResultPath()); + return; } if (model) { From 5624818caf179fc4b96524e8faa20dc84cdf2213 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 14 Aug 2017 20:37:40 +0200 Subject: [PATCH 5/5] Updated Changelog --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c55d776d..a346bc43d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,11 @@ The releases of major and minor versions contain an overview of changes since th Version 1.1.x ------------- +### Version 1.1.1 +- c++ api changes: Building model takes BuilderOptions instead of extended list of Booleans, does not depend on settings anymore. +- storm-cli-utilities now contains cli related stuff, instead of storm-lib +- storm-pars: support for welldefinedness constraints in mdps. + ### Version 1.1.0 (2017/8) - Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach.