29namespace modelchecker {
30namespace multiobjective {
32template<
class SparseModelType>
39template<
class SparseModelType>
44 "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
46 "There might be infinite reward for some scheduler. Multi-objective model checking restricts to schedulers that yield finite reward "
47 "for all objectives. Be aware that solutions yielding infinite reward are discarded.");
48 STORM_LOG_THROW(rewardAnalysis.totalRewardLessInfinityEStates, storm::exceptions::UnexpectedException,
49 "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
51 "At least one objective was not reduced to an expected (long run, total or cumulative) reward objective during preprocessing. This is not "
52 "supported by the considered weight vector checker.");
54 "The model has multiple initial states.");
60 rewardAnalysis.totalRewardLessInfinityEStates.get(), rewardAnalysis.totalRewardLessInfinityEStates.get());
61 std::set<std::string> relevantRewardModels;
62 for (
auto const& obj : this->objectives) {
63 obj.formula->gatherReferencedRewardModels(relevantRewardModels);
68 std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices);
71 initializeModelTypeSpecificData(*mergerResult.model);
74 transitionMatrix = std::move(mergerResult.model->getTransitionMatrix());
75 initialState = *mergerResult.model->getInitialStates().begin();
76 totalReward0EStates = rewardAnalysis.totalReward0EStates % maybeStates;
77 if (mergerResult.targetState) {
79 totalReward0EStates.
resize(totalReward0EStates.size() + 1,
true);
83 targetStateAsVector.
set(*mergerResult.targetState,
true);
84 ecChoicesHint = transitionMatrix.getRowFilter(
87 ecChoicesHint.set(transitionMatrix.getRowGroupIndices()[*mergerResult.targetState],
true);
96 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
97 auto const& formula = *this->objectives[objIndex].formula;
98 if (formula.getSubformula().isTotalRewardFormula()) {
99 objectivesWithNoUpperTimeBound.set(objIndex,
true);
102 if (formula.getSubformula().isLongRunAverageRewardFormula()) {
103 lraObjectives.set(objIndex,
true);
104 objectivesWithNoUpperTimeBound.set(objIndex,
true);
109 if (!lraObjectives.empty()) {
110 lraMecDecomposition = LraMecDecomposition();
112 transitionMatrix, transitionMatrix.transpose(
true),
storm::storage::BitVector(transitionMatrix.getRowGroupCount(),
true),
113 actionsWithoutRewardInUnboundedPhase);
114 lraMecDecomposition->auxMecValues.resize(lraMecDecomposition->mecs.size());
118 checkHasBeenCalled =
false;
119 objectiveResults.resize(this->objectives.size());
120 offsetsToUnderApproximation.resize(this->objectives.size(), storm::utility::zero<ValueType>());
121 offsetsToOverApproximation.resize(this->objectives.size(), storm::utility::zero<ValueType>());
122 optimalChoices.resize(transitionMatrix.getRowGroupCount(), 0);
127 STORM_PRINT_AND_LOG(
"Final preprocessed model has " << transitionMatrix.getRowGroupCount() <<
" states.\n");
128 STORM_PRINT_AND_LOG(
"Final preprocessed model has " << transitionMatrix.getRowCount() <<
" actions.\n");
129 if (lraMecDecomposition) {
130 STORM_PRINT_AND_LOG(
"Found " << lraMecDecomposition->mecs.size() <<
" end components that are relevant for LRA-analysis.\n");
131 uint64_t numLraMecStates = 0;
132 for (
auto const& mec : this->lraMecDecomposition->mecs) {
133 numLraMecStates += mec.size();
141template<
class SparseModelType>
143 checkHasBeenCalled =
true;
148 std::vector<ValueType> weightedRewardVector(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
149 if (!lraObjectives.empty()) {
150 boost::optional<std::vector<ValueType>> weightedStateRewardVector;
151 for (
auto objIndex : lraObjectives) {
153 storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
155 if (!stateRewards.empty() && !stateRewards[objIndex].empty()) {
156 if (!weightedStateRewardVector) {
157 weightedStateRewardVector = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
162 infiniteHorizonWeightedPhase(env, weightedRewardVector, weightedStateRewardVector);
164 weightedRewardVector.assign(weightedRewardVector.size(), storm::utility::zero<ValueType>());
168 auto totalRewardObjectives = objectivesWithNoUpperTimeBound & ~lraObjectives;
169 for (
auto objIndex : totalRewardObjectives) {
176 unboundedWeightedPhase(env, weightedRewardVector, weightVector);
178 unboundedIndividualPhase(env, weightVector);
180 for (
auto const& obj : this->objectives) {
181 if (!obj.formula->getSubformula().isTotalRewardFormula() && !obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
182 boundedPhase(env, weightVector, weightedRewardVector);
186 STORM_LOG_INFO(
"Weight vector check done. Lower bounds for results in initial state: "
193 STORM_LOG_THROW(resultingWeightedPrecision <= this->getWeightedPrecision(), storm::exceptions::UnexpectedException,
194 "The desired precision was not reached");
197template<
class SparseModelType>
198std::vector<typename StandardPcaaWeightVectorChecker<SparseModelType>::ValueType>
200 STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException,
"Tried to retrieve results but check(..) has not been called before.");
201 std::vector<ValueType> res;
202 res.reserve(this->objectives.size());
203 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
204 res.push_back(this->objectiveResults[objIndex][initialState] + this->offsetsToUnderApproximation[objIndex]);
209template<
class SparseModelType>
210std::vector<typename StandardPcaaWeightVectorChecker<SparseModelType>::ValueType>
212 STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException,
"Tried to retrieve results but check(..) has not been called before.");
213 std::vector<ValueType> res;
214 res.reserve(this->objectives.size());
215 for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
216 res.push_back(this->objectiveResults[objIndex][initialState] + this->offsetsToOverApproximation[objIndex]);
221template<
class SparseModelType>
224 STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException,
225 "Tried to retrieve results but check(..) has not been called before.");
226 for (
auto const& obj : this->objectives) {
227 STORM_LOG_THROW(obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isLongRunAverageRewardFormula(),
228 storm::exceptions::NotImplementedException,
"Scheduler retrival is only implemented for objectives without time-bound.");
232 uint_fast64_t state = 0;
233 for (
auto const& choice : optimalChoices) {
240template<
typename ValueType>
244 std::vector<uint64_t> stack;
246 stack.insert(stack.end(), processedStates.
begin(), processedStates.
end());
247 uint64_t currentState = 0;
249 while (!stack.empty()) {
250 currentState = stack.back();
253 for (
auto const& predecessorEntry : backwardTransitions.
getRow(currentState)) {
254 auto predecessor = predecessorEntry.getColumn();
255 if (consideredStates.
get(predecessor) && !processedStates.
get(predecessor)) {
259 uint64_t row = allowedChoices ? allowedChoices->getNextSetIndex(groupStart) : groupStart;
260 for (; row < groupEnd; row = allowedChoices ? allowedChoices->getNextSetIndex(row + 1) : row + 1) {
261 bool hasSuccessorInProcessedStates =
false;
262 for (
auto const& successorOfPredecessor : transitionMatrix.
getRow(row)) {
263 if (processedStates.
get(successorOfPredecessor.getColumn())) {
264 hasSuccessorInProcessedStates =
true;
268 if (hasSuccessorInProcessedStates) {
269 choices[predecessor] = row - groupStart;
270 processedStates.
set(predecessor,
true);
271 stack.push_back(predecessor);
276 "Unable to find choice at a predecessor of a processed state that leads to a processed state.");
283template<
typename ValueType>
287 for (
auto state : consideredStates) {
290 bool choiceFound =
false;
293 for (
auto const& element : transitionMatrix.
getRow(row)) {
294 if (statesToAvoid.
get(element.getColumn())) {
300 choices[state] = row - groupStart;
308template<
typename ValueType>
312 auto backwardsTransitions = matrix.
transpose(
true);
314 for (uint64_t state = 0; state < result.size(); ++state) {
315 if (rowsWithSumLessOne.
getNextSetIndex(groups[state]) < groups[state + 1]) {
316 result[state] = rowsWithSumLessOne.
getNextSetIndex(groups[state]) - groups[state];
317 processedStates.
set(state,
true);
330template<
typename ValueType>
334 auto badStates = transitionMatrix.
getRowGroupFilter(finitelyOftenChoices,
true) & ~safeStates;
338 transitionMatrix, transitionMatrix.
getRowGroupIndices(), backwardTransitions, ~safeStates, badStates,
false, 0, ~finitelyOftenChoices);
341 auto avoidBadStates = ~reachBadWithProbGreater0AStates & ~safeStates;
342 computeSchedulerProb0(transitionMatrix, backwardTransitions, avoidBadStates, reachBadWithProbGreater0AStates, ~finitelyOftenChoices, choices);
347 computeSchedulerProb1(transitionMatrix, backwardTransitions, reachBadWithProbGreater0AStates, avoidBadStates | safeStates, choices);
350template<
class SparseModelType>
352 std::vector<ValueType>
const& weightedActionRewardVector,
353 boost::optional<std::vector<ValueType>>
const& weightedStateRewardVector) {
355 STORM_LOG_ASSERT(lraMecDecomposition,
"Mec decomposition for lra computations not initialized.");
360 for (uint64_t mecIndex = 0; mecIndex < lraMecDecomposition->mecs.size(); ++mecIndex) {
361 auto const& mec = lraMecDecomposition->mecs[mecIndex];
362 auto actionValueGetter = [&weightedActionRewardVector](uint64_t
const& a) {
return weightedActionRewardVector[a]; };
364 if (weightedStateRewardVector) {
365 stateValueGetter = [&weightedStateRewardVector](uint64_t
const& s) {
return weightedStateRewardVector.get()[s]; };
367 stateValueGetter = [](uint64_t
const&) {
return storm::utility::zero<ValueType>(); };
369 lraMecDecomposition->auxMecValues[mecIndex] = helper.
computeLraForComponent(env, stateValueGetter, actionValueGetter, mec);
375template<
class SparseModelType>
377 std::vector<ValueType>
const& weightVector) {
379 if (this->objectivesWithNoUpperTimeBound.empty() ||
382 this->weightedResult.assign(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
384 if (this->lraMecDecomposition) {
385 for (
auto const& mec : this->lraMecDecomposition->mecs) {
386 for (
auto const& sc : mec) {
387 statesInLraMec.
set(sc.first,
true);
393 this->optimalChoices);
397 updateEcQuotient(weightedRewardVector);
401 std::map<uint64_t, uint64_t> ecqStateToOptimalMecMap;
402 if (!lraObjectives.empty()) {
407 for (uint64_t mecIndex = 0; mecIndex < lraMecDecomposition->mecs.size(); ++mecIndex) {
408 auto const& mec = lraMecDecomposition->mecs[mecIndex];
409 auto const& mecValue = lraMecDecomposition->auxMecValues[mecIndex];
410 uint64_t ecqState = ecQuotient->originalToEcqStateMapping[mec.begin()->first];
411 if (ecqState >= ecQuotient->matrix.getRowGroupCount()) {
416 uint64_t ecqChoice = ecQuotient->ecqStayInEcChoices.getNextSetIndex(ecQuotient->matrix.getRowGroupIndices()[ecqState]);
417 STORM_LOG_ASSERT(ecqChoice < ecQuotient->matrix.getRowGroupIndices()[ecqState + 1],
418 "Unable to find choice that represents staying inside the (eliminated) ec.");
419 auto& ecqChoiceValue = ecQuotient->auxChoiceValues[ecqChoice];
420 auto insertionRes = ecqStateToOptimalMecMap.emplace(ecqState, mecIndex);
421 if (insertionRes.second) {
424 "Expected a total reward of zero for choices that represent staying in an EC for ever.");
425 ecqChoiceValue = mecValue;
427 if (mecValue > ecqChoiceValue) {
428 ecqChoiceValue = mecValue;
429 insertionRes.first->second = mecIndex;
436 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.
create(env, ecQuotient->matrix);
437 solver->setTrackScheduler(
true);
438 solver->setHasUniqueSolution(
true);
439 solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
440 auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize);
441 setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix,
442 ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues);
443 if (solver->hasLowerBound()) {
444 req.clearLowerBounds();
446 if (solver->hasUpperBound()) {
447 req.clearUpperBounds();
449 if (req.validInitialScheduler()) {
451 req.clearValidInitialScheduler();
453 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
454 "Solver requirements " + req.getEnabledRequirementsAsString() +
" not checked.");
455 solver->setRequirementsChecked(
true);
458 std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero<ValueType>());
460 solver->solveEquations(env, ecQuotient->auxStateValues, ecQuotient->auxChoiceValues);
461 this->weightedResult = std::vector<ValueType>(transitionMatrix.getRowGroupCount());
463 transformEcqSolutionToOriginalModel(ecQuotient->auxStateValues, solver->getSchedulerChoices(), ecqStateToOptimalMecMap, this->weightedResult,
464 this->optimalChoices);
467template<
class SparseModelType>
469 if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 &&
storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) {
470 uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin();
471 objectiveResults[objIndex] = weightedResult;
475 for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) {
476 if (objIndex != objIndex2) {
477 objectiveResults[objIndex2] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
483 std::vector<ValueType> deterministicStateRewards(deterministicMatrix.
getRowCount());
486 auto infiniteHorizonHelper = createDetInfiniteHorizonHelper(deterministicMatrix);
487 infiniteHorizonHelper.provideBackwardTransitions(deterministicBackwardTransitions);
491 std::vector<ValueType> weightedSumOfUncheckedObjectives = weightedResult;
495 auto const& obj = this->objectives[objIndex];
496 if (objectivesWithNoUpperTimeBound.get(objIndex)) {
497 offsetsToUnderApproximation[objIndex] = storm::utility::zero<ValueType>();
498 offsetsToOverApproximation[objIndex] = storm::utility::zero<ValueType>();
499 if (lraObjectives.get(objIndex)) {
500 auto actionValueGetter = [&](uint64_t
const& a) {
501 return actionRewards[objIndex][transitionMatrix.getRowGroupIndices()[a] + this->optimalChoices[a]];
504 if (stateRewards.empty() || stateRewards[objIndex].empty()) {
505 stateValueGetter = [](uint64_t
const&) {
return storm::utility::zero<ValueType>(); };
507 stateValueGetter = [&](uint64_t
const& s) {
return stateRewards[objIndex][s]; };
512 actionRewards[objIndex]);
520 objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
521 ValueType scalingFactor = storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives;
523 scalingFactor *= -storm::utility::one<ValueType>();
529 objectiveResults[objIndex].resize(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
531 if (!maybeStates.
empty()) {
532 bool needEquationSystem =
535 deterministicMatrix.
getSubmatrix(
true, maybeStates, maybeStates, needEquationSystem);
536 if (needEquationSystem) {
547 std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.
create(env, submatrix);
548 auto req = solver->getRequirements(env);
549 solver->clearBounds();
552 this->setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b);
553 if (solver->hasLowerBound()) {
554 req.clearLowerBounds();
556 if (solver->hasUpperBound()) {
557 req.clearUpperBounds();
559 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
560 "Solver requirements " + req.getEnabledRequirementsAsString() +
" not checked.");
561 solver->solveEquations(env, x, b);
563 storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], maybeStates, x);
565 storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], ~maybeStates, storm::utility::zero<ValueType>());
570 sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex];
573 objectiveResults[objIndex] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
579template<
class SparseModelType>
584 if (lraMecDecomposition) {
585 for (uint64_t mecIndex = 0; mecIndex < lraMecDecomposition->mecs.size(); ++mecIndex) {
588 auto const& mec = lraMecDecomposition->mecs[mecIndex];
589 for (
auto const& stateChoices : mec) {
590 for (
auto const& choice : stateChoices.second) {
591 zeroLraRewardChoices.
set(choice,
false);
598 if (!ecQuotient || ecQuotient->origReward0Choices != newReward0Choices) {
600 auto nonZeroRewardStates = transitionMatrix.getRowGroupFilter(newReward0Choices,
true);
603 transitionMatrix.transpose(
true),
storm::storage::BitVector(transitionMatrix.getRowGroupCount(),
true), nonZeroRewardStates);
608 ecChoicesHint & newTotalReward0Choices, totalReward0EStates);
611 for (uint64_t row = 0; row < rowsWithSumLessOne.
size(); ++row) {
612 if (ecElimResult.matrix.getRow(row).getNumberOfEntries() == 0) {
613 rowsWithSumLessOne.
set(row,
true);
615 for (
auto const& entry : transitionMatrix.getRow(ecElimResult.newToOldRowMapping[row])) {
616 if (!subsystemStates.
get(entry.getColumn())) {
617 rowsWithSumLessOne.
set(row,
true);
625 ecQuotient->matrix = std::move(ecElimResult.matrix);
626 ecQuotient->ecqToOriginalChoiceMapping = std::move(ecElimResult.newToOldRowMapping);
627 ecQuotient->originalToEcqStateMapping = std::move(ecElimResult.oldToNewStateMapping);
628 ecQuotient->ecqToOriginalStateMapping.resize(ecQuotient->matrix.getRowGroupCount());
629 for (uint64_t state = 0; state < ecQuotient->originalToEcqStateMapping.size(); ++state) {
630 uint64_t ecqState = ecQuotient->originalToEcqStateMapping[state];
631 if (ecqState < ecQuotient->matrix.getRowGroupCount()) {
632 ecQuotient->ecqToOriginalStateMapping[ecqState].insert(state);
635 ecQuotient->ecqStayInEcChoices = std::move(ecElimResult.sinkRows);
636 ecQuotient->origReward0Choices = std::move(newReward0Choices);
637 ecQuotient->origTotalReward0Choices = std::move(newTotalReward0Choices);
638 ecQuotient->rowsWithSumLessOne = std::move(rowsWithSumLessOne);
639 ecQuotient->auxStateValues.resize(ecQuotient->matrix.getRowGroupCount());
640 ecQuotient->auxChoiceValues.resize(ecQuotient->matrix.getRowCount());
644template<
class SparseModelType>
646 bool requiresUpper, uint64_t objIndex,
649 std::vector<ValueType>
const& rewards)
const {
651 if (this->objectives[objIndex].lowerResultBound) {
652 solver.
setLowerBound(this->objectives[objIndex].lowerResultBound.get());
654 if (this->objectives[objIndex].upperResultBound) {
655 solver.
setUpperBound(this->objectives[objIndex].upperResultBound.get());
659 computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
663template<
class SparseModelType>
665 bool requiresUpper, std::vector<ValueType>
const& weightVector,
669 std::vector<ValueType>
const& rewards)
const {
671 boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(
true, weightVector, objectiveFilter & ~lraObjectives);
673 if (!lraObjectives.empty()) {
674 auto min = std::min_element(lraMecDecomposition->auxMecValues.begin(), lraMecDecomposition->auxMecValues.end());
675 if (min != lraMecDecomposition->auxMecValues.end()) {
676 lowerBound.get() += *min;
681 boost::optional<ValueType> upperBound = this->computeWeightedResultBound(
false, weightVector, objectiveFilter);
683 if (!lraObjectives.empty()) {
684 auto max = std::max_element(lraMecDecomposition->auxMecValues.begin(), lraMecDecomposition->auxMecValues.end());
685 if (max != lraMecDecomposition->auxMecValues.end()) {
686 upperBound.get() += *max;
693 computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
697template<
class SparseModelType>
702 std::vector<ValueType>
const& rewards)
const {
704 std::vector<ValueType> oneStepTargetProbs(transitions.
getRowCount(), storm::utility::zero<ValueType>());
705 for (
auto row : rowsWithSumLessOne) {
706 oneStepTargetProbs[row] = storm::utility::one<ValueType>() - transitions.
getRowSum(row);
711 std::vector<ValueType> negativeRewards;
712 negativeRewards.reserve(transitions.
getRowCount());
714 for (
auto const& rew : rewards) {
715 if (rew < storm::utility::zero<ValueType>()) {
716 negativeRewards.resize(row, storm::utility::zero<ValueType>());
717 negativeRewards.push_back(-rew);
721 if (!negativeRewards.empty()) {
722 negativeRewards.resize(row, storm::utility::zero<ValueType>());
723 std::vector<ValueType> lowerBounds =
735 std::vector<ValueType> positiveRewards;
736 positiveRewards.reserve(transitions.
getRowCount());
738 for (
auto const& rew : rewards) {
739 if (rew > storm::utility::zero<ValueType>()) {
740 positiveRewards.resize(row, storm::utility::zero<ValueType>());
741 positiveRewards.push_back(rew);
745 if (!positiveRewards.empty()) {
746 positiveRewards.resize(row, storm::utility::zero<ValueType>());
755template<
class SparseModelType>
757 std::vector<uint_fast64_t>
const& ecqOptimalChoices,
758 std::map<uint64_t, uint64_t>
const& ecqStateToOptimalMecMap,
759 std::vector<ValueType>& originalSolution,
760 std::vector<uint_fast64_t>& originalOptimalChoices)
const {
761 auto backwardsTransitions = transitionMatrix.transpose(
true);
772 for (uint64_t ecqState = 0; ecqState < ecqSolution.size(); ++ecqState) {
773 uint64_t ecqChoice = ecQuotient->matrix.getRowGroupIndices()[ecqState] + ecqOptimalChoices[ecqState];
774 uint_fast64_t origChoice = ecQuotient->ecqToOriginalChoiceMapping[ecqChoice];
775 auto const& origStates = ecQuotient->ecqToOriginalStateMapping[ecqState];
776 STORM_LOG_ASSERT(!origStates.empty(),
"Unexpected empty set of original states.");
777 if (ecQuotient->ecqStayInEcChoices.get(ecqChoice)) {
780 if (!ecqStateToOptimalMecMap.empty()) {
783 STORM_LOG_ASSERT(ecqStateToOptimalMecMap.count(ecqState) > 0,
"No Lra Mec associated to given eliminated EC");
784 auto const& lraMec = lraMecDecomposition->mecs[ecqStateToOptimalMecMap.at(ecqState)];
785 if (lraMec.size() == origStates.size()) {
787 for (
auto const& state : origStates) {
788 STORM_LOG_ASSERT(lraMec.containsState(state),
"Expected state to be contained in the lra mec.");
790 unprocessedStates.
set(state,
false);
791 originalSolution[state] = ecqSolution[ecqState];
795 STORM_LOG_ASSERT(lraMec.size() < origStates.size(),
"Lra Mec (" << lraMec.size()
796 <<
" states) should be a proper subset of the eliminated ec ("
797 << origStates.size() <<
" states).");
798 for (
auto const& state : origStates) {
799 if (lraMec.containsState(state)) {
800 ecStatesToReach.
set(state,
true);
803 ecStatesToProcess.
set(state,
true);
805 unprocessedStates.
set(state,
false);
806 originalSolution[state] = ecqSolution[ecqState];
808 computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices,
809 &ecQuotient->origTotalReward0Choices);
811 ecStatesToProcess.
clear();
812 ecStatesToReach.
clear();
818 bool needSchedulerComputation =
false;
820 "Solution for state that stays inside EC must be zero. Got " << ecqSolution[ecqState] <<
" instead.");
821 for (
auto const& state : origStates) {
822 originalSolution[state] = storm::utility::zero<ValueType>();
823 ecStatesToProcess.
set(state,
true);
825 auto validChoices = transitionMatrix.getRowFilter(ecStatesToProcess, ecStatesToProcess);
826 auto valid0RewardChoices = validChoices & actionsWithoutRewardInUnboundedPhase;
827 for (
auto const& state : origStates) {
828 auto groupStart = transitionMatrix.getRowGroupIndices()[state];
829 auto groupEnd = transitionMatrix.getRowGroupIndices()[state + 1];
830 auto nextValidChoice = valid0RewardChoices.getNextSetIndex(groupStart);
831 if (nextValidChoice < groupEnd) {
832 originalOptimalChoices[state] = nextValidChoice - groupStart;
835 ecStatesToAvoid.
set(state,
true);
836 needSchedulerComputation =
true;
839 if (needSchedulerComputation) {
841 auto ecStatesThatCanAvoid =
843 ecStatesToProcess, ecStatesToAvoid,
false, 0, valid0RewardChoices);
844 ecStatesThatCanAvoid.complement();
846 computeSchedulerProb0(transitionMatrix, backwardsTransitions, ecStatesThatCanAvoid, ecStatesToAvoid, valid0RewardChoices,
847 originalOptimalChoices);
849 computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess & ~ecStatesToAvoid, ecStatesToAvoid, originalOptimalChoices,
852 ecStatesToAvoid.
clear();
853 ecStatesToProcess.
clear();
859 if (origStates.size() > 1) {
860 for (
auto const& state : origStates) {
862 auto groupStart = transitionMatrix.getRowGroupIndices()[state];
863 auto groupEnd = transitionMatrix.getRowGroupIndices()[state + 1];
864 if (origChoice >= groupStart && origChoice < groupEnd) {
865 originalOptimalChoices[state] = origChoice - groupStart;
866 ecStatesToReach.
set(state,
true);
868 STORM_LOG_ASSERT(origStates.size() > 1,
"Multiple original states expected.");
869 ecStatesToProcess.
set(state,
true);
871 unprocessedStates.
set(state,
false);
872 originalSolution[state] = ecqSolution[ecqState];
874 auto validChoices = transitionMatrix.getRowFilter(ecStatesToProcess, ecStatesToProcess | ecStatesToReach);
875 computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices, &validChoices);
877 ecStatesToProcess.
clear();
878 ecStatesToReach.
clear();
881 auto state = *origStates.begin();
882 auto groupStart = transitionMatrix.getRowGroupIndices()[state];
884 origChoice >= groupStart && origChoice < transitionMatrix.getRowGroupIndices()[state + 1],
885 "Invalid choice: " << originalOptimalChoices[state] <<
" at a state with " << transitionMatrix.getRowGroupSize(state) <<
" choices.");
886 originalOptimalChoices[state] = origChoice - groupStart;
887 originalSolution[state] = ecqSolution[ecqState];
888 unprocessedStates.
set(state,
false);
897 if (this->lraMecDecomposition) {
899 for (
auto const& mec : this->lraMecDecomposition->mecs) {
900 for (
auto const& sc : mec) {
901 if (unprocessedStates.
get(sc.first)) {
902 ecStatesToReach.
set(sc.first,
true);
907 ecStatesToReach = unprocessedStates & totalReward0EStates;
909 computeSchedulerProb0(transitionMatrix, backwardsTransitions, ecStatesToReach, ~unprocessedStates | ~totalReward0EStates,
910 actionsWithoutRewardInUnboundedPhase, originalOptimalChoices);
912 unprocessedStates &= ~ecStatesToReach;
914 computeSchedulerProb1(transitionMatrix, backwardsTransitions, unprocessedStates, ecStatesToReach, originalOptimalChoices);
919#ifdef STORM_HAVE_CARL
ValueType computeUpperBound()
Computes an upper bound on the expected rewards.
std::vector< ValueType > computeUpperBounds()
Computes upper bounds on the expected rewards.
void setProduceScheduler(bool value)
Sets whether an optimal scheduler shall be constructed during the computation.
void setOptimizationDirection(storm::solver::OptimizationDirection const &direction)
Sets the optimization direction, i.e., whether we want to minimize or maximize the value for each sta...
void provideLongRunComponentDecomposition(storm::storage::Decomposition< LongRunComponentType > const &decomposition)
Provides the decomposition into long run components (BSCCs/MECs) that can be used during the computat...
std::vector< ValueType > computeLongRunAverageValues(Environment const &env, std::vector< ValueType > const *stateValues=nullptr, std::vector< ValueType > const *actionValues=nullptr)
Computes the long run average value given the provided state and action-based rewards.
Helper class for model checking queries that depend on the long run behavior of the (nondeterministic...
SparseInfiniteHorizonHelper< ValueType, true >::ValueGetter ValueGetter
Function mapping from indices to values.
std::vector< uint64_t > const & getProducedOptimalChoices() const
virtual ValueType computeLraForComponent(Environment const &env, ValueGetter const &stateValuesGetter, ValueGetter const &actionValuesGetter, storm::storage::MaximalEndComponent const &component) override
Helper Class that takes a weight vector and ...
Helper Class that takes preprocessed Pcaa data and a weight vector and ...
void unboundedWeightedPhase(Environment const &env, std::vector< ValueType > const &weightedRewardVector, std::vector< ValueType > const &weightVector)
Determines the scheduler that optimizes the weighted reward vector of the unbounded objectives.
virtual std::vector< ValueType > getOverApproximationOfInitialStateResults() const override
void computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver< ValueType > &solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix< ValueType > const &transitions, storm::storage::BitVector const &rowsWithSumLessOne, std::vector< ValueType > const &rewards) const
StandardPcaaWeightVectorChecker(preprocessing::SparseMultiObjectivePreprocessorResult< SparseModelType > const &preprocessorResult)
SparseModelType::ValueType ValueType
virtual std::vector< ValueType > getUnderApproximationOfInitialStateResults() const override
Retrieves the results of the individual objectives at the initial state of the given model.
void transformEcqSolutionToOriginalModel(std::vector< ValueType > const &ecqSolution, std::vector< uint_fast64_t > const &ecqOptimalChoices, std::map< uint64_t, uint64_t > const &ecqStateToOptimalMecMap, std::vector< ValueType > &originalSolution, std::vector< uint_fast64_t > &originalOptimalChoices) const
Transforms the results of a min-max-solver that considers a reduced model (without end components) to...
void infiniteHorizonWeightedPhase(Environment const &env, std::vector< ValueType > const &weightedActionRewardVector, boost::optional< std::vector< ValueType > > const &weightedStateRewardVector)
virtual storm::storage::Scheduler< ValueType > computeScheduler() const override
Retrieves a scheduler that induces the current values Note that check(..) has to be called before ret...
virtual void check(Environment const &env, std::vector< ValueType > const &weightVector) override
void updateEcQuotient(std::vector< ValueType > const &weightedRewardVector)
void initialize(preprocessing::SparseMultiObjectivePreprocessorResult< SparseModelType > const &preprocessorResult)
void unboundedIndividualPhase(Environment const &env, std::vector< ValueType > const &weightVector)
Computes the values of the objectives that do not have a stepBound w.r.t.
void setBoundsToSolver(storm::solver::AbstractEquationSolver< ValueType > &solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix< ValueType > const &transitions, storm::storage::BitVector const &rowsWithSumLessOne, std::vector< ValueType > const &rewards) const
static ReturnType analyze(storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessorResult< SparseModelType > const &preprocessorResult)
Analyzes the reward objectives of the multi objective query.
void setUpperBound(ValueType const &value)
Sets an upper bound for the solution that can potentially be used by the solver.
bool hasUpperBound(BoundType const &type=BoundType::Any) const
Retrieves whether this solver has an upper bound.
bool hasLowerBound(BoundType const &type=BoundType::Any) const
Retrieves whether this solver has a lower bound.
void setLowerBound(ValueType const &value)
Sets a lower bound for the solution that can potentially be used by the solver.
void setLowerBounds(std::vector< ValueType > const &values)
Sets lower bounds for the solution that can potentially be used by the solver.
virtual std::unique_ptr< LinearEquationSolver< ValueType > > create(Environment const &env) const override
Creates an equation solver with the current settings, but without a matrix.
virtual std::unique_ptr< MinMaxLinearEquationSolver< ValueType, SolutionType > > create(Environment const &env) const override
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const &env) const
Retrieves the problem format that the solver expects if it was created with the current settings.
A bit vector that is internally represented as a vector of 64-bit values.
void complement()
Negates all bits in the bit vector.
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
void clear()
Removes all set bits from the bit vector.
bool isSubsetOf(BitVector const &other) const
Checks whether all bits that are set in the current bit vector are also set in the given 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.
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.
This class defines which action is chosen in a particular state of a non-deterministic model.
void setChoice(SchedulerChoice< ValueType > const &choice, uint_fast64_t modelState, uint_fast64_t memoryState=0)
Sets the choice defined by the scheduler for the given state.
A class that holds a possibly non-square matrix in the compressed row storage format.
void convertToEquationSystem()
Transforms the matrix into an equation system.
const_rows getRow(index_type row) const
Returns an object representing the given row.
SparseMatrix selectRowsFromRowGroups(std::vector< index_type > const &rowGroupToRowIndexMapping, bool insertDiagonalEntries=true) const
Selects exactly one row from each row group of this matrix and returns the resulting matrix.
SparseMatrix getSubmatrix(bool useGroups, storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint, bool insertDiagonalEntries=false, storm::storage::BitVector const &makeZeroColumns=storm::storage::BitVector()) const
Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not set to ...
value_type getRowSum(index_type row) const
Computes the sum of the entries in a given row.
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
storm::storage::BitVector getRowGroupFilter(storm::storage::BitVector const &rowConstraint, bool setIfForAllRowsInGroup) const
Returns the indices of all row groups selected by the row constraints.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
storm::storage::SparseMatrix< value_type > transpose(bool joinGroups=false, bool keepZeros=false) const
Transposes the matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
storm::storage::BitVector getRowFilter(storm::storage::BitVector const &groupConstraint) const
Returns a bitvector representing the set of rows, with all indices set that correspond to one of the ...
#define STORM_LOG_INFO(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
#define STORM_PRINT_AND_LOG(message)
std::vector< uint64_t > computeValidInitialScheduler(storm::storage::SparseMatrix< ValueType > const &matrix, storm::storage::BitVector const &rowsWithSumLessOne)
void computeSchedulerFinitelyOften(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &finitelyOftenChoices, storm::storage::BitVector safeStates, std::vector< uint64_t > &choices)
Computes a scheduler taking the choices from the given set only finitely often.
void computeSchedulerProb1(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &consideredStates, storm::storage::BitVector const &statesToReach, std::vector< uint64_t > &choices, storm::storage::BitVector const *allowedChoices=nullptr)
void computeSchedulerProb0(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &consideredStates, storm::storage::BitVector const &statesToAvoid, storm::storage::BitVector const &allowedChoices, std::vector< uint64_t > &choices)
SettingsType const & getModule()
Get module.
bool constexpr minimize(OptimizationDirection d)
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...
storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under any pos...
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...
storm::storage::BitVector performProb0E(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 0 of satisfying phi until psi under at least one po...
T dotProduct(std::vector< T > const &firstOperand, std::vector< T > const &secondOperand)
Computes the dot product (aka scalar product) and returns the result.
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.
void selectVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Selects the elements from a vector at the specified positions and writes them consecutively into anot...
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...
std::string toString(std::vector< ValueType > const &vector)
Output vector as string.
void clip(std::vector< ValueType > &x, boost::optional< ValueType > const &lowerBound, boost::optional< ValueType > const &upperBound)
Takes the input vector and ensures that all entries conform to the bounds.
VT sum_if(std::vector< VT > const &values, storm::storage::BitVector const &filter)
Sum the entries from values that are set to one in the filter vector.
std::vector< uint_fast64_t > getSortedIndices(std::vector< T > const &v)
Returns a list of indices such that the first index refers to the highest entry of the given vector,...
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...
void scaleVectorInPlace(std::vector< ValueType1 > &target, ValueType2 const &factor)
Multiplies each element of the given vector with the given factor and writes the result into the vect...
bool hasNonZeroEntry(std::vector< T > const &v)
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
bool isOne(ValueType const &a)
bool isZero(ValueType const &a)
ValueType sqrt(ValueType const &number)
bool containsOnlyTrivialObjectives() const
std::shared_ptr< SparseModelType > preprocessedModel