|
|
@ -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> |
|
|
|