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); };