Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StandardMdpPcaaWeightVectorChecker.cpp
Go to the documentation of this file.
2
10
15
16namespace storm {
17namespace modelchecker {
18namespace multiobjective {
19
20template<class SparseMdpModelType>
26
27template<class SparseMdpModelType>
29 // set the state action rewards. Also do some sanity checks on the objectives.
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());
39 } else {
40 STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula() || formula.getSubformula().isLongRunAverageRewardFormula(),
41 storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula());
42 }
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());
47 }
48}
49
50template<class SparseMdpModelType>
56
57template<class SparseMdpModelType>
60 STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix.");
62}
63
64template<class SparseMdpModelType>
65void StandardMdpPcaaWeightVectorChecker<SparseMdpModelType>::boundedPhase(Environment const& env, std::vector<ValueType> const& weightVector,
66 std::vector<ValueType>& weightedRewardVector) {
67 // Allocate some memory so this does not need to happen for each time epoch
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());
71 // Get for each occurring timeBound the indices of the objectives with that bound.
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()) {
78 --stepBound;
79 }
80 auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first;
81 stepBoundIt->second.set(objIndex);
82
83 // There is no error for the values of these objectives.
84 this->offsetsToUnderApproximation[objIndex] = storm::utility::zero<ValueType>();
85 this->offsetsToOverApproximation[objIndex] = storm::utility::zero<ValueType>();
86 }
87 }
88
89 // Stores the objectives for which we need to compute values in the current time epoch.
90 storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound & ~this->lraObjectives;
91
92 auto stepBoundIt = stepBounds.begin();
93 uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first;
94
95 while (currentEpoch > 0) {
96 if (stepBoundIt != stepBounds.end() && currentEpoch == stepBoundIt->first) {
97 consideredObjectives |= stepBoundIt->second;
98 for (auto objIndex : stepBoundIt->second) {
99 // This objective now plays a role in the weighted sum
100 ValueType factor =
101 storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
102 storm::utility::vector::addScaledVector(weightedRewardVector, this->actionRewards[objIndex], factor);
103 }
104 ++stepBoundIt;
105 }
106
107 // Get values and scheduler for weighted sum of objectives
108 this->transitionMatrix.multiplyWithVector(this->weightedResult, choiceValues);
109 storm::utility::vector::addVectors(choiceValues, weightedRewardVector, choiceValues);
110 storm::utility::vector::reduceVectorMax(choiceValues, this->weightedResult, this->transitionMatrix.getRowGroupIndices(), &optimalChoicesInCurrentEpoch);
111
112 // get values for individual objectives
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);
120 ++rowGroupIndexIt;
121 ++optimalChoiceIt;
122 stateValue = objectiveRewards[row];
123 for (auto const& entry : this->transitionMatrix.getRow(row)) {
124 stateValue += entry.getValue() * objectiveResult[entry.getColumn()];
125 }
126 }
127 objectiveResult.swap(temporaryResult);
128 }
129 --currentEpoch;
130 }
131}
132
133template class StandardMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>;
134#ifdef STORM_HAVE_CARL
135template class StandardMdpPcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
136#endif
137
138} // namespace multiobjective
139} // namespace modelchecker
140} // namespace storm
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.
Definition BitVector.h:18
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)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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.
Definition vector.h:443
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...
Definition vector.h:504
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.
Definition vector.h:829
LabParser.cpp.
Definition cli.cpp:18