Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
MultiDimensionalRewardUnfolding.cpp
Go to the documentation of this file.
2
3#include <functional>
4#include <set>
5#include <string>
6
9
18
20
25
26namespace storm {
27namespace modelchecker {
28namespace helper {
29namespace rewardbounded {
30
31template<typename ValueType, bool SingleObjectiveMode>
38template<typename ValueType, bool SingleObjectiveMode>
40 storm::models::sparse::Model<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula,
41 std::set<storm::expressions::Variable> const& infinityBoundVariables)
42 : model(model) {
43 STORM_LOG_TRACE("initializing multi-dimensional reward unfolding for formula " << *objectiveFormula << " and " << infinityBoundVariables.size()
44 << " bound variables should approach infinity.");
45
46 if (objectiveFormula->isProbabilityOperatorFormula()) {
47 if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) {
48 for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) {
49 STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException,
50 "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << ".");
51 }
52 } else {
53 STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException,
54 "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << ".");
55 }
56 } else {
57 STORM_LOG_THROW(objectiveFormula->isRewardOperatorFormula() && objectiveFormula->getSubformula().isCumulativeRewardFormula(),
58 storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported.");
59 }
60
61 // Build an objective from the formula.
63 objective.formula = objectiveFormula;
64 objective.originalFormula = objective.formula;
65 objective.considersComplementaryEvent = false;
66 objectives.push_back(std::move(objective));
68 initialize(infinityBoundVariables);
69}
70
71template<typename ValueType, bool SingleObjectiveMode>
72void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initialize(std::set<storm::expressions::Variable> const& infinityBoundVariables) {
73 STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives.");
74 std::vector<Epoch> epochSteps;
75 initializeObjectives(epochSteps, infinityBoundVariables);
76 initializeMemoryProduct(epochSteps);
78 // collect which epoch steps are possible
79 possibleEpochSteps.clear();
80 for (auto const& step : epochSteps) {
81 possibleEpochSteps.insert(step);
82 }
83}
85template<typename ValueType, bool SingleObjectiveMode>
87 std::vector<Epoch>& epochSteps, std::set<storm::expressions::Variable> const& infinityBoundVariables) {
88 std::vector<std::vector<uint64_t>> dimensionWiseEpochSteps;
89 // collect the time-bounded subobjectives
90 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
91 auto const& formula = *this->objectives[objIndex].formula;
92 if (formula.isProbabilityOperatorFormula()) {
93 STORM_LOG_THROW(formula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException,
94 "Unexpected type of subformula for formula " << formula);
95 auto const& subformula = formula.getSubformula().asBoundedUntilFormula();
96 for (uint64_t dim = 0; dim < subformula.getDimension(); ++dim) {
97 Dimension<ValueType> dimension;
98 dimension.formula = subformula.restrictToDimension(dim);
99 dimension.objectiveIndex = objIndex;
100 std::string memLabel = "dim" + std::to_string(dimensions.size()) + "_maybe";
101 while (model.getStateLabeling().containsLabel(memLabel)) {
102 memLabel = "_" + memLabel;
103 }
104 dimension.memoryLabel = memLabel;
105 // for simplicity we do not allow interval formulas.
106 STORM_LOG_THROW(!subformula.hasLowerBound(dim) || !subformula.hasUpperBound(dim), storm::exceptions::NotSupportedException,
107 "Bounded until formulas are only supported by this method if they consider either an upper bound or a lower bound. Got "
108 << subformula << " instead.");
109 // lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the
110 // ProductModel::transformMemoryState method).
112 subformula.hasUpperBound(dim) || subformula.getLeftSubformula(dim).isTrueFormula(), storm::exceptions::NotSupportedException,
113 "Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got " << subformula << " instead.");
114
115 // Treat formulas that aren't acutally bounded differently
116 bool formulaUnbounded =
117 (!subformula.hasLowerBound(dim) && !subformula.hasUpperBound(dim)) ||
118 (subformula.hasLowerBound(dim) && !subformula.isLowerBoundStrict(dim) && !subformula.getLowerBound(dim).containsVariables() &&
119 storm::utility::isZero(subformula.getLowerBound(dim).evaluateAsRational())) ||
120 (subformula.hasUpperBound(dim) && subformula.getUpperBound(dim).isVariable() &&
121 infinityBoundVariables.count(subformula.getUpperBound(dim).getBaseExpression().asVariableExpression().getVariable()) > 0);
122 if (formulaUnbounded) {
123 dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getTransitionMatrix().getRowCount(), 0));
124 dimension.scalingFactor = storm::utility::zero<ValueType>();
126 } else {
127 if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) {
128 dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getTransitionMatrix().getRowCount(), 1));
129 dimension.scalingFactor = storm::utility::one<ValueType>();
130 } else {
131 STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound.");
132 STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).hasRewardModelName() || this->model.hasUniqueRewardModel(),
133 "Model has several reward models, but no reward model has been specified in the formula.");
134 std::string const& rewardName = subformula.getTimeBoundReference(dim).hasRewardModelName()
135 ? subformula.getTimeBoundReference(dim).getRewardName()
136 : this->model.getUniqueRewardModelName();
137 STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException,
138 "No reward model with name '" << rewardName << "' found.");
139 auto const& rewardModel = this->model.getRewardModel(rewardName);
140 STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException,
141 "Transition rewards are currently not supported as reward bounds.");
142 std::vector<ValueType> actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix());
143 auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector<ValueType, uint64_t>(actionRewards);
144 dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first));
145 dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second);
146 }
147 if (subformula.hasLowerBound(dim)) {
148 if (subformula.getLowerBound(dim).isVariable() &&
149 infinityBoundVariables.count(subformula.getLowerBound(dim).getBaseExpression().asVariableExpression().getVariable()) > 0) {
151 } else {
153 }
154 } else {
156 }
157 }
158 dimensions.emplace_back(std::move(dimension));
159 }
160 } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) {
161 auto const& subformula = formula.getSubformula().asCumulativeRewardFormula();
162 for (uint64_t dim = 0; dim < subformula.getDimension(); ++dim) {
163 Dimension<ValueType> dimension;
164 dimension.formula = subformula.restrictToDimension(dim);
165 STORM_LOG_THROW(!(dimension.formula->asCumulativeRewardFormula().getBound().isVariable() &&
166 infinityBoundVariables.count(
167 dimension.formula->asCumulativeRewardFormula().getBound().getBaseExpression().asVariableExpression().getVariable()) > 0),
168 storm::exceptions::NotSupportedException, "Letting cumulative reward bounds approach infinite is not supported.");
169 dimension.objectiveIndex = objIndex;
171 if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) {
172 dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getTransitionMatrix().getRowCount(), 1));
173 dimension.scalingFactor = storm::utility::one<ValueType>();
174 } else {
175 STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound.");
176 std::string const& rewardName = subformula.getTimeBoundReference(dim).getRewardName();
177 STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException,
178 "No reward model with name '" << rewardName << "' found.");
179 auto const& rewardModel = this->model.getRewardModel(rewardName);
180 STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException,
181 "Transition rewards are currently not supported as reward bounds.");
182 std::vector<ValueType> actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix());
183 auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector<ValueType, uint64_t>(actionRewards);
184 dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first));
185 dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second);
186 }
187 dimensions.emplace_back(std::move(dimension));
188 }
189 }
190 }
191
192 // Compute a mapping for each objective to the set of dimensions it considers
193 // Also store for each dimension dim, which dimensions should be unsatisfiable whenever the bound of dim is violated
194 uint64_t dim = 0;
195 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
196 storm::storage::BitVector objDimensions(dimensions.size(), false);
197 uint64_t objDimensionCount = 0;
198 bool objDimensionsCanBeSatisfiedIndividually = false;
199 if (objectives[objIndex].formula->isProbabilityOperatorFormula() && objectives[objIndex].formula->getSubformula().isBoundedUntilFormula()) {
200 objDimensionCount = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula().getDimension();
201 objDimensionsCanBeSatisfiedIndividually = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula().hasMultiDimensionalSubformulas();
202 } else if (objectives[objIndex].formula->isRewardOperatorFormula() && objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) {
203 objDimensionCount = objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula().getDimension();
204 }
205 for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim) {
206 objDimensions.set(currDim);
207 }
208 for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim) {
209 if (!objDimensionsCanBeSatisfiedIndividually || dimensions[currDim].boundType == DimensionBoundType::UpperBound) {
210 dimensions[currDim].dependentDimensions = objDimensions;
211 } else {
212 dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false);
213 dimensions[currDim].dependentDimensions.set(currDim, true);
214 }
215 }
216 dim += objDimensionCount;
217 objectiveDimensions.push_back(std::move(objDimensions));
218 }
219 assert(dim == dimensions.size());
220
221 // Initialize the epoch manager
222 epochManager = EpochManager(dimensions.size());
223
224 // Convert the epoch steps to a choice-wise representation
225 epochSteps.reserve(model.getTransitionMatrix().getRowCount());
226 for (uint64_t choice = 0; choice < model.getTransitionMatrix().getRowCount(); ++choice) {
227 Epoch step;
228 uint64_t dim = 0;
229 for (auto const& dimensionSteps : dimensionWiseEpochSteps) {
230 epochManager.setDimensionOfEpoch(step, dim, dimensionSteps[choice]);
231 ++dim;
232 }
233 epochSteps.push_back(step);
234 }
235
236 // Set the maximal values we need to consider for each dimension
237 computeMaxDimensionValues();
238 translateLowerBoundInfinityDimensions(epochSteps);
239}
240
241template<typename ValueType, bool SingleObjectiveMode>
243 productModel = std::make_unique<ProductModel<ValueType>>(model, objectives, dimensions, objectiveDimensions, epochManager, epochSteps);
244}
245
246template<typename ValueType, bool SingleObjectiveMode>
247void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::computeMaxDimensionValues() {
248 for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
250 bool isStrict = false;
251 storm::logic::Formula const& dimFormula = *dimensions[dim].formula;
252 if (dimFormula.isBoundedUntilFormula()) {
254 if (dimFormula.asBoundedUntilFormula().hasUpperBound()) {
255 STORM_LOG_ASSERT(!dimFormula.asBoundedUntilFormula().hasLowerBound(), "Bounded until formulas with interval bounds are not supported.");
256 bound = dimFormula.asBoundedUntilFormula().getUpperBound();
257 isStrict = dimFormula.asBoundedUntilFormula().isUpperBoundStrict();
258 } else {
259 STORM_LOG_ASSERT(dimFormula.asBoundedUntilFormula().hasLowerBound(), "Bounded until formulas without any bounds are not supported.");
260 bound = dimFormula.asBoundedUntilFormula().getLowerBound();
261 isStrict = dimFormula.asBoundedUntilFormula().isLowerBoundStrict();
262 }
263 } else if (dimFormula.isCumulativeRewardFormula()) {
264 assert(!dimFormula.asCumulativeRewardFormula().isMultiDimensional());
265 bound = dimFormula.asCumulativeRewardFormula().getBound();
266 isStrict = dimFormula.asCumulativeRewardFormula().isBoundStrict();
267 }
268
269 if (!bound.containsVariables()) {
270 // We always consider upper bounds to be non-strict and lower bounds to be strict.
271 // Thus, >=N would become >N-1. However, note that the case N=0 is treated separately.
272 if (dimensions[dim].boundType == DimensionBoundType::LowerBound || dimensions[dim].boundType == DimensionBoundType::UpperBound) {
273 ValueType discretizedBound = storm::utility::convertNumber<ValueType>(bound.evaluateAsRational());
274 discretizedBound /= dimensions[dim].scalingFactor;
275 if (storm::utility::isInteger(discretizedBound)) {
276 if (isStrict == (dimensions[dim].boundType == DimensionBoundType::UpperBound)) {
277 discretizedBound -= storm::utility::one<ValueType>();
278 }
279 } else {
280 discretizedBound = storm::utility::floor(discretizedBound);
281 }
282 uint64_t dimensionValue = storm::utility::convertNumber<uint64_t>(discretizedBound);
283 STORM_LOG_THROW(epochManager.isValidDimensionValue(dimensionValue), storm::exceptions::NotSupportedException,
284 "The bound " << bound << " is too high for the considered number of dimensions.");
285 dimensions[dim].maxValue = dimensionValue;
286 }
287 }
288 }
289}
290
291template<typename ValueType, bool SingleObjectiveMode>
292void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::translateLowerBoundInfinityDimensions(std::vector<Epoch>& epochSteps) {
293 // Translate lowerBoundedByInfinity dimensions to finite bounds
294 storm::storage::BitVector infLowerBoundedDimensions(dimensions.size(), false);
295 storm::storage::BitVector upperBoundedDimensions(dimensions.size(), false);
296 for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
297 infLowerBoundedDimensions.set(dim, dimensions[dim].boundType == DimensionBoundType::LowerBoundInfinity);
298 upperBoundedDimensions.set(dim, dimensions[dim].boundType == DimensionBoundType::UpperBound);
299 }
300 if (!infLowerBoundedDimensions.empty()) {
301 // We can currently only handle this case for single maximizing bounded until probability objectives.
302 // The approach is to erase all epochSteps that are not part of an end component and then change the reward bound to '> 0'.
303 // Then, reaching a reward means reaching an end component where arbitrarily many reward can be collected.
305 SingleObjectiveMode, storm::exceptions::NotSupportedException,
306 "Letting lower bounds approach infinity is only supported in single objective mode."); // It most likely also works with multiple objectives with
307 // the same shape. However, we haven't checked this yet.
308 STORM_LOG_THROW(objectives.front().formula->isProbabilityOperatorFormula(), storm::exceptions::NotSupportedException,
309 "Letting lower bounds approach infinity is only supported for probability operator formulas");
310 auto const& probabilityOperatorFormula = objectives.front().formula->asProbabilityOperatorFormula();
311 STORM_LOG_THROW(probabilityOperatorFormula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException,
312 "Letting lower bounds approach infinity is only supported for bounded until probabilities.");
314 (probabilityOperatorFormula.hasOptimalityType() && storm::solver::maximize(probabilityOperatorFormula.getOptimalityType())),
315 storm::exceptions::NotSupportedException,
316 "Letting lower bounds approach infinity is only supported for maximizing bounded until probabilities.");
317
318 STORM_LOG_THROW(upperBoundedDimensions.empty() || !probabilityOperatorFormula.getSubformula().asBoundedUntilFormula().hasMultiDimensionalSubformulas(),
319 storm::exceptions::NotSupportedException,
320 "Letting lower bounds approach infinity is only supported if the formula has either only lower bounds or if it has a single goal "
321 "state."); // This would fail because the upper bounded dimension(s) might be satisfied already. One should erase epoch steps in the
322 // epoch model (after applying the goal-unfolding).
323 storm::storage::BitVector choicesWithoutUpperBoundedStep(model.getNumberOfChoices(), true);
324 if (!upperBoundedDimensions.empty()) {
325 // To not invalidate upper-bounded dimensions, one needs to consider MECS where no reward for such a dimension is collected.
326 for (uint64_t choiceIndex = 0; choiceIndex < model.getNumberOfChoices(); ++choiceIndex) {
327 for (auto dim : upperBoundedDimensions) {
328 if (epochManager.getDimensionOfEpoch(epochSteps[choiceIndex], dim) != 0) {
329 choicesWithoutUpperBoundedStep.set(choiceIndex, false);
330 break;
331 }
332 }
333 }
334 }
337 choicesWithoutUpperBoundedStep);
338 storm::storage::BitVector nonMecChoices(model.getNumberOfChoices(), true);
339 for (auto const& mec : mecDecomposition) {
340 for (auto const& stateChoicesPair : mec) {
341 for (auto const& choice : stateChoicesPair.second) {
342 nonMecChoices.set(choice, false);
343 }
344 }
345 }
346 for (auto choice : nonMecChoices) {
347 for (auto dim : infLowerBoundedDimensions) {
348 epochManager.setDimensionOfEpoch(epochSteps[choice], dim, 0);
349 }
350 }
351
352 // Translate the dimension to '>0'
353 for (auto dim : infLowerBoundedDimensions) {
354 dimensions[dim].boundType = DimensionBoundType::LowerBound;
355 dimensions[dim].maxValue = 0;
356 }
357 }
358}
359
360template<typename ValueType, bool SingleObjectiveMode>
362 bool setUnknownDimsToBottom) {
363 Epoch startEpoch = epochManager.getZeroEpoch();
364 for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
365 if (dimensions[dim].maxValue) {
366 epochManager.setDimensionOfEpoch(startEpoch, dim, dimensions[dim].maxValue.get());
367 } else {
368 STORM_LOG_THROW(setUnknownDimsToBottom || dimensions[dim].boundType == DimensionBoundType::Unbounded, storm::exceptions::UnexpectedException,
369 "Tried to obtain the start epoch although no bound on dimension " << dim << " is known.");
370 epochManager.setBottomDimension(startEpoch, dim);
371 }
372 }
373 STORM_LOG_TRACE("Start epoch is " << epochManager.toString(startEpoch));
374 return startEpoch;
375}
376
377template<typename ValueType, bool SingleObjectiveMode>
378std::vector<typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch>
380 // Perform a DFS to find all the reachable epochs
381 std::vector<Epoch> dfsStack;
382 std::set<Epoch, std::function<bool(Epoch const&, Epoch const&)>> collectedEpochs(
383 std::bind(&EpochManager::epochClassZigZagOrder, &epochManager, std::placeholders::_1, std::placeholders::_2));
384
385 if (!stopAtComputedEpochs || epochSolutions.count(startEpoch) == 0) {
386 collectedEpochs.insert(startEpoch);
387 dfsStack.push_back(startEpoch);
388 }
389 while (!dfsStack.empty()) {
390 Epoch currentEpoch = dfsStack.back();
391 dfsStack.pop_back();
392 for (auto const& step : possibleEpochSteps) {
393 Epoch successorEpoch = epochManager.getSuccessorEpoch(currentEpoch, step);
394 if (!stopAtComputedEpochs || epochSolutions.count(successorEpoch) == 0) {
395 if (collectedEpochs.insert(successorEpoch).second) {
396 dfsStack.push_back(std::move(successorEpoch));
397 }
398 }
399 }
400 }
401 return std::vector<Epoch>(collectedEpochs.begin(), collectedEpochs.end());
402}
403
404template<typename ValueType, bool SingleObjectiveMode>
406 STORM_LOG_DEBUG("Setting model for epoch " << epochManager.toString(epoch));
407
408 // Check if we need to update the current epoch class
409 if (!currentEpoch || !epochManager.compareEpochClass(epoch, currentEpoch.get())) {
410 setCurrentEpochClass(epoch);
411 epochModel.epochMatrixChanged = true;
413 if (storm::utility::graph::hasCycle(epochModel.epochMatrix)) {
414 std::cout << "Epoch model for epoch " << epochManager.toString(epoch) << " is cyclic.\n";
415 }
416 }
417 } else {
418 epochModel.epochMatrixChanged = false;
419 }
420
421 bool containsLowerBoundedObjective = false;
422 for (auto const& dimension : dimensions) {
423 if (dimension.boundType == DimensionBoundType::LowerBound) {
424 containsLowerBoundedObjective = true;
425 break;
426 }
427 }
428 std::map<Epoch, EpochSolution const*> subSolutions;
429 for (auto const& step : possibleEpochSteps) {
430 Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, step);
431 if (successorEpoch != epoch) {
432 auto successorSolIt = epochSolutions.find(successorEpoch);
433 STORM_LOG_ASSERT(successorSolIt != epochSolutions.end(), "Solution for successor epoch does not exist (anymore).");
434 subSolutions.emplace(successorEpoch, &successorSolIt->second);
435 }
436 }
437 epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
438 auto stepSolIt = epochModel.stepSolutions.begin();
439 for (auto reducedChoice : epochModel.stepChoices) {
440 uint64_t productChoice = epochModelToProductChoiceMap[reducedChoice];
441 uint64_t productState = productModel->getProductStateFromChoice(productChoice);
442 auto const& memoryState = productModel->getMemoryState(productState);
443 Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, productModel->getSteps()[productChoice]);
444 EpochClass successorEpochClass = epochManager.getEpochClass(successorEpoch);
445 // Find out whether objective reward is earned for the current choice
446 // Objective reward is not earned if
447 // a) there is an upper bounded subObjective that is __still_relevant__ but the corresponding reward bound is passed after taking the choice
448 // b) there is a lower bounded subObjective and the corresponding reward bound is not passed yet.
449 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
450 bool rewardEarned = !storm::utility::isZero(epochModel.objectiveRewards[objIndex][reducedChoice]);
451 if (rewardEarned) {
452 for (auto dim : objectiveDimensions[objIndex]) {
453 if ((dimensions[dim].boundType == DimensionBoundType::UpperBound) == epochManager.isBottomDimension(successorEpoch, dim) &&
454 productModel->getMemoryStateManager().isRelevantDimension(memoryState, dim)) {
455 rewardEarned = false;
456 break;
457 }
458 }
459 }
460 epochModel.objectiveRewardFilter[objIndex].set(reducedChoice, rewardEarned);
461 }
462 // compute the solution for the stepChoices
463 // For optimization purposes, we distinguish the case where the memory state does not have to be transformed
464 EpochSolution const& successorEpochSolution = getEpochSolution(subSolutions, successorEpoch);
465 SolutionType choiceSolution;
466 bool firstSuccessor = true;
467 if (!containsLowerBoundedObjective && epochManager.compareEpochClass(epoch, successorEpoch)) {
468 for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
469 if (firstSuccessor) {
470 choiceSolution = getScaledSolution(getStateSolution(successorEpochSolution, successor.getColumn()), successor.getValue());
471 firstSuccessor = false;
472 } else {
473 addScaledSolution(choiceSolution, getStateSolution(successorEpochSolution, successor.getColumn()), successor.getValue());
474 }
475 }
476 } else {
477 for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
478 uint64_t successorProductState = productModel->transformProductState(successor.getColumn(), successorEpochClass, memoryState);
479 SolutionType const& successorSolution = getStateSolution(successorEpochSolution, successorProductState);
480 if (firstSuccessor) {
481 choiceSolution = getScaledSolution(successorSolution, successor.getValue());
482 firstSuccessor = false;
483 } else {
484 addScaledSolution(choiceSolution, successorSolution, successor.getValue());
485 }
486 }
487 }
488 assert(!firstSuccessor);
489 *stepSolIt = std::move(choiceSolution);
490 ++stepSolIt;
491 }
492
493 assert(epochModel.objectiveRewards.size() == objectives.size());
494 assert(epochModel.objectiveRewardFilter.size() == objectives.size());
495 assert(epochModel.epochMatrix.getRowCount() == epochModel.stepChoices.size());
496 assert(epochModel.stepChoices.size() == epochModel.objectiveRewards.front().size());
497 assert(epochModel.objectiveRewards.front().size() == epochModel.objectiveRewards.back().size());
498 assert(epochModel.objectiveRewards.front().size() == epochModel.objectiveRewardFilter.front().size());
499 assert(epochModel.objectiveRewards.back().size() == epochModel.objectiveRewardFilter.back().size());
500 assert(epochModel.stepChoices.getNumberOfSetBits() == epochModel.stepSolutions.size());
501
502 currentEpoch = epoch;
503 /*
504 std::cout << "Epoch model for epoch " << storm::utility::vector::toString(epoch) << '\n';
505 std::cout << "Matrix: \n" << epochModel.epochMatrix << '\n';
506 std::cout << "ObjectiveRewards: " << storm::utility::vector::toString(epochModel.objectiveRewards[0]) << '\n';
507 std::cout << "steps: " << epochModel.stepChoices << '\n';
508 std::cout << "step solutions: ";
509 for (int i = 0; i < epochModel.stepSolutions.size(); ++i) {
510 std::cout << " " << epochModel.stepSolutions[i].weightedValue;
511 }
512 std::cout << '\n';
513 */
514 return epochModel;
515}
516
517template<typename ValueType, bool SingleObjectiveMode>
519 EpochClass epochClass = epochManager.getEpochClass(epoch);
520 // std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << '\n';
521 auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives);
522
523 storm::storage::BitVector stepChoices(productModel->getProduct().getTransitionMatrix().getRowCount(), false);
524 uint64_t choice = 0;
525 for (auto const& step : productModel->getSteps()) {
526 if (!epochManager.isZeroEpoch(step) && epochManager.getSuccessorEpoch(epoch, step) != epoch) {
527 stepChoices.set(choice, true);
528 }
529 ++choice;
530 }
531 epochModel.epochMatrix = productModel->getProduct().getTransitionMatrix().filterEntries(~stepChoices);
532 // redirect transitions for the case where the lower reward bounds are not met yet
533 storm::storage::BitVector violatedLowerBoundedDimensions(dimensions.size(), false);
534 for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
535 if (dimensions[dim].boundType == DimensionBoundType::LowerBound && !epochManager.isBottomDimensionEpochClass(epochClass, dim)) {
536 violatedLowerBoundedDimensions.set(dim);
537 }
538 }
539 if (!violatedLowerBoundedDimensions.empty()) {
540 for (uint64_t state = 0; state < epochModel.epochMatrix.getRowGroupCount(); ++state) {
541 auto const& memoryState = productModel->getMemoryState(state);
542 for (auto& entry : epochModel.epochMatrix.getRowGroup(state)) {
543 entry.setColumn(productModel->transformProductState(entry.getColumn(), epochClass, memoryState));
544 }
545 }
546 }
547
548 storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getTransitionMatrix().getRowCount(), true);
549 for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
550 if (violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) {
551 zeroObjRewardChoices &= storm::utility::vector::filterZero(productObjectiveRewards[objIndex]);
552 }
553 }
554 storm::storage::BitVector allProductStates(productModel->getProduct().getNumberOfStates(), true);
555
556 // Get the relevant states for this epoch.
557 storm::storage::BitVector productInStates = productModel->getInStates(epochClass);
558 // The epoch model only needs to consider the states that are reachable from a relevant state
559 storm::storage::BitVector consideredStates =
560 storm::utility::graph::getReachableStates(epochModel.epochMatrix, productInStates, allProductStates, ~allProductStates);
561
562 // We assume that there is no end component in which objective reward is earned
563 STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix, epochModel.epochMatrix.transpose(true), allProductStates,
564 ~zeroObjRewardChoices & ~stepChoices),
565 "There is a scheduler that yields infinite reward for one objective. This case should be excluded");
566
567 // Create the epoch model matrix
568 std::vector<uint64_t> productToEpochModelStateMapping;
570 assert(zeroObjRewardChoices.size() == productModel->getProduct().getNumberOfStates());
571 assert(stepChoices.size() == productModel->getProduct().getNumberOfStates());
572 STORM_LOG_ASSERT(epochModel.equationSolverProblemFormat.is_initialized(), "Linear equation problem format was not set.");
573 bool convertToEquationSystem = epochModel.equationSolverProblemFormat.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
574 // For DTMCs we consider the subsystem induced by the considered states.
575 // The transitions for states with zero reward are filtered out to guarantee a unique solution of the eq-system.
576 auto backwardTransitions = epochModel.epochMatrix.transpose(true);
577 storm::storage::BitVector nonZeroRewardStates =
578 storm::utility::graph::performProbGreater0(backwardTransitions, consideredStates, consideredStates & (~zeroObjRewardChoices | stepChoices));
579 // If there is at least one considered state with reward zero, we have to add a 'zero-reward-state' to the epoch model.
580 bool requiresZeroRewardState = nonZeroRewardStates != consideredStates;
581 uint64_t numEpochModelStates = nonZeroRewardStates.getNumberOfSetBits();
582 uint64_t zeroRewardInState = numEpochModelStates;
583 if (requiresZeroRewardState) {
584 ++numEpochModelStates;
585 }
587 if (!nonZeroRewardStates.empty()) {
589 epochModel.epochMatrix.getSubmatrix(true, nonZeroRewardStates, nonZeroRewardStates, convertToEquationSystem));
590 }
591 if (requiresZeroRewardState) {
592 if (convertToEquationSystem) {
593 // add a diagonal entry
594 builder.addNextValue(zeroRewardInState, zeroRewardInState, storm::utility::zero<ValueType>());
595 }
596 epochModel.epochMatrix = builder.build(numEpochModelStates, numEpochModelStates);
597 } else {
598 assert(!nonZeroRewardStates.empty());
599 epochModel.epochMatrix = builder.build();
600 }
601 if (convertToEquationSystem) {
602 epochModel.epochMatrix.convertToEquationSystem();
603 }
604
605 epochModelToProductChoiceMap.clear();
606 epochModelToProductChoiceMap.reserve(numEpochModelStates);
607 productToEpochModelStateMapping.assign(nonZeroRewardStates.size(), zeroRewardInState);
608 for (auto productState : nonZeroRewardStates) {
609 productToEpochModelStateMapping[productState] = epochModelToProductChoiceMap.size();
610 epochModelToProductChoiceMap.push_back(productState);
611 }
612 if (requiresZeroRewardState) {
613 uint64_t zeroRewardProductState = (consideredStates & ~nonZeroRewardStates).getNextSetIndex(0);
614 assert(zeroRewardProductState < consideredStates.size());
615 epochModelToProductChoiceMap.push_back(zeroRewardProductState);
616 }
617 } else if (model.isOfType(storm::models::ModelType::Mdp)) {
618 // Eliminate zero-reward end components
619 auto ecElimResult = storm::transformer::EndComponentEliminator<ValueType>::transform(epochModel.epochMatrix, consideredStates,
620 zeroObjRewardChoices & ~stepChoices, consideredStates);
621 epochModel.epochMatrix = std::move(ecElimResult.matrix);
622 epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping);
623 productToEpochModelStateMapping = std::move(ecElimResult.oldToNewStateMapping);
624 } else {
625 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unsupported model type.");
626 }
627
628 epochModel.stepChoices = storm::storage::BitVector(epochModel.epochMatrix.getRowCount(), false);
629 for (uint64_t choice = 0; choice < epochModel.epochMatrix.getRowCount(); ++choice) {
630 if (stepChoices.get(epochModelToProductChoiceMap[choice])) {
631 epochModel.stepChoices.set(choice, true);
632 }
633 }
634
635 epochModel.objectiveRewards.clear();
636 for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
637 std::vector<ValueType> const& productObjRew = productObjectiveRewards[objIndex];
638 std::vector<ValueType> reducedModelObjRewards;
639 reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount());
640 for (auto const& productChoice : epochModelToProductChoiceMap) {
641 reducedModelObjRewards.push_back(productObjRew[productChoice]);
642 }
643 // Check if the objective is violated in the current epoch
644 if (!violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) {
645 storm::utility::vector::setVectorValues(reducedModelObjRewards, ~epochModel.stepChoices, storm::utility::zero<ValueType>());
646 }
647 epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards));
648 }
649
650 epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false);
651 for (auto productState : productInStates) {
652 STORM_LOG_ASSERT(productToEpochModelStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(),
653 "Selected product state does not exist in the epoch model.");
654 epochModel.epochInStates.set(productToEpochModelStateMapping[productState], true);
655 }
656
657 std::vector<uint64_t> toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits<uint64_t>::max());
658 std::vector<uint64_t> epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices();
659 for (auto productState : productInStates) {
660 toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[productToEpochModelStateMapping[productState]];
661 }
662 productStateToEpochModelInStateMap = std::make_shared<std::vector<uint64_t> const>(std::move(toEpochModelInStatesMap));
663
664 epochModel.objectiveRewardFilter.clear();
665 for (auto const& objRewards : epochModel.objectiveRewards) {
666 epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards));
667 epochModel.objectiveRewardFilter.back().complement();
668 }
669}
670
671template<typename ValueType, bool SingleObjectiveMode>
674 STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Dtmc), "Trying to set the equation problem format although the model is not deterministic.");
675 epochModel.equationSolverProblemFormat = eqSysFormat;
676}
677
678template<typename ValueType, bool SingleObjectiveMode>
679template<bool SO, typename std::enable_if<SO, int>::type>
681MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const {
682 return solution * scalingFactor;
683}
684
685template<typename ValueType, bool SingleObjectiveMode>
686template<bool SO, typename std::enable_if<!SO, int>::type>
688MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const {
689 SolutionType res;
690 res.reserve(solution.size());
691 for (auto const& sol : solution) {
692 res.push_back(sol * scalingFactor);
693 }
694 return res;
695}
696
697template<typename ValueType, bool SingleObjectiveMode>
698template<bool SO, typename std::enable_if<SO, int>::type>
699void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd,
700 ValueType const& scalingFactor) const {
701 solution += solutionToAdd * scalingFactor;
702}
703
704template<typename ValueType, bool SingleObjectiveMode>
705template<bool SO, typename std::enable_if<!SO, int>::type>
706void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd,
707 ValueType const& scalingFactor) const {
708 storm::utility::vector::addScaledVector(solution, solutionToAdd, scalingFactor);
709}
710
711template<typename ValueType, bool SingleObjectiveMode>
712template<bool SO, typename std::enable_if<SO, int>::type>
713void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionEntry(SolutionType& solution, uint64_t objIndex,
714 ValueType const& value) const {
715 STORM_LOG_ASSERT(objIndex == 0, "Invalid objective index in single objective mode");
716 solution = value;
717}
718
719template<typename ValueType, bool SingleObjectiveMode>
720template<bool SO, typename std::enable_if<!SO, int>::type>
721void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionEntry(SolutionType& solution, uint64_t objIndex,
722 ValueType const& value) const {
723 STORM_LOG_ASSERT(objIndex < solution.size(), "Invalid objective index " << objIndex << ".");
724 solution[objIndex] = value;
725}
726
727template<typename ValueType, bool SingleObjectiveMode>
728template<bool SO, typename std::enable_if<SO, int>::type>
729std::string MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::solutionToString(SolutionType const& solution) const {
730 std::stringstream stringstream;
731 stringstream << solution;
732 return stringstream.str();
733}
734
735template<typename ValueType, bool SingleObjectiveMode>
736template<bool SO, typename std::enable_if<!SO, int>::type>
737std::string MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::solutionToString(SolutionType const& solution) const {
738 std::stringstream stringstream;
739 stringstream << "(";
740 bool first = true;
741 for (auto const& s : solution) {
742 if (first) {
743 first = false;
744 } else {
745 stringstream << ", ";
746 }
747 stringstream << s;
748 }
749 stringstream << ")";
750 return stringstream.str();
751}
752
753template<typename ValueType, bool SingleObjectiveMode>
755 return precision / storm::utility::convertNumber<ValueType>(epochManager.getSumOfDimensions(startEpoch) + 1);
756}
757
758template<typename ValueType, bool SingleObjectiveMode>
760 auto& objective = this->objectives[objectiveIndex];
761 if (!objective.upperResultBound) {
762 if (objective.formula->isProbabilityOperatorFormula()) {
763 objective.upperResultBound = storm::utility::one<ValueType>();
764 } else if (objective.formula->isRewardOperatorFormula()) {
765 auto const& rewModel = this->model.getRewardModel(objective.formula->asRewardOperatorFormula().getRewardModelName());
766 auto actionRewards = rewModel.getTotalRewardVector(this->model.getTransitionMatrix());
767 if (objective.formula->getSubformula().isCumulativeRewardFormula()) {
768 // Try to get an upper bound by computing the maximal reward achievable within one epoch step
769 auto const& cumulativeRewardFormula = objective.formula->getSubformula().asCumulativeRewardFormula();
770 for (uint64_t objDim = 0; objDim < cumulativeRewardFormula.getDimension(); ++objDim) {
771 boost::optional<ValueType> resBound;
772 ValueType rewardBound = cumulativeRewardFormula.template getBound<ValueType>(objDim);
773 if (cumulativeRewardFormula.getTimeBoundReference(objDim).isRewardBound()) {
774 auto const& costModel = this->model.getRewardModel(cumulativeRewardFormula.getTimeBoundReference(objDim).getRewardName());
775 if (!costModel.hasTransitionRewards()) {
776 auto actionCosts = costModel.getTotalRewardVector(this->model.getTransitionMatrix());
777 ValueType largestRewardPerCost = storm::utility::zero<ValueType>();
778 bool isFinite = true;
779 for (auto rewIt = actionRewards.begin(), costIt = actionCosts.begin(); rewIt != actionRewards.end(); ++rewIt, ++costIt) {
780 if (!storm::utility::isZero(*rewIt)) {
781 if (storm::utility::isZero(*costIt)) {
782 isFinite = false;
783 break;
784 }
785 ValueType rewardPerCost = *rewIt / *costIt;
786 largestRewardPerCost = std::max(largestRewardPerCost, rewardPerCost);
787 }
788 }
789 if (isFinite) {
790 resBound = largestRewardPerCost * rewardBound;
791 }
792 }
793 } else {
794 resBound = (*std::max_element(actionRewards.begin(), actionRewards.end())) * rewardBound;
795 }
796 if (resBound && (!objective.upperResultBound || objective.upperResultBound.get() > resBound.get())) {
797 objective.upperResultBound = resBound;
798 }
799 }
800
801 // If we could not find an upper bound, try to get an upper bound for the unbounded case
802 if (!objective.upperResultBound) {
803 storm::storage::BitVector allStates(model.getNumberOfStates(), true);
804 // Get the set of states from which reward is reachable
805 auto nonZeroRewardStates = rewModel.getStatesWithZeroReward(model.getTransitionMatrix());
806 nonZeroRewardStates.complement();
807 auto expRewGreater0EStates = storm::utility::graph::performProbGreater0E(model.getBackwardTransitions(), allStates, nonZeroRewardStates);
808 // Eliminate zero-reward ECs
809 auto zeroRewardChoices = rewModel.getChoicesWithZeroReward(model.getTransitionMatrix());
811 zeroRewardChoices, ~allStates);
812 allStates.resize(ecElimRes.matrix.getRowGroupCount());
813 storm::storage::BitVector outStates(allStates.size(), false);
814 std::vector<ValueType> rew0StateProbs;
815 rew0StateProbs.reserve(ecElimRes.matrix.getRowCount());
816 for (uint64_t state = 0; state < allStates.size(); ++state) {
817 for (uint64_t choice = ecElimRes.matrix.getRowGroupIndices()[state]; choice < ecElimRes.matrix.getRowGroupIndices()[state + 1];
818 ++choice) {
819 // Check whether the choice lead to a state with expRew 0 in the original model
820 bool isOutChoice = false;
821 uint64_t originalModelChoice = ecElimRes.newToOldRowMapping[choice];
822 for (auto const& entry : model.getTransitionMatrix().getRow(originalModelChoice)) {
823 if (!expRewGreater0EStates.get(entry.getColumn())) {
824 isOutChoice = true;
825 outStates.set(state, true);
826 rew0StateProbs.push_back(storm::utility::one<ValueType>() - ecElimRes.matrix.getRowSum(choice));
827 assert(!storm::utility::isZero(rew0StateProbs.back()));
828 break;
829 }
830 }
831 if (!isOutChoice) {
832 rew0StateProbs.push_back(storm::utility::zero<ValueType>());
833 }
834 }
835 }
836 // An upper reward bound can only be computed if it is below infinity
837 if (storm::utility::graph::performProb1A(ecElimRes.matrix, ecElimRes.matrix.getRowGroupIndices(), ecElimRes.matrix.transpose(true),
838 allStates, outStates)
839 .full()) {
840 std::vector<ValueType> rewards;
841 rewards.reserve(ecElimRes.matrix.getRowCount());
842 for (auto row : ecElimRes.newToOldRowMapping) {
843 rewards.push_back(actionRewards[row]);
844 }
845 storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType> baier(ecElimRes.matrix, rewards, rew0StateProbs);
846 objective.upperResultBound = baier.computeUpperBound();
847 }
848 }
849 }
850 }
851 }
852 return objective.upperResultBound;
853}
854
855template<typename ValueType, bool SingleObjectiveMode>
857 auto& objective = this->objectives[objectiveIndex];
858 if (!objective.lowerResultBound) {
859 objective.lowerResultBound = storm::utility::zero<ValueType>();
860 }
861 return objective.lowerResultBound;
862}
863
864template<typename ValueType, bool SingleObjectiveMode>
866 STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before.");
867 STORM_LOG_ASSERT(inStateSolutions.size() == epochModel.epochInStates.getNumberOfSetBits(), "Invalid number of solutions.");
868
869 std::set<Epoch> predecessorEpochs, successorEpochs;
870 for (auto const& step : possibleEpochSteps) {
871 epochManager.gatherPredecessorEpochs(predecessorEpochs, currentEpoch.get(), step);
872 successorEpochs.insert(epochManager.getSuccessorEpoch(currentEpoch.get(), step));
873 }
874 predecessorEpochs.erase(currentEpoch.get());
875 successorEpochs.erase(currentEpoch.get());
876
877 // clean up solutions that are not needed anymore
878 for (auto const& successorEpoch : successorEpochs) {
879 auto successorEpochSolutionIt = epochSolutions.find(successorEpoch);
880 STORM_LOG_ASSERT(successorEpochSolutionIt != epochSolutions.end(), "Solution for successor epoch does not exist (anymore).");
881 --successorEpochSolutionIt->second.count;
882 if (successorEpochSolutionIt->second.count == 0) {
883 epochSolutions.erase(successorEpochSolutionIt);
884 }
885 }
886
887 // add the new solution
888 EpochSolution solution;
889 solution.count = predecessorEpochs.size();
890 solution.productStateToSolutionVectorMap = productStateToEpochModelInStateMap;
891 solution.solutions = std::move(inStateSolutions);
892 epochSolutions[currentEpoch.get()] = std::move(solution);
893}
894
895template<typename ValueType, bool SingleObjectiveMode>
897MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(Epoch const& epoch, uint64_t const& productState) {
898 auto epochSolutionIt = epochSolutions.find(epoch);
899 STORM_LOG_ASSERT(epochSolutionIt != epochSolutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
900 return getStateSolution(epochSolutionIt->second, productState);
901}
902
903template<typename ValueType, bool SingleObjectiveMode>
904typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::EpochSolution const&
905MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getEpochSolution(std::map<Epoch, EpochSolution const*> const& solutions, Epoch const& epoch) {
906 auto epochSolutionIt = solutions.find(epoch);
907 STORM_LOG_ASSERT(epochSolutionIt != solutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
908 return *epochSolutionIt->second;
909}
910
911template<typename ValueType, bool SingleObjectiveMode>
913MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(EpochSolution const& epochSolution, uint64_t const& productState) {
914 STORM_LOG_ASSERT(productState < epochSolution.productStateToSolutionVectorMap->size(), "Requested solution at an unexisting product state.");
915 STORM_LOG_ASSERT((*epochSolution.productStateToSolutionVectorMap)[productState] < epochSolution.solutions.size(),
916 "Requested solution for epoch at product state " << productState << " for which no solution was stored.");
917 return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]];
918}
919
920template<typename ValueType, bool SingleObjectiveMode>
923 STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states.");
924 return getInitialStateResult(epoch, *model.getInitialStates().begin());
925}
926
927template<typename ValueType, bool SingleObjectiveMode>
930 STORM_LOG_ASSERT(model.getInitialStates().get(initialStateIndex), "The given model state is not an initial state.");
931
932 auto result = getStateSolution(epoch, productModel->getInitialProductState(initialStateIndex, model.getInitialStates(), epochManager.getEpochClass(epoch)));
933 for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
934 if (productModel->getProb1InitialStates(objIndex) && productModel->getProb1InitialStates(objIndex)->get(initialStateIndex)) {
935 // Check whether the objective can actually hold in this epoch
936 bool objectiveHolds = true;
937 for (auto dim : objectiveDimensions[objIndex]) {
938 if (dimensions[dim].boundType == DimensionBoundType::LowerBound && !epochManager.isBottomDimension(epoch, dim)) {
939 objectiveHolds = false;
940 } else if (dimensions[dim].boundType == DimensionBoundType::UpperBound && epochManager.isBottomDimension(epoch, dim)) {
941 objectiveHolds = false;
942 }
943 STORM_LOG_ASSERT(dimensions[dim].boundType != DimensionBoundType::LowerBoundInfinity, "Unexpected bound type at this point.");
944 }
945 if (objectiveHolds) {
946 setSolutionEntry(result, objIndex, storm::utility::one<ValueType>());
947 }
948 }
949 }
950 return result;
951}
952
953template<typename ValueType, bool SingleObjectiveMode>
957
958template<typename ValueType, bool SingleObjectiveMode>
962
967} // namespace rewardbounded
968} // namespace helper
969} // namespace modelchecker
970} // namespace storm
storm::RationalNumber evaluateAsRational() const
Evaluates the expression and returns the resulting rational number.
bool containsVariables() const
Retrieves whether the expression contains a variable.
bool isLowerBoundStrict(unsigned i=0) const
storm::expressions::Expression const & getUpperBound(unsigned i=0) const
storm::expressions::Expression const & getLowerBound(unsigned i=0) const
bool isUpperBoundStrict(unsigned i=0) const
storm::expressions::Expression const & getBound() const
BoundedUntilFormula & asBoundedUntilFormula()
Definition Formula.cpp:325
virtual bool isCumulativeRewardFormula() const
Definition Formula.cpp:144
virtual bool isBoundedUntilFormula() const
Definition Formula.cpp:84
CumulativeRewardFormula & asCumulativeRewardFormula()
Definition Formula.cpp:421
ValueType computeUpperBound()
Computes an upper bound on the expected rewards.
bool epochClassZigZagOrder(Epoch const &epoch1, Epoch const &epoch2) const
Epoch getStartEpoch(bool setUnknownDimsToBottom=false)
Retrieves the desired epoch that needs to be analyzed to compute the reward bounded values.
std::conditional< SingleObjectiveMode, ValueType, std::vector< ValueType > >::type SolutionType
EpochModel< ValueType, SingleObjectiveMode > & setCurrentEpoch(Epoch const &epoch)
std::vector< Epoch > getEpochComputationOrder(Epoch const &startEpoch, bool stopAtComputedEpochs=false)
Computes a sequence of epochs that need to be analyzed to get a result at the start epoch.
ValueType getRequiredEpochModelPrecision(Epoch const &startEpoch, ValueType const &precision)
Returns the precision required for the analyzis of each epoch model in order to achieve the given ove...
boost::optional< ValueType > getUpperObjectiveBound(uint64_t objectiveIndex=0)
Returns an upper/lower bound for the objective result in every state (if this bound could be computed...
void setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat)
MultiDimensionalRewardUnfolding(storm::models::sparse::Model< ValueType > const &model, std::vector< storm::modelchecker::multiobjective::Objective< ValueType > > const &objectives)
bool isNondeterministicModel() const
Returns true if the model is a nondeterministic model.
Definition ModelBase.cpp:23
bool isOfType(storm::models::ModelType const &modelType) const
Checks whether the model is of the given type.
Definition ModelBase.cpp:19
bool containsLabel(std::string const &label) const
Checks whether a label is registered within this labeling.
Base class for all sparse models.
Definition Model.h:33
storm::storage::SparseMatrix< ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:197
virtual uint_fast64_t getNumberOfChoices() const override
Returns the number of choices ine the model.
Definition Model.cpp:172
storm::storage::SparseMatrix< ValueType > getBackwardTransitions() const
Retrieves the backward transition relation of the model, i.e.
Definition Model.cpp:152
virtual bool hasRewardModel(std::string const &rewardModelName) const override
Retrieves whether the model has a reward model with the given name.
Definition Model.cpp:207
storm::models::sparse::StateLabeling const & getStateLabeling() const
Returns the state labeling associated with this model.
Definition Model.cpp:319
virtual uint_fast64_t getNumberOfStates() const override
Returns the number of states of the model.
Definition Model.cpp:162
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
Definition Model.cpp:218
virtual std::string const & getUniqueRewardModelName() const override
Retrieves the name of the unique reward model, if there exists exactly one.
Definition Model.cpp:292
storm::storage::BitVector const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:177
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
void complement()
Negates all bits in the bit vector.
bool full() const
Retrieves whether all bits are set in this bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
void resize(uint_fast64_t newLength, bool init=false)
Resizes the bit vector to hold the given new number of bits.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
size_t size() const
Retrieves the number of bits this bit vector can store.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
bool get(uint_fast64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
This class represents the decomposition of a nondeterministic model into its maximal end components.
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
static EndComponentEliminatorReturnType transform(storm::storage::SparseMatrix< ValueType > const &originalMatrix, storm::storage::MaximalEndComponentDecomposition< ValueType > ecs, storm::storage::BitVector const &subsystemStates, storm::storage::BitVector const &addSinkRowStates, bool addSelfLoopAtSinkStates=false)
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
SFTBDDChecker::ValueType ValueType
SettingsType const & getModule()
Get module.
bool constexpr maximize(OptimizationDirection d)
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceFilter)
Performs a forward depth-first search through the underlying graph structure to identify the states t...
Definition graph.cpp:48
storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Performs a backward depth-first search trough the underlying graph structure of the given model to de...
Definition graph.cpp:322
bool hasCycle(storm::storage::SparseMatrix< T > const &transitionMatrix, boost::optional< storm::storage::BitVector > const &subsystem)
Returns true if the graph represented by the given matrix has a cycle.
Definition graph.cpp:143
storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 1 of satisfying phi until psi under all possible re...
Definition graph.cpp:997
storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under at leas...
Definition graph.cpp:689
bool checkIfECWithChoiceExists(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
Checks whether there is an End Component that.
Definition graph.cpp:182
void setVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Sets the provided values at the provided positions in the given vector.
Definition vector.h:83
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
storm::storage::BitVector filterZero(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is equal to ze...
Definition vector.h:563
ValueType floor(ValueType const &number)
bool isZero(ValueType const &a)
Definition constants.cpp:41
bool isInteger(ValueType const &number)
Definition constants.cpp:76
LabParser.cpp.
Definition cli.cpp:18
boost::optional< std::string > memoryLabel
A label that indicates the states where this dimension is still relevant (i.e., it is yet unknown whe...
Definition Dimension.h:29
DimensionBoundType boundType
The type of the bound on this dimension.
Definition Dimension.h:32
std::shared_ptr< storm::logic::Formula const > formula
The formula describing this dimension.
Definition Dimension.h:23
uint64_t objectiveIndex
The index of the associated objective.
Definition Dimension.h:26
ValueType scalingFactor
Multiplying an epoch value with this factor yields the reward/cost in the original domain.
Definition Dimension.h:35
boost::optional< ValueType > upperResultBound
Definition Objective.h:28
boost::optional< ValueType > lowerResultBound
Definition Objective.h:28
std::shared_ptr< storm::logic::Formula const > originalFormula
Definition Objective.h:17
std::shared_ptr< storm::logic::OperatorFormula const > formula
Definition Objective.h:20