diff --git a/CHANGELOG.md b/CHANGELOG.md index 7c55d776d..56004ed4f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,12 @@ The releases of major and minor versions contain an overview of changes since th Version 1.1.x ------------- +Long run average computation via ValueIteration, LP based MDP model checking, parametric model checking has an own binary + +### 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) 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) { 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); };