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;
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) {
98 dimension.
formula = subformula.restrictToDimension(dim);
100 std::string memLabel =
"dim" + std::to_string(dimensions.size()) +
"_maybe";
102 memLabel =
"_" + memLabel;
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.");
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.");
116 bool formulaUnbounded =
117 (!subformula.hasLowerBound(dim) && !subformula.hasUpperBound(dim)) ||
118 (subformula.hasLowerBound(dim) && !subformula.isLowerBoundStrict(dim) && !subformula.getLowerBound(dim).containsVariables() &&
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));
127 if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) {
128 dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.
getTransitionMatrix().getRowCount(), 1));
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()
138 "No reward model with name '" << rewardName <<
"' found.");
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);
147 if (subformula.hasLowerBound(dim)) {
148 if (subformula.getLowerBound(dim).isVariable() &&
149 infinityBoundVariables.count(subformula.getLowerBound(dim).getBaseExpression().asVariableExpression().getVariable()) > 0) {
158 dimensions.emplace_back(std::move(dimension));
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) {
164 dimension.
formula = subformula.restrictToDimension(dim);
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.");
171 if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) {
172 dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.
getTransitionMatrix().getRowCount(), 1));
175 STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(),
"Unexpected type of time bound.");
176 std::string
const& rewardName = subformula.getTimeBoundReference(dim).getRewardName();
178 "No reward model with name '" << rewardName <<
"' found.");
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);
187 dimensions.emplace_back(std::move(dimension));
195 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
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();
205 for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim) {
206 objDimensions.
set(currDim);
208 for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim) {
210 dimensions[currDim].dependentDimensions = objDimensions;
213 dimensions[currDim].dependentDimensions.set(currDim,
true);
216 dim += objDimensionCount;
217 objectiveDimensions.push_back(std::move(objDimensions));
219 assert(dim == dimensions.size());
229 for (
auto const& dimensionSteps : dimensionWiseEpochSteps) {
230 epochManager.setDimensionOfEpoch(step, dim, dimensionSteps[choice]);
233 epochSteps.push_back(step);
237 computeMaxDimensionValues();
238 translateLowerBoundInfinityDimensions(epochSteps);
241template<
typename ValueType,
bool SingleObjectiveMode>
243 productModel = std::make_unique<ProductModel<ValueType>>(model, objectives, dimensions, objectiveDimensions, epochManager, epochSteps);
246template<
typename ValueType,
bool SingleObjectiveMode>
247void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::computeMaxDimensionValues() {
248 for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
250 bool isStrict =
false;
274 discretizedBound /= dimensions[dim].scalingFactor;
277 discretizedBound -= storm::utility::one<ValueType>();
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;
291template<
typename ValueType,
bool SingleObjectiveMode>
292void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::translateLowerBoundInfinityDimensions(std::vector<Epoch>& epochSteps) {
296 for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
300 if (!infLowerBoundedDimensions.empty()) {
305 SingleObjectiveMode, storm::exceptions::NotSupportedException,
306 "Letting lower bounds approach infinity is only supported in single objective mode.");
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.");
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 "
324 if (!upperBoundedDimensions.empty()) {
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);
337 choicesWithoutUpperBoundedStep);
339 for (
auto const& mec : mecDecomposition) {
340 for (
auto const& stateChoicesPair : mec) {
341 for (
auto const& choice : stateChoicesPair.second) {
342 nonMecChoices.set(choice,
false);
346 for (
auto choice : nonMecChoices) {
347 for (
auto dim : infLowerBoundedDimensions) {
348 epochManager.setDimensionOfEpoch(epochSteps[choice], dim, 0);
353 for (
auto dim : infLowerBoundedDimensions) {
355 dimensions[dim].maxValue = 0;
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());
369 "Tried to obtain the start epoch although no bound on dimension " << dim <<
" is known.");
370 epochManager.setBottomDimension(startEpoch, dim);
373 STORM_LOG_TRACE(
"Start epoch is " << epochManager.toString(startEpoch));
377template<
typename ValueType,
bool SingleObjectiveMode>
378std::vector<typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch>
381 std::vector<Epoch> dfsStack;
382 std::set<
Epoch, std::function<bool(
Epoch const&,
Epoch const&)>> collectedEpochs(
385 if (!stopAtComputedEpochs || epochSolutions.count(startEpoch) == 0) {
386 collectedEpochs.insert(startEpoch);
387 dfsStack.push_back(startEpoch);
389 while (!dfsStack.empty()) {
390 Epoch currentEpoch = dfsStack.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));
401 return std::vector<Epoch>(collectedEpochs.begin(), collectedEpochs.end());
404template<
typename ValueType,
bool SingleObjectiveMode>
406 STORM_LOG_DEBUG(
"Setting model for epoch " << epochManager.toString(epoch));
409 if (!currentEpoch || !epochManager.compareEpochClass(epoch, currentEpoch.get())) {
410 setCurrentEpochClass(epoch);
411 epochModel.epochMatrixChanged =
true;
414 std::cout <<
"Epoch model for epoch " << epochManager.toString(epoch) <<
" is cyclic.\n";
418 epochModel.epochMatrixChanged =
false;
421 bool containsLowerBoundedObjective =
false;
422 for (
auto const& dimension : dimensions) {
424 containsLowerBoundedObjective =
true;
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);
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);
449 for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
452 for (
auto dim : objectiveDimensions[objIndex]) {
454 productModel->getMemoryStateManager().isRelevantDimension(memoryState, dim)) {
455 rewardEarned =
false;
460 epochModel.objectiveRewardFilter[objIndex].set(reducedChoice, rewardEarned);
464 EpochSolution
const& successorEpochSolution = getEpochSolution(subSolutions, successorEpoch);
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;
473 addScaledSolution(choiceSolution, getStateSolution(successorEpochSolution, successor.getColumn()), successor.getValue());
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;
484 addScaledSolution(choiceSolution, successorSolution, successor.getValue());
488 assert(!firstSuccessor);
489 *stepSolIt = std::move(choiceSolution);
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());
502 currentEpoch = epoch;
517template<
typename ValueType,
bool SingleObjectiveMode>
519 EpochClass epochClass = epochManager.getEpochClass(epoch);
521 auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives);
525 for (
auto const& step : productModel->getSteps()) {
526 if (!epochManager.isZeroEpoch(step) && epochManager.getSuccessorEpoch(epoch, step) != epoch) {
527 stepChoices.set(choice,
true);
531 epochModel.epochMatrix = productModel->getProduct().getTransitionMatrix().filterEntries(~stepChoices);
534 for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
536 violatedLowerBoundedDimensions.set(dim);
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));
549 for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
550 if (violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) {
564 ~zeroObjRewardChoices & ~stepChoices),
565 "There is a scheduler that yields infinite reward for one objective. This case should be excluded");
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.");
576 auto backwardTransitions = epochModel.epochMatrix.transpose(
true);
580 bool requiresZeroRewardState = nonZeroRewardStates != consideredStates;
582 uint64_t zeroRewardInState = numEpochModelStates;
583 if (requiresZeroRewardState) {
584 ++numEpochModelStates;
587 if (!nonZeroRewardStates.
empty()) {
589 epochModel.epochMatrix.getSubmatrix(
true, nonZeroRewardStates, nonZeroRewardStates, convertToEquationSystem));
591 if (requiresZeroRewardState) {
592 if (convertToEquationSystem) {
594 builder.
addNextValue(zeroRewardInState, zeroRewardInState, storm::utility::zero<ValueType>());
596 epochModel.epochMatrix = builder.
build(numEpochModelStates, numEpochModelStates);
598 assert(!nonZeroRewardStates.
empty());
599 epochModel.epochMatrix = builder.
build();
601 if (convertToEquationSystem) {
602 epochModel.epochMatrix.convertToEquationSystem();
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);
612 if (requiresZeroRewardState) {
613 uint64_t zeroRewardProductState = (consideredStates & ~nonZeroRewardStates).getNextSetIndex(0);
614 assert(zeroRewardProductState < consideredStates.
size());
615 epochModelToProductChoiceMap.push_back(zeroRewardProductState);
620 zeroObjRewardChoices & ~stepChoices, consideredStates);
621 epochModel.epochMatrix = std::move(ecElimResult.matrix);
622 epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping);
623 productToEpochModelStateMapping = std::move(ecElimResult.oldToNewStateMapping);
625 STORM_LOG_THROW(
false, storm::exceptions::UnexpectedException,
"Unsupported model type.");
629 for (uint64_t choice = 0; choice < epochModel.epochMatrix.getRowCount(); ++choice) {
630 if (stepChoices.get(epochModelToProductChoiceMap[choice])) {
631 epochModel.stepChoices.set(choice,
true);
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]);
644 if (!violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) {
647 epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards));
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);
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]];
662 productStateToEpochModelInStateMap = std::make_shared<std::vector<uint64_t>
const>(std::move(toEpochModelInStatesMap));
664 epochModel.objectiveRewardFilter.clear();
665 for (
auto const& objRewards : epochModel.objectiveRewards) {
667 epochModel.objectiveRewardFilter.back().complement();
671template<
typename ValueType,
bool SingleObjectiveMode>
675 epochModel.equationSolverProblemFormat = eqSysFormat;
678template<
typename ValueType,
bool SingleObjectiveMode>
679template<bool SO, typename std::enable_if<SO, int>::type>
682 return solution * scalingFactor;
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 {
690 res.reserve(solution.size());
691 for (
auto const& sol : solution) {
692 res.push_back(sol * scalingFactor);
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;
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 {
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");
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;
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();
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;
741 for (
auto const& s : solution) {
745 stringstream <<
", ";
750 return stringstream.str();
753template<
typename ValueType,
bool SingleObjectiveMode>
755 return precision / storm::utility::convertNumber<ValueType>(epochManager.getSumOfDimensions(startEpoch) + 1);
758template<
typename ValueType,
bool SingleObjectiveMode>
760 auto& objective = this->objectives[objectiveIndex];
762 if (objective.
formula->isProbabilityOperatorFormula()) {
764 }
else if (objective.
formula->isRewardOperatorFormula()) {
765 auto const& rewModel = this->model.
getRewardModel(objective.
formula->asRewardOperatorFormula().getRewardModelName());
767 if (objective.
formula->getSubformula().isCumulativeRewardFormula()) {
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()) {
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) {
785 ValueType rewardPerCost = *rewIt / *costIt;
786 largestRewardPerCost = std::max(largestRewardPerCost, rewardPerCost);
790 resBound = largestRewardPerCost * rewardBound;
794 resBound = (*std::max_element(actionRewards.begin(), actionRewards.end())) * rewardBound;
811 zeroRewardChoices, ~allStates);
812 allStates.
resize(ecElimRes.matrix.getRowGroupCount());
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];
820 bool isOutChoice =
false;
821 uint64_t originalModelChoice = ecElimRes.newToOldRowMapping[choice];
823 if (!expRewGreater0EStates.get(entry.getColumn())) {
825 outStates.
set(state,
true);
826 rew0StateProbs.push_back(storm::utility::one<ValueType>() - ecElimRes.matrix.getRowSum(choice));
832 rew0StateProbs.push_back(storm::utility::zero<ValueType>());
838 allStates, outStates)
840 std::vector<ValueType> rewards;
841 rewards.reserve(ecElimRes.matrix.getRowCount());
842 for (
auto row : ecElimRes.newToOldRowMapping) {
843 rewards.push_back(actionRewards[row]);
855template<
typename ValueType,
bool SingleObjectiveMode>
857 auto& objective = this->objectives[objectiveIndex];
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.");
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));
874 predecessorEpochs.erase(currentEpoch.get());
875 successorEpochs.erase(currentEpoch.get());
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);
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);
895template<
typename ValueType,
bool SingleObjectiveMode>
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);
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;
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]];
920template<
typename ValueType,
bool SingleObjectiveMode>
927template<
typename ValueType,
bool SingleObjectiveMode>
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)) {
936 bool objectiveHolds =
true;
937 for (
auto dim : objectiveDimensions[objIndex]) {
939 objectiveHolds =
false;
941 objectiveHolds =
false;
945 if (objectiveHolds) {
946 setSolutionEntry(result, objIndex, storm::utility::one<ValueType>());
953template<
typename ValueType,
bool SingleObjectiveMode>
958template<
typename ValueType,
bool SingleObjectiveMode>
960 return dimensions.at(dim);