17namespace modelchecker {
18namespace multiobjective {
20template<
class SparseMdpModelType>
27template<
class SparseMdpModelType>
30 this->actionRewards.resize(this->objectives.size());
31 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
32 auto const& formula = *this->objectives[objIndex].formula;
33 STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException,
34 "Unexpected type of operator formula: " << formula);
35 if (formula.getSubformula().isCumulativeRewardFormula()) {
36 auto const& cumulativeRewardFormula = formula.getSubformula().asCumulativeRewardFormula();
37 STORM_LOG_THROW(!cumulativeRewardFormula.isMultiDimensional() && !cumulativeRewardFormula.getTimeBoundReference().isRewardBound(),
38 storm::exceptions::UnexpectedException,
"Unexpected type of sub-formula: " << formula.getSubformula());
40 STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula() || formula.getSubformula().isLongRunAverageRewardFormula(),
41 storm::exceptions::UnexpectedException,
"Unexpected type of sub-formula: " << formula.getSubformula());
43 typename SparseMdpModelType::RewardModelType
const& rewModel = model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName());
44 STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException,
45 "Reward model has transition rewards which is not expected.");
46 this->actionRewards[objIndex] = rewModel.getTotalRewardVector(model.getTransitionMatrix());
50template<
class SparseMdpModelType>
57template<
class SparseMdpModelType>
64template<
class SparseMdpModelType>
66 std::vector<ValueType>& weightedRewardVector) {
68 std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->transitionMatrix.getRowGroupCount());
69 std::vector<ValueType> choiceValues(weightedRewardVector.size());
70 std::vector<ValueType> temporaryResult(this->transitionMatrix.getRowGroupCount());
72 std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> stepBounds;
73 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
74 if (this->objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) {
75 auto const& subformula = this->objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula();
76 uint_fast64_t stepBound = subformula.template getBound<uint_fast64_t>();
77 if (subformula.isBoundStrict()) {
80 auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound,
storm::storage::BitVector(this->objectives.size(),
false))).first;
81 stepBoundIt->second.set(objIndex);
84 this->offsetsToUnderApproximation[objIndex] = storm::utility::zero<ValueType>();
85 this->offsetsToOverApproximation[objIndex] = storm::utility::zero<ValueType>();
92 auto stepBoundIt = stepBounds.
begin();
93 uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first;
95 while (currentEpoch > 0) {
96 if (stepBoundIt != stepBounds.end() && currentEpoch == stepBoundIt->first) {
97 consideredObjectives |= stepBoundIt->second;
98 for (
auto objIndex : stepBoundIt->second) {
101 storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
108 this->transitionMatrix.multiplyWithVector(this->weightedResult, choiceValues);
113 for (
auto objIndex : consideredObjectives) {
114 std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex];
115 std::vector<ValueType>
const& objectiveRewards = this->actionRewards[objIndex];
116 auto rowGroupIndexIt = this->transitionMatrix.getRowGroupIndices().begin();
117 auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin();
118 for (ValueType& stateValue : temporaryResult) {
119 uint_fast64_t row = (*rowGroupIndexIt) + (*optimalChoiceIt);
122 stateValue = objectiveRewards[row];
123 for (
auto const& entry : this->transitionMatrix.getRow(row)) {
124 stateValue += entry.getValue() * objectiveResult[entry.getColumn()];
127 objectiveResult.swap(temporaryResult);
133template class StandardMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>;
134#ifdef STORM_HAVE_CARL
135template class StandardMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
Helper class for model checking queries that depend on the long run behavior of the (nondeterministic...
Helper class for model checking queries that depend on the long run behavior of the (nondeterministic...
Helper Class that takes preprocessed Pcaa data and a weight vector and ...
virtual storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper< ValueType > createNondetInfiniteHorizonHelper(storm::storage::SparseMatrix< ValueType > const &transitions) const override
StandardMdpPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult< SparseMdpModelType > const &preprocessorResult)
virtual void initializeModelTypeSpecificData(SparseMdpModelType const &model) override
virtual storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper< ValueType > createDetInfiniteHorizonHelper(storm::storage::SparseMatrix< ValueType > const &transitions) const override
Helper Class that takes preprocessed Pcaa data and a weight vector and ...
void initialize(preprocessing::SparseMultiObjectivePreprocessorResult< SparseMdpModelType > const &preprocessorResult)
A bit vector that is internally represented as a vector of 64-bit values.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
A class that holds a possibly non-square matrix in the compressed row storage format.
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
bool constexpr minimize(OptimizationDirection d)
void addVectors(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Adds the two given vectors and writes the result to the target vector.
void addScaledVector(std::vector< InValueType1 > &firstOperand, std::vector< InValueType2 > const &secondOperand, InValueType3 const &factor)
Computes x:= x + a*y, i.e., adds each element of the first vector and (the corresponding element of t...
void reduceVectorMax(std::vector< T > const &source, std::vector< T > &target, std::vector< uint_fast64_t > const &rowGrouping, std::vector< uint_fast64_t > *choices=nullptr)
Reduces the given source vector by selecting the largest element out of each row group.