From 9e9060ecd73eea5a29a31678b14b65e755d600b2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 13 Aug 2017 18:09:37 +0200 Subject: [PATCH 1/4] fix in changelog --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 90c72cd28..66635c85e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,7 +6,7 @@ The releases of major and minor versions contain an overview of changes since th Version 1.1.x ------------- -Long run average computation via LRA, LP based MDP model checking, parametric model checking has an own binary +Long run average computation via ValueIteration, LP based MDP model checking, parametric model checking has an own binary ### Version 1.1.0 (2017/8) From 2b01e2fa61a2a2a8fc0e19c317fa71875786252f Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 14 Aug 2017 20:37:04 +0200 Subject: [PATCH 2/4] 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 3/4] 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 4/4] 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.