diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 063c963b1..1872a4634 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -2,9 +2,11 @@ #include "GraphConditions.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace analysis { + template <typename ValueType> ConstraintCollector<ValueType>::ConstraintCollector(storm::models::sparse::Dtmc<ValueType> const& dtmc) { process(dtmc); @@ -20,6 +22,7 @@ namespace storm { return this->graphPreservingConstraintSet; } + template <typename ValueType> void ConstraintCollector<ValueType>::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) { for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { @@ -50,6 +53,45 @@ namespace storm { } } + for(auto const& rewModelEntry : dtmc.getRewardModels()) { + if (rewModelEntry.second.hasStateRewards()) { + for(auto const& stateReward : rewModelEntry.second.getStateRewardVector()) { + if (!storm::utility::isConstant(stateReward)) { + if (stateReward.denominator().isConstant()) { + if (stateReward.denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace(stateReward.nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (stateReward.denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace(stateReward.nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(stateReward.denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + } + } + } + } + if (rewModelEntry.second.hasStateActionRewards()) { + for(auto const& saReward : rewModelEntry.second.getStateActionRewardVector()) { + if (!storm::utility::isConstant(saReward)) { + if (saReward.denominator().isConstant()) { + if (saReward.denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace(saReward.nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (saReward.denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace(saReward.nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(saReward.denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + } + } + } + } + + } } template <typename ValueType>