Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StandardPcaaWeightVectorChecker.cpp
Go to the documentation of this file.
2
3#include <map>
4#include <set>
5
18#include "storm/utility/graph.h"
21
27
28namespace storm {
29namespace modelchecker {
30namespace multiobjective {
31
32template<class SparseModelType>
35 : PcaaWeightVectorChecker<SparseModelType>(preprocessorResult.objectives) {
36 // Intantionally left empty
37}
38
39template<class SparseModelType>
43 STORM_LOG_THROW(rewardAnalysis.rewardFinitenessType != preprocessing::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException,
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.");
50 STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException,
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.");
53 STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
54 "The model has multiple initial states.");
55
56 // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers.
57 // We can also merge the states that will have reward zero anyway.
58 storm::storage::BitVector maybeStates = rewardAnalysis.totalRewardLessInfinityEStates.get() & ~rewardAnalysis.reward0AStates;
59 storm::storage::BitVector finiteTotalRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(
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);
64 }
66 auto mergerResult =
67 merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false),
68 std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices);
69
70 // Initialize data specific for the considered model type
71 initializeModelTypeSpecificData(*mergerResult.model);
72
73 // Initilize general data of the model
74 transitionMatrix = std::move(mergerResult.model->getTransitionMatrix());
75 initialState = *mergerResult.model->getInitialStates().begin();
76 totalReward0EStates = rewardAnalysis.totalReward0EStates % maybeStates;
77 if (mergerResult.targetState) {
78 // There is an additional state in the result
79 totalReward0EStates.resize(totalReward0EStates.size() + 1, true);
80
81 // The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself.
82 storm::storage::BitVector targetStateAsVector(transitionMatrix.getRowGroupCount(), false);
83 targetStateAsVector.set(*mergerResult.targetState, true);
84 ecChoicesHint = transitionMatrix.getRowFilter(
85 storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), transitionMatrix.transpose(true),
86 storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector));
87 ecChoicesHint.set(transitionMatrix.getRowGroupIndices()[*mergerResult.targetState], true);
88 } else {
89 ecChoicesHint = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
90 }
92 // set data for unbounded objectives
93 lraObjectives = storm::storage::BitVector(this->objectives.size(), false);
94 objectivesWithNoUpperTimeBound = storm::storage::BitVector(this->objectives.size(), false);
95 actionsWithoutRewardInUnboundedPhase = storm::storage::BitVector(transitionMatrix.getRowCount(), 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);
100 actionsWithoutRewardInUnboundedPhase &= storm::utility::vector::filterZero(actionRewards[objIndex]);
101 }
102 if (formula.getSubformula().isLongRunAverageRewardFormula()) {
103 lraObjectives.set(objIndex, true);
104 objectivesWithNoUpperTimeBound.set(objIndex, true);
105 }
107
108 // Set data for LRA objectives (if available)
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());
115 }
116
117 // initialize data for the results
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);
123
124 // Print some statistics (if requested)
126 STORM_PRINT_AND_LOG("Weight Vector Checker Statistics:\n");
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();
134 }
135 STORM_PRINT_AND_LOG(numLraMecStates << " states lie on such an end component.\n");
136 }
138 }
139}
140
141template<class SparseModelType>
142void StandardPcaaWeightVectorChecker<SparseModelType>::check(Environment const& env, std::vector<ValueType> const& weightVector) {
143 checkHasBeenCalled = true;
144 STORM_LOG_INFO("Invoked WeightVectorChecker with weights \n"
145 << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVector)));
146
147 // Prepare and invoke weighted infinite horizon (long run average) phase
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) {
152 ValueType weight =
153 storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
154 storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weight);
155 if (!stateRewards.empty() && !stateRewards[objIndex].empty()) {
156 if (!weightedStateRewardVector) {
157 weightedStateRewardVector = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
158 }
159 storm::utility::vector::addScaledVector(weightedStateRewardVector.get(), stateRewards[objIndex], weight);
160 }
161 }
162 infiniteHorizonWeightedPhase(env, weightedRewardVector, weightedStateRewardVector);
163 // Clear all values of the weighted reward vector
164 weightedRewardVector.assign(weightedRewardVector.size(), storm::utility::zero<ValueType>());
165 }
166
167 // Prepare and invoke weighted indefinite horizon (unbounded total reward) phase
168 auto totalRewardObjectives = objectivesWithNoUpperTimeBound & ~lraObjectives;
169 for (auto objIndex : totalRewardObjectives) {
170 if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
171 storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], -weightVector[objIndex]);
172 } else {
173 storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weightVector[objIndex]);
174 }
175 }
176 unboundedWeightedPhase(env, weightedRewardVector, weightVector);
177
178 unboundedIndividualPhase(env, weightVector);
179 // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound
180 for (auto const& obj : this->objectives) {
181 if (!obj.formula->getSubformula().isTotalRewardFormula() && !obj.formula->getSubformula().isLongRunAverageRewardFormula()) {
182 boundedPhase(env, weightVector, weightedRewardVector);
183 break;
184 }
185 }
186 STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: "
187 << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getUnderApproximationOfInitialStateResults())));
188 // Validate that the results are sufficiently precise
189 ValueType resultingWeightedPrecision =
190 storm::utility::abs<ValueType>(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) -
191 storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector));
192 resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector));
193 STORM_LOG_THROW(resultingWeightedPrecision <= this->getWeightedPrecision(), storm::exceptions::UnexpectedException,
194 "The desired precision was not reached");
195}
196
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]);
205 }
206 return res;
207}
208
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]);
217 }
218 return res;
219}
220
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.");
229 }
230
231 storm::storage::Scheduler<ValueType> result(this->optimalChoices.size());
232 uint_fast64_t state = 0;
233 for (auto const& choice : optimalChoices) {
234 result.setChoice(choice, state);
235 ++state;
236 }
237 return result;
238}
239
240template<typename ValueType>
242 storm::storage::BitVector const& consideredStates, storm::storage::BitVector const& statesToReach, std::vector<uint64_t>& choices,
243 storm::storage::BitVector const* allowedChoices = nullptr) {
244 std::vector<uint64_t> stack;
245 storm::storage::BitVector processedStates = statesToReach;
246 stack.insert(stack.end(), processedStates.begin(), processedStates.end());
247 uint64_t currentState = 0;
248
249 while (!stack.empty()) {
250 currentState = stack.back();
251 stack.pop_back();
252
253 for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) {
254 auto predecessor = predecessorEntry.getColumn();
255 if (consideredStates.get(predecessor) && !processedStates.get(predecessor)) {
256 // Find a choice leading to an already processed state (such a choice has to exist since this is a predecessor of the currentState)
257 auto const& groupStart = transitionMatrix.getRowGroupIndices()[predecessor];
258 auto const& groupEnd = transitionMatrix.getRowGroupIndices()[predecessor + 1];
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;
265 break;
266 }
267 }
268 if (hasSuccessorInProcessedStates) {
269 choices[predecessor] = row - groupStart;
270 processedStates.set(predecessor, true);
271 stack.push_back(predecessor);
272 break;
273 }
274 }
275 STORM_LOG_ASSERT(allowedChoices || row < groupEnd,
276 "Unable to find choice at a predecessor of a processed state that leads to a processed state.");
277 }
278 }
279 }
280 STORM_LOG_ASSERT(consideredStates.isSubsetOf(processedStates), "Not all states have been processed.");
281}
282
283template<typename ValueType>
285 storm::storage::BitVector const& consideredStates, storm::storage::BitVector const& statesToAvoid,
286 storm::storage::BitVector const& allowedChoices, std::vector<uint64_t>& choices) {
287 for (auto state : consideredStates) {
288 auto const& groupStart = transitionMatrix.getRowGroupIndices()[state];
289 auto const& groupEnd = transitionMatrix.getRowGroupIndices()[state + 1];
290 bool choiceFound = false;
291 for (uint64_t row = allowedChoices.getNextSetIndex(groupStart); row < groupEnd; row = allowedChoices.getNextSetIndex(row + 1)) {
292 choiceFound = true;
293 for (auto const& element : transitionMatrix.getRow(row)) {
294 if (statesToAvoid.get(element.getColumn())) {
295 choiceFound = false;
296 break;
297 }
298 }
299 if (choiceFound) {
300 choices[state] = row - groupStart;
301 break;
302 }
303 }
304 STORM_LOG_ASSERT(choiceFound, "Unable to find choice for a state.");
305 }
306}
307
308template<typename ValueType>
309std::vector<uint64_t> computeValidInitialScheduler(storm::storage::SparseMatrix<ValueType> const& matrix, storm::storage::BitVector const& rowsWithSumLessOne) {
310 std::vector<uint64_t> result(matrix.getRowGroupCount());
311 auto const& groups = matrix.getRowGroupIndices();
312 auto backwardsTransitions = matrix.transpose(true);
313 storm::storage::BitVector processedStates(result.size(), false);
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);
318 }
319 }
320
321 computeSchedulerProb1(matrix, backwardsTransitions, ~processedStates, processedStates, result);
322 return result;
323}
324
330template<typename ValueType>
332 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& finitelyOftenChoices,
333 storm::storage::BitVector safeStates, std::vector<uint64_t>& choices) {
334 auto badStates = transitionMatrix.getRowGroupFilter(finitelyOftenChoices, true) & ~safeStates;
335 // badStates shall only be reached finitely often
336
337 auto reachBadWithProbGreater0AStates = storm::utility::graph::performProbGreater0A(
338 transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, ~safeStates, badStates, false, 0, ~finitelyOftenChoices);
339 // States in ~reachBadWithProbGreater0AStates can avoid bad states forever by only taking ~finitelyOftenChoices.
340 // We compute a scheduler for these states achieving exactly this (but we exclude the safe states)
341 auto avoidBadStates = ~reachBadWithProbGreater0AStates & ~safeStates;
342 computeSchedulerProb0(transitionMatrix, backwardTransitions, avoidBadStates, reachBadWithProbGreater0AStates, ~finitelyOftenChoices, choices);
343
344 // We need to take care of states that will reach a bad state with prob greater 0 (including the bad states themselves).
345 // due to the precondition, we know that it has to be possible to eventually avoid the bad states for ever.
346 // Perform a backwards search from the avoid states and store choices with prob. 1
347 computeSchedulerProb1(transitionMatrix, backwardTransitions, reachBadWithProbGreater0AStates, avoidBadStates | safeStates, choices);
348}
349
350template<class SparseModelType>
352 std::vector<ValueType> const& weightedActionRewardVector,
353 boost::optional<std::vector<ValueType>> const& weightedStateRewardVector) {
354 // Compute the optimal (weighted) lra value for each mec, keeping track of the optimal choices
355 STORM_LOG_ASSERT(lraMecDecomposition, "Mec decomposition for lra computations not initialized.");
356 storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType> helper = createNondetInfiniteHorizonHelper(this->transitionMatrix);
357 helper.provideLongRunComponentDecomposition(lraMecDecomposition->mecs);
358 helper.setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
359 helper.setProduceScheduler(true);
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]; };
366 } else {
367 stateValueGetter = [](uint64_t const&) { return storm::utility::zero<ValueType>(); };
368 }
369 lraMecDecomposition->auxMecValues[mecIndex] = helper.computeLraForComponent(env, stateValueGetter, actionValueGetter, mec);
370 }
371 // Extract the produced optimal choices for the MECs
372 this->optimalChoices = std::move(helper.getProducedOptimalChoices());
373}
374
375template<class SparseModelType>
376void StandardPcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(Environment const& env, std::vector<ValueType> const& weightedRewardVector,
377 std::vector<ValueType> const& weightVector) {
378 // Catch the case where all values on the RHS of the MinMax equation system are zero.
379 if (this->objectivesWithNoUpperTimeBound.empty() ||
380 ((this->lraObjectives.empty() || !storm::utility::vector::hasNonZeroEntry(lraMecDecomposition->auxMecValues)) &&
381 !storm::utility::vector::hasNonZeroEntry(weightedRewardVector))) {
382 this->weightedResult.assign(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
383 storm::storage::BitVector statesInLraMec(transitionMatrix.getRowGroupCount(), false);
384 if (this->lraMecDecomposition) {
385 for (auto const& mec : this->lraMecDecomposition->mecs) {
386 for (auto const& sc : mec) {
387 statesInLraMec.set(sc.first, true);
388 }
389 }
390 }
391 // Get an arbitrary scheduler that yields finite reward for all objectives
392 computeSchedulerFinitelyOften(transitionMatrix, transitionMatrix.transpose(true), ~actionsWithoutRewardInUnboundedPhase, statesInLraMec,
393 this->optimalChoices);
394 return;
395 }
396
397 updateEcQuotient(weightedRewardVector);
398
399 // Set up the choice values
400 storm::utility::vector::selectVectorValues(ecQuotient->auxChoiceValues, ecQuotient->ecqToOriginalChoiceMapping, weightedRewardVector);
401 std::map<uint64_t, uint64_t> ecqStateToOptimalMecMap;
402 if (!lraObjectives.empty()) {
403 // We also need to assign a value for each ecQuotientChoice that corresponds to "staying" in the eliminated EC. (at this point these choices should all
404 // have a value of zero). Since each of the eliminated ECs has to contain *at least* one LRA EC, we need to find the largest value among the contained
405 // LRA ECs
406 storm::storage::BitVector foundEcqChoices(ecQuotient->matrix.getRowCount(), false); // keeps track of choices we have already seen before
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()) {
412 // The mec was not part of the ecquotient. This means that it must have value 0.
413 // No further processing is needed.
414 continue;
415 }
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) {
422 // We have seen this ecqState for the first time.
424 "Expected a total reward of zero for choices that represent staying in an EC for ever.");
425 ecqChoiceValue = mecValue;
426 } else {
427 if (mecValue > ecqChoiceValue) { // found a larger value
428 ecqChoiceValue = mecValue;
429 insertionRes.first->second = mecIndex;
430 }
431 }
432 }
433 }
434
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();
445 }
446 if (solver->hasUpperBound()) {
447 req.clearUpperBounds();
448 }
449 if (req.validInitialScheduler()) {
450 solver->setInitialScheduler(computeValidInitialScheduler(ecQuotient->matrix, ecQuotient->rowsWithSumLessOne));
451 req.clearValidInitialScheduler();
452 }
453 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
454 "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
455 solver->setRequirementsChecked(true);
456
457 // Use the (0...0) vector as initial guess for the solution.
458 std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero<ValueType>());
459
460 solver->solveEquations(env, ecQuotient->auxStateValues, ecQuotient->auxChoiceValues);
461 this->weightedResult = std::vector<ValueType>(transitionMatrix.getRowGroupCount());
462
463 transformEcqSolutionToOriginalModel(ecQuotient->auxStateValues, solver->getSchedulerChoices(), ecqStateToOptimalMecMap, this->weightedResult,
464 this->optimalChoices);
465}
466
467template<class SparseModelType>
468void StandardPcaaWeightVectorChecker<SparseModelType>::unboundedIndividualPhase(Environment const& env, std::vector<ValueType> const& weightVector) {
469 if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) {
470 uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin();
471 objectiveResults[objIndex] = weightedResult;
472 if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
473 storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one<ValueType>());
474 }
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>());
478 }
479 }
480 } else {
481 storm::storage::SparseMatrix<ValueType> deterministicMatrix = transitionMatrix.selectRowsFromRowGroups(this->optimalChoices, false);
482 storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
483 std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount()); // allocate here
485
486 auto infiniteHorizonHelper = createDetInfiniteHorizonHelper(deterministicMatrix);
487 infiniteHorizonHelper.provideBackwardTransitions(deterministicBackwardTransitions);
488
489 // We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives
490 // computed so far. Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i.
491 std::vector<ValueType> weightedSumOfUncheckedObjectives = weightedResult;
492 ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound);
493
494 for (uint_fast64_t const& objIndex : storm::utility::vector::getSortedIndices(weightVector)) {
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]];
502 };
504 if (stateRewards.empty() || stateRewards[objIndex].empty()) {
505 stateValueGetter = [](uint64_t const&) { return storm::utility::zero<ValueType>(); };
506 } else {
507 stateValueGetter = [&](uint64_t const& s) { return stateRewards[objIndex][s]; };
508 }
509 objectiveResults[objIndex] = infiniteHorizonHelper.computeLongRunAverageValues(env, stateValueGetter, actionValueGetter);
510 } else { // i.e. a total reward objective
511 storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, transitionMatrix.getRowGroupIndices(),
512 actionRewards[objIndex]);
513 storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards);
514 // As maybestates we pick the states from which a state with reward is reachable
516 deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards);
517
518 // Compute the estimate for this objective
519 if (!storm::utility::isZero(weightVector[objIndex]) && !storm::utility::isZero(sumOfWeightsOfUncheckedObjectives)) {
520 objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
521 ValueType scalingFactor = storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives;
522 if (storm::solver::minimize(obj.formula->getOptimalityType())) {
523 scalingFactor *= -storm::utility::one<ValueType>();
524 }
525 storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor);
526 storm::utility::vector::clip(objectiveResults[objIndex], obj.lowerResultBound, obj.upperResultBound);
527 }
528 // Make sure that the objectiveResult is initialized correctly
529 objectiveResults[objIndex].resize(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
530
531 if (!maybeStates.empty()) {
532 bool needEquationSystem =
535 deterministicMatrix.getSubmatrix(true, maybeStates, maybeStates, needEquationSystem);
536 if (needEquationSystem) {
537 // Converting the matrix from the fixpoint notation to the form needed for the equation
538 // system. That is, we go from x = A*x + b to (I-A)x = b.
539 submatrix.convertToEquationSystem();
540 }
541
542 // Prepare solution vector and rhs of the equation system.
543 std::vector<ValueType> x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates);
544 std::vector<ValueType> b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates);
545
546 // Now solve the resulting equation system.
547 std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, submatrix);
548 auto req = solver->getRequirements(env);
549 solver->clearBounds();
550 storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates;
551 submatrixRowsWithSumLessOne.complement();
552 this->setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b);
553 if (solver->hasLowerBound()) {
554 req.clearLowerBounds();
555 }
556 if (solver->hasUpperBound()) {
557 req.clearUpperBounds();
558 }
559 STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
560 "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
561 solver->solveEquations(env, x, b);
562 // Set the result for this objective accordingly
563 storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], maybeStates, x);
564 }
565 storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], ~maybeStates, storm::utility::zero<ValueType>());
566 }
567 // Update the estimate for the next objectives.
568 if (!storm::utility::isZero(weightVector[objIndex])) {
569 storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]);
570 sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex];
571 }
572 } else {
573 objectiveResults[objIndex] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
574 }
575 }
576 }
577}
578
579template<class SparseModelType>
580void StandardPcaaWeightVectorChecker<SparseModelType>::updateEcQuotient(std::vector<ValueType> const& weightedRewardVector) {
581 // Check whether we need to update the currently cached ecElimResult
582 storm::storage::BitVector newTotalReward0Choices = storm::utility::vector::filterZero(weightedRewardVector);
583 storm::storage::BitVector zeroLraRewardChoices(weightedRewardVector.size(), true);
584 if (lraMecDecomposition) {
585 for (uint64_t mecIndex = 0; mecIndex < lraMecDecomposition->mecs.size(); ++mecIndex) {
586 if (!storm::utility::isZero(lraMecDecomposition->auxMecValues[mecIndex])) {
587 // The mec has a non-zero value, so flag all its choices as non-zero
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);
592 }
593 }
594 }
595 }
596 }
597 storm::storage::BitVector newReward0Choices = newTotalReward0Choices & zeroLraRewardChoices;
598 if (!ecQuotient || ecQuotient->origReward0Choices != newReward0Choices) {
599 // It is sufficient to consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero).
600 auto nonZeroRewardStates = transitionMatrix.getRowGroupFilter(newReward0Choices, true);
601 nonZeroRewardStates.complement();
603 transitionMatrix.transpose(true), storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), nonZeroRewardStates);
604
605 // Remove neutral end components, i.e., ECs in which no total reward is earned.
606 // Note that such ECs contain one (or maybe more) LRA ECs.
607 auto ecElimResult = storm::transformer::EndComponentEliminator<ValueType>::transform(transitionMatrix, subsystemStates,
608 ecChoicesHint & newTotalReward0Choices, totalReward0EStates);
609
610 storm::storage::BitVector rowsWithSumLessOne(ecElimResult.matrix.getRowCount(), false);
611 for (uint64_t row = 0; row < rowsWithSumLessOne.size(); ++row) {
612 if (ecElimResult.matrix.getRow(row).getNumberOfEntries() == 0) {
613 rowsWithSumLessOne.set(row, true);
614 } else {
615 for (auto const& entry : transitionMatrix.getRow(ecElimResult.newToOldRowMapping[row])) {
616 if (!subsystemStates.get(entry.getColumn())) {
617 rowsWithSumLessOne.set(row, true);
618 break;
619 }
620 }
621 }
622 }
623
624 ecQuotient = EcQuotient();
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);
633 }
634 }
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());
641 }
642}
643
644template<class SparseModelType>
646 bool requiresUpper, uint64_t objIndex,
648 storm::storage::BitVector const& rowsWithSumLessOne,
649 std::vector<ValueType> const& rewards) const {
650 // Check whether bounds are already available
651 if (this->objectives[objIndex].lowerResultBound) {
652 solver.setLowerBound(this->objectives[objIndex].lowerResultBound.get());
653 }
654 if (this->objectives[objIndex].upperResultBound) {
655 solver.setUpperBound(this->objectives[objIndex].upperResultBound.get());
656 }
657
658 if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) {
659 computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
660 }
661}
662
663template<class SparseModelType>
665 bool requiresUpper, std::vector<ValueType> const& weightVector,
666 storm::storage::BitVector const& objectiveFilter,
668 storm::storage::BitVector const& rowsWithSumLessOne,
669 std::vector<ValueType> const& rewards) const {
670 // Check whether bounds are already available
671 boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectiveFilter & ~lraObjectives);
672 if (lowerBound) {
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;
677 }
678 }
679 solver.setLowerBound(lowerBound.get());
680 }
681 boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, objectiveFilter);
682 if (upperBound) {
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;
687 }
688 }
689 solver.setUpperBound(upperBound.get());
690 }
691
692 if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) {
693 computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
694 }
695}
696
697template<class SparseModelType>
699 bool requiresUpper,
701 storm::storage::BitVector const& rowsWithSumLessOne,
702 std::vector<ValueType> const& rewards) const {
703 // Compute the one step target probs
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);
707 }
708
709 if (requiresLower && !solver.hasLowerBound()) {
710 // Compute lower bounds
711 std::vector<ValueType> negativeRewards;
712 negativeRewards.reserve(transitions.getRowCount());
713 uint64_t row = 0;
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);
718 }
719 ++row;
720 }
721 if (!negativeRewards.empty()) {
722 negativeRewards.resize(row, storm::utility::zero<ValueType>());
723 std::vector<ValueType> lowerBounds =
724 storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ValueType>(transitions, negativeRewards, oneStepTargetProbs)
726 storm::utility::vector::scaleVectorInPlace(lowerBounds, -storm::utility::one<ValueType>());
727 solver.setLowerBounds(std::move(lowerBounds));
728 } else {
729 solver.setLowerBound(storm::utility::zero<ValueType>());
730 }
731 }
732
733 // Compute upper bounds
734 if (requiresUpper && !solver.hasUpperBound()) {
735 std::vector<ValueType> positiveRewards;
736 positiveRewards.reserve(transitions.getRowCount());
737 uint64_t row = 0;
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);
742 }
743 ++row;
744 }
745 if (!positiveRewards.empty()) {
746 positiveRewards.resize(row, storm::utility::zero<ValueType>());
747 solver.setUpperBound(
748 storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType>(transitions, positiveRewards, oneStepTargetProbs).computeUpperBound());
749 } else {
750 solver.setUpperBound(storm::utility::zero<ValueType>());
751 }
752 }
753}
754
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);
762
763 // Keep track of states for which no choice has been set yet.
764 storm::storage::BitVector unprocessedStates(transitionMatrix.getRowGroupCount(), true);
765
766 // For each eliminated ec, keep track of the states (within the ec) that we want to reach and the states for which a choice needs to be set
767 // (Declared already at this point to avoid expensive allocations in each loop iteration)
768 storm::storage::BitVector ecStatesToReach(transitionMatrix.getRowGroupCount(), false);
769 storm::storage::BitVector ecStatesToProcess(transitionMatrix.getRowGroupCount(), false);
770
771 // Run through each state of the ec quotient as well as the associated state(s) of the original model
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)) {
778 // We stay in the current state(s) forever (End component)
779 // We need to set choices in a way that (i) the optimal LRA Mec is reached (if there is any) and (ii) 0 total reward is collected.
780 if (!ecqStateToOptimalMecMap.empty()) {
781 // The current ecqState represents an elimnated EC and we need to stay in this EC and we need to make sure that optimal MEC decisions are
782 // performed within this EC.
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()) {
786 // LRA mec and eliminated EC coincide
787 for (auto const& state : origStates) {
788 STORM_LOG_ASSERT(lraMec.containsState(state), "Expected state to be contained in the lra mec.");
789 // Note that the optimal choice for this state has already been set in the infinite horizon phase.
790 unprocessedStates.set(state, false);
791 originalSolution[state] = ecqSolution[ecqState];
792 }
793 } else {
794 // LRA mec is proper subset of eliminated ec. There are also other states for which we have to set choices leading to the LRA MEC inside.
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);
801 // Note that the optimal choice for this state has already been set in the infinite horizon phase.
802 } else {
803 ecStatesToProcess.set(state, true);
804 }
805 unprocessedStates.set(state, false);
806 originalSolution[state] = ecqSolution[ecqState];
807 }
808 computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices,
809 &ecQuotient->origTotalReward0Choices);
810 // Clear bitvectors for next ecqState.
811 ecStatesToProcess.clear();
812 ecStatesToReach.clear();
813 }
814 } else {
815 // If there is no LRA Mec to reach, we just need to make sure that finite total reward is collected for all objectives
816 // In this branch our BitVectors have a slightly different meaning, so we create more readable aliases
817 storm::storage::BitVector& ecStatesToAvoid = ecStatesToReach;
818 bool needSchedulerComputation = false;
819 STORM_LOG_ASSERT(storm::utility::isZero(ecqSolution[ecqState]),
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>(); // i.e. ecqSolution[ecqState];
823 ecStatesToProcess.set(state, true);
824 }
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;
833 } else {
834 // this state should not be reached infinitely often
835 ecStatesToAvoid.set(state, true);
836 needSchedulerComputation = true;
837 }
838 }
839 if (needSchedulerComputation) {
840 // There are ec states which we should not visit infinitely often
841 auto ecStatesThatCanAvoid =
842 storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardsTransitions,
843 ecStatesToProcess, ecStatesToAvoid, false, 0, valid0RewardChoices);
844 ecStatesThatCanAvoid.complement();
845 // Set the choice for all states that can achieve value 0
846 computeSchedulerProb0(transitionMatrix, backwardsTransitions, ecStatesThatCanAvoid, ecStatesToAvoid, valid0RewardChoices,
847 originalOptimalChoices);
848 // Set the choice for all remaining states
849 computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess & ~ecStatesToAvoid, ecStatesToAvoid, originalOptimalChoices,
850 &validChoices);
851 }
852 ecStatesToAvoid.clear();
853 ecStatesToProcess.clear();
854 }
855 } else {
856 // We eventually leave the current state(s)
857 // In this case, we can safely take the origChoice at the corresponding state (say 's').
858 // For all other origStates associated with ecqState (if there are any), we make sure that the state 's' is reached almost surely.
859 if (origStates.size() > 1) {
860 for (auto const& state : origStates) {
861 // Check if the orig choice originates from this state
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);
867 } else {
868 STORM_LOG_ASSERT(origStates.size() > 1, "Multiple original states expected.");
869 ecStatesToProcess.set(state, true);
870 }
871 unprocessedStates.set(state, false);
872 originalSolution[state] = ecqSolution[ecqState];
873 }
874 auto validChoices = transitionMatrix.getRowFilter(ecStatesToProcess, ecStatesToProcess | ecStatesToReach);
875 computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices, &validChoices);
876 // Clear bitvectors for next ecqState.
877 ecStatesToProcess.clear();
878 ecStatesToReach.clear();
879 } else {
880 // There is just one state so we take the associated choice.
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);
889 }
890 }
891 }
892
893 // The states that still not have been processed, there is no associated state of the ec quotient.
894 // This is because the value for these states will be 0 under all (lra optimal-) schedulers.
895 storm::utility::vector::setVectorValues(originalSolution, unprocessedStates, storm::utility::zero<ValueType>());
896 // Get a set of states for which we know that no reward (for all objectives) will be collected
897 if (this->lraMecDecomposition) {
898 // In this case, all unprocessed non-lra mec states should reach an (unprocessed) lra mec
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);
903 }
904 }
905 }
906 } else {
907 ecStatesToReach = unprocessedStates & totalReward0EStates;
908 // Set a scheduler for the ecStates that we want to reach
909 computeSchedulerProb0(transitionMatrix, backwardsTransitions, ecStatesToReach, ~unprocessedStates | ~totalReward0EStates,
910 actionsWithoutRewardInUnboundedPhase, originalOptimalChoices);
911 }
912 unprocessedStates &= ~ecStatesToReach;
913 // Set a scheduler for the remaining states
914 computeSchedulerProb1(transitionMatrix, backwardsTransitions, unprocessedStates, ecStatesToReach, originalOptimalChoices);
915}
916
919#ifdef STORM_HAVE_CARL
922#endif
923
924} // namespace multiobjective
925} // namespace modelchecker
926} // namespace storm
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.
virtual ValueType computeLraForComponent(Environment const &env, ValueGetter const &stateValuesGetter, ValueGetter const &actionValuesGetter, storm::storage::MaximalEndComponent const &component) override
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)
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.
Definition BitVector.h:18
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.
Definition Scheduler.h:18
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.
Definition Scheduler.cpp:37
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 ...
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_INFO(message)
Definition logging.h:29
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
#define STORM_PRINT_AND_LOG(message)
Definition macros.h:68
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...
Definition graph.cpp:322
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...
Definition graph.cpp:848
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:680
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...
Definition graph.cpp:967
T dotProduct(std::vector< T > const &firstOperand, std::vector< T > const &secondOperand)
Computes the dot product (aka scalar product) and returns the result.
Definition vector.h:477
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:82
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...
Definition vector.h:188
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:464
std::string toString(std::vector< ValueType > const &vector)
Output vector as string.
Definition vector.h:1149
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.
Definition vector.h:892
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.
Definition vector.h:556
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,...
Definition vector.h:148
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:523
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...
Definition vector.h:451
bool hasNonZeroEntry(std::vector< T > const &v)
Definition vector.h:1103
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
Definition vector.h:1064
bool isOne(ValueType const &a)
Definition constants.cpp:36
bool isZero(ValueType const &a)
Definition constants.cpp:41
ValueType sqrt(ValueType const &number)
LabParser.cpp.
Definition cli.cpp:18