Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMdpPrctlHelper.cpp
Go to the documentation of this file.
2
3#include <boost/container/flat_map.hpp>
4
6
13
15
17
18#include "storm/utility/graph.h"
21
25
29
35
36#include "storm/io/export.h"
41
43
45
54
55namespace storm {
56namespace modelchecker {
57namespace helper {
58
59template<typename ValueType, typename SolutionType>
60std::map<storm::storage::sparse::state_type, SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeRewardBoundedValues(
62 storm::storage::BitVector const& initialStates) {
63 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
64 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing reward bounded values with interval models.");
65 } else {
66 storm::utility::Stopwatch swAll(true), swBuild, swCheck;
67
68 // Get lower and upper bounds for the solution.
69 auto lowerBound = rewardUnfolding.getLowerObjectiveBound();
70 auto upperBound = rewardUnfolding.getUpperObjectiveBound();
71
72 // Initialize epoch models
73 auto initEpoch = rewardUnfolding.getStartEpoch();
74 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
75
76 // initialize data that will be needed for each epoch
77 std::vector<ValueType> x, b;
78 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
79
80 ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(
81 initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
82 Environment preciseEnv = env;
83 preciseEnv.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(precision));
84
85 // In case of cdf export we store the necessary data.
86 std::vector<std::vector<ValueType>> cdfData;
87
88 storm::utility::ProgressMeasurement progress("epochs");
89 progress.setMaxCount(epochOrder.size());
90 progress.startNewMeasurement(0);
91 uint64_t numCheckedEpochs = 0;
92 for (auto const& epoch : epochOrder) {
93 swBuild.start();
94 auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
95 swBuild.stop();
96 swCheck.start();
97 rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, dir, x, b, minMaxSolver, lowerBound, upperBound));
98 swCheck.stop();
99 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() &&
100 !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
101 std::vector<ValueType> cdfEntry;
102 for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) {
103 uint64_t offset = rewardUnfolding.getDimension(i).boundType == helper::rewardbounded::DimensionBoundType::LowerBound ? 1 : 0;
104 cdfEntry.push_back(storm::utility::convertNumber<ValueType>(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) *
105 rewardUnfolding.getDimension(i).scalingFactor);
106 }
107 cdfEntry.push_back(rewardUnfolding.getInitialStateResult(epoch));
108 cdfData.push_back(std::move(cdfEntry));
109 }
110 ++numCheckedEpochs;
111 progress.updateProgress(numCheckedEpochs);
113 break;
114 }
115 }
116
117 std::map<storm::storage::sparse::state_type, ValueType> result;
118 for (auto initState : initialStates) {
119 result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState);
120 }
121
122 swAll.stop();
123
124 if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet()) {
125 std::vector<std::string> headers;
126 for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) {
127 headers.push_back(rewardUnfolding.getDimension(i).formula->toString());
128 }
129 headers.push_back("Result");
130 storm::io::exportDataToCSVFile<ValueType, std::string, std::string>(
131 storm::settings::getModule<storm::settings::modules::IOSettings>().getExportCdfDirectory() + "cdf.csv", cdfData, headers);
132 }
133
134 if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
135 STORM_PRINT_AND_LOG("---------------------------------\n");
136 STORM_PRINT_AND_LOG("Statistics:\n");
137 STORM_PRINT_AND_LOG("---------------------------------\n");
138 STORM_PRINT_AND_LOG(" #checked epochs: " << epochOrder.size() << ".\n");
139 STORM_PRINT_AND_LOG(" overall Time: " << swAll << ".\n");
140 STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << ".\n");
141 STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << ".\n");
142 STORM_PRINT_AND_LOG("---------------------------------\n");
143 }
144
145 return result;
146 }
147}
148
149template<typename ValueType, typename SolutionType>
151 Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
152 storm::storage::BitVector const& nextStates) {
153 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
154 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support next probabilities with reward models.");
155 } else {
156 // Create the vector with which to multiply and initialize it correctly.
157 std::vector<ValueType> result(transitionMatrix.getRowGroupCount());
158 storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
159
160 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
161 multiplier->multiplyAndReduce(env, dir, result, nullptr, result);
162
163 return result;
164 }
165}
166
167template<typename ValueType, typename SolutionType = ValueType>
168std::vector<uint_fast64_t> computeValidSchedulerHint(Environment const& env, SemanticSolutionType const& type,
169 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
170 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
171 storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates,
172 storm::storage::BitVector const& targetStates,
173 boost::optional<storm::storage::BitVector> const& selectedChoices) {
174 storm::storage::Scheduler<SolutionType> validScheduler(maybeStates.size());
175
177 storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler,
178 selectedChoices);
179 } else if (type == SemanticSolutionType::ExpectedRewards) {
180 storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates,
181 validScheduler, selectedChoices);
182 } else {
183 STORM_LOG_ASSERT(false, "Unexpected equation system type.");
184 }
185
186 // Extract the relevant parts of the scheduler for the solver.
187 std::vector<uint64_t> schedulerHint;
188 schedulerHint.reserve(maybeStates.getNumberOfSetBits());
189 if (selectedChoices) {
190 // There might be unselected choices so the local choice indices from the scheduler need to be adapted
191 for (auto maybeState : maybeStates) {
192 auto choice = validScheduler.getChoice(maybeState).getDeterministicChoice();
193 auto const groupStart = transitionMatrix.getRowGroupIndices()[maybeState];
194 auto const origGlobalChoiceIndex = groupStart + choice;
195 STORM_LOG_ASSERT(selectedChoices->get(origGlobalChoiceIndex), "The computed scheduler selects an illegal choice.");
196 // Count the number of unselected choices in [groupStart, origGlobalChoiceIndex) and subtract that from choice
197 for (auto pos = selectedChoices->getNextUnsetIndex(groupStart); pos < origGlobalChoiceIndex; pos = selectedChoices->getNextUnsetIndex(pos + 1)) {
198 --choice;
199 }
200 schedulerHint.push_back(choice);
201 }
202 } else {
203 for (auto maybeState : maybeStates) {
204 schedulerHint.push_back(validScheduler.getChoice(maybeState).getDeterministicChoice());
205 }
206 }
207 return schedulerHint;
208}
209
210template<typename ValueType>
213 // Intentionally left empty.
214 }
215
216 bool hasSchedulerHint() const {
217 return static_cast<bool>(schedulerHint);
218 }
219
220 bool hasValueHint() const {
221 return static_cast<bool>(valueHint);
222 }
223
224 bool hasLowerResultBound() const {
225 return static_cast<bool>(lowerResultBound);
226 }
227
228 ValueType const& getLowerResultBound() const {
229 return lowerResultBound.get();
230 }
231
232 bool hasUpperResultBound() const {
233 return static_cast<bool>(upperResultBound);
234 }
235
236 bool hasUpperResultBounds() const {
237 return static_cast<bool>(upperResultBounds);
238 }
239
240 ValueType const& getUpperResultBound() const {
241 return upperResultBound.get();
242 }
243
244 std::vector<ValueType>& getUpperResultBounds() {
245 return upperResultBounds.get();
246 }
247
248 std::vector<ValueType> const& getUpperResultBounds() const {
249 return upperResultBounds.get();
250 }
251
252 std::vector<uint64_t>& getSchedulerHint() {
253 return schedulerHint.get();
254 }
255
256 std::vector<ValueType>& getValueHint() {
257 return valueHint.get();
258 }
259
262 }
263
265 return computeUpperBounds;
266 }
267
268 bool hasUniqueSolution() const {
269 return uniqueSolution;
270 }
271
272 bool hasNoEndComponents() const {
273 return noEndComponents;
274 }
275
276 boost::optional<std::vector<uint64_t>> schedulerHint;
277 boost::optional<std::vector<ValueType>> valueHint;
278 boost::optional<ValueType> lowerResultBound;
279 boost::optional<ValueType> upperResultBound;
280 boost::optional<std::vector<ValueType>> upperResultBounds;
285};
286
287template<typename ValueType, typename SolutionType>
289 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates,
290 boost::optional<storm::storage::BitVector> const& selectedChoices, ModelCheckerHint const& hint,
291 bool skipECWithinMaybeStatesCheck) {
292 // Deal with scheduler hint.
293 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint()) {
294 if (hintStorage.hasSchedulerHint()) {
295 STORM_LOG_WARN("A scheduler hint was provided, but the solver requires a specific one. The provided scheduler hint will be ignored.");
296 } else {
297 auto const& schedulerHint = hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint();
298 std::vector<uint64_t> hintChoices;
299
300 // The scheduler hint is only applicable if it induces no BSCC consisting of maybe states.
301 bool hintApplicable;
302 if (!skipECWithinMaybeStatesCheck) {
303 hintChoices.reserve(maybeStates.size());
304 for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) {
305 hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice());
306 }
307 hintApplicable =
308 storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full();
309 } else {
310 hintApplicable = true;
311 }
312
313 if (hintApplicable) {
314 // Compute the hint w.r.t. the given subsystem.
315 hintChoices.clear();
316 hintChoices.reserve(maybeStates.getNumberOfSetBits());
317 for (auto state : maybeStates) {
318 uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice();
319 if (selectedChoices) {
320 uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state];
321 uint_fast64_t lastChoice = firstChoice + hintChoice;
322 hintChoice = 0;
323 for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice;
324 choice = selectedChoices->getNextSetIndex(choice + 1)) {
325 ++hintChoice;
326 }
327 }
328 hintChoices.push_back(hintChoice);
329 }
330 hintStorage.schedulerHint = std::move(hintChoices);
331 }
332 }
333 }
334
335 // Deal with solution value hint. Only applicable if there are no End Components consisting of maybe states.
336 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint() &&
337 (skipECWithinMaybeStatesCheck || hintStorage.hasSchedulerHint() ||
338 storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)
339 .full())) {
340 hintStorage.valueHint = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<SolutionType>().getResultHint(), maybeStates);
341 }
342}
343
344template<typename ValueType, typename SolutionType>
347 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates,
348 storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, bool produceScheduler,
349 boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
351
352 // There are no end components if we minimize until probabilities or
353 // maximize reachability rewards or if the hint tells us so.
354 result.noEndComponents = (dir == storm::solver::OptimizationDirection::Minimize && type == SemanticSolutionType::UntilProbabilities) ||
355 (dir == storm::solver::OptimizationDirection::Maximize && type == SemanticSolutionType::ExpectedRewards) ||
356 (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
357
358 // If there are no end components, the solution is unique. (Note that the other direction does not hold,
359 // e.g., end components in which infinite reward is collected.
360 result.uniqueSolution = result.hasNoEndComponents();
361
362 // Check for requirements of the solver.
363 bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint();
366 minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, result.noEndComponents, dir, hasSchedulerHint, produceScheduler);
367 if (requirements.hasEnabledRequirement()) {
368 // If the solver still requires no end-components, we have to eliminate them later.
369 if (requirements.uniqueSolution()) {
371 "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
372 STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires a unique solution.");
373 result.eliminateEndComponents = true;
374 // If end components have been eliminated we can assume a unique solution.
375 result.uniqueSolution = true;
376 requirements.clearUniqueSolution();
377 // If we compute until probabilities, we can even assume the absence of end components.
378 // Note that in the case of minimizing expected rewards there might still be end components in which reward is collected.
380 }
381
382 // If the solver requires an initial scheduler, compute one now. Note that any scheduler is valid if there are no end components.
383 if (requirements.validInitialScheduler() && !result.noEndComponents) {
384 STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
385 result.schedulerHint = computeValidSchedulerHint<ValueType, SolutionType>(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates,
386 targetStates, selectedChoices);
387 requirements.clearValidInitialScheduler();
388 }
389
390 // Finally, we have information on the bounds depending on the problem type.
392 requirements.clearBounds();
393 } else if (type == SemanticSolutionType::ExpectedRewards) {
394 requirements.clearLowerBounds();
395 }
396 if (requirements.upperBounds()) {
397 result.computeUpperBounds = true;
398 requirements.clearUpperBounds();
399 }
400 STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
401 "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
402 } else {
403 STORM_LOG_DEBUG("Solver has no requirements.");
404 }
405
406 // Only if there is no end component decomposition that we will need to do later, we use value and scheduler
407 // hints from the provided hint.
408 if (!result.eliminateEndComponents) {
409 extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, result.uniqueSolution);
410 } else {
411 if (hint.isEmpty()) {
412 STORM_LOG_TRACE("Warn A non-empty hint was provided, but its information will be disregarded.");
413 }
414 }
415
416 // Only set bounds if we did not obtain them from the hint.
417 if (!result.hasLowerResultBound()) {
418 result.lowerResultBound = storm::utility::zero<SolutionType>();
419 }
421 result.upperResultBound = storm::utility::one<SolutionType>();
422 }
423
424 // If we received an upper bound, we can drop the requirement to compute one.
425 if (result.hasUpperResultBound()) {
426 result.computeUpperBounds = false;
427 }
428
429 return result;
430}
431
432template<typename ValueType>
434 MaybeStateResult(std::vector<ValueType>&& values) : values(std::move(values)) {
435 // Intentionally left empty.
436 }
437
438 bool hasScheduler() const {
439 return static_cast<bool>(scheduler);
440 }
441
442 std::vector<uint64_t> const& getScheduler() const {
443 return scheduler.get();
444 }
445
446 std::vector<ValueType> const& getValues() const {
447 return values;
448 }
449
450 std::vector<ValueType> values;
451 boost::optional<std::vector<uint64_t>> scheduler;
452};
453
454template<typename ValueType, typename SolutionType>
456 storm::storage::SparseMatrix<ValueType>&& submatrix, std::vector<ValueType> const& b,
457 bool produceScheduler, SparseMdpHintType<SolutionType>& hint) {
458 // Initialize the solution vector.
459 std::vector<SolutionType> x =
460 hint.hasValueHint() ? std::move(hint.getValueHint())
461 : std::vector<SolutionType>(submatrix.getRowGroupCount(),
462 hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero<SolutionType>());
463
464 // Set up the solver.
466 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType, SolutionType>> solver =
467 storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
468 solver->setRequirementsChecked();
469 solver->setUncertaintyIsRobust(goal.isRobust());
470 solver->setHasUniqueSolution(hint.hasUniqueSolution());
471 solver->setHasNoEndComponents(hint.hasNoEndComponents());
472 if (hint.hasLowerResultBound()) {
473 solver->setLowerBound(hint.getLowerResultBound());
474 }
475 if (hint.hasUpperResultBound()) {
476 solver->setUpperBound(hint.getUpperResultBound());
477 }
478 if (hint.hasUpperResultBounds()) {
479 solver->setUpperBounds(std::move(hint.getUpperResultBounds()));
480 }
481 if (hint.hasSchedulerHint()) {
482 solver->setInitialScheduler(std::move(hint.getSchedulerHint()));
483 }
484 solver->setTrackScheduler(produceScheduler);
485
486 // Solve the corresponding system of equations.
487 solver->solveEquations(env, x, b);
488
489#ifndef NDEBUG
490 // As a sanity check, make sure our local upper bounds were in fact correct.
492 uint64_t relevantState = solver->hasRelevantValues() ? solver->getRelevantValues().getNextSetIndex(0ull) : 0ull;
493 std::function<void()> getNextRelevantStateIndex;
494 if (solver->hasRelevantValues()) {
495 storm::storage::BitVector const& relevantValues = solver->getRelevantValues();
496 getNextRelevantStateIndex = [&relevantState, &relevantValues]() { relevantState = relevantValues.getNextSetIndex(++relevantState); };
497 } else {
498 getNextRelevantStateIndex = [&relevantState]() { ++relevantState; };
499 }
500 for (; relevantState < solver->getUpperBounds().size(); getNextRelevantStateIndex()) {
501 STORM_LOG_ASSERT(x.at(relevantState) <=
502 solver->getUpperBounds().at(relevantState) + storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision()),
503 "Expecting result value for state " << relevantState << " to be <= " << solver->getUpperBounds().at(relevantState) << ", but got "
504 << x.at(relevantState) << ".");
505 }
506 }
507#endif
508
509 // Create result.
510 MaybeStateResult<SolutionType> result(std::move(x));
511
512 // If requested, return the requested scheduler.
513 if (produceScheduler) {
514 result.scheduler = std::move(solver->getSchedulerChoices());
515 }
516 return result;
517}
518
524
525template<typename ValueType>
528 result.maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
529
530 // Treat the states with probability zero/one.
531 std::vector<ValueType> const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
534 storm::storage::BitVector nonMaybeStates = ~result.maybeStates;
535 for (auto state : nonMaybeStates) {
536 if (storm::utility::isOne(resultsForNonMaybeStates[state])) {
537 result.statesWithProbability1.set(state, true);
538 } else {
539 STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException,
540 "Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
541 result.statesWithProbability0.set(state, true);
542 }
543 }
544
545 return result;
546}
547
548template<typename ValueType, typename SolutionType>
550 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
551 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
552 storm::storage::BitVector const& phiStates,
553 storm::storage::BitVector const& psiStates) {
555
556 // Get all states that have probability 0 and 1 of satisfying the until-formula.
557 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
558 if (goal.minimize()) {
559 statesWithProbability01 =
560 storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
561 } else {
562 statesWithProbability01 =
563 storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
564 }
565 result.statesWithProbability0 = std::move(statesWithProbability01.first);
566 result.statesWithProbability1 = std::move(statesWithProbability01.second);
568
569 return result;
570}
571
572template<typename ValueType, typename SolutionType>
574 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
575 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
576 storm::storage::BitVector const& phiStates,
577 storm::storage::BitVector const& psiStates, ModelCheckerHint const& hint) {
578 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
579 return getQualitativeStateSetsUntilProbabilitiesFromHint<ValueType>(hint);
580 } else {
581 return computeQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates);
582 }
583}
584
585template<typename SolutionType, bool subChoicesCoverOnlyMaybeStates = true>
586void extractSchedulerChoices(storm::storage::Scheduler<SolutionType>& scheduler, std::vector<uint64_t> const& subChoices,
587 storm::storage::BitVector const& maybeStates) {
588 if constexpr (subChoicesCoverOnlyMaybeStates) {
589 auto subChoiceIt = subChoices.begin();
590 for (auto maybeState : maybeStates) {
591 scheduler.setChoice(*subChoiceIt, maybeState);
592 ++subChoiceIt;
593 }
594 assert(subChoiceIt == subChoices.end());
595 } else {
596 // See computeFixedPointSystemUntilProbabilities, where we create a different equation system.
597 // Consequentially, we run a slightly different code here for interval-based models.
598 STORM_LOG_ASSERT(maybeStates.size() == subChoices.size(), "Sizes do not coincide.");
599 for (auto maybeState : maybeStates) {
600 scheduler.setChoice(subChoices[maybeState], maybeState);
601 }
602 }
603}
604
605template<typename ValueType, typename SolutionType>
607 QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
608 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates,
609 storm::storage::BitVector const& psiStates) {
610 // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
611 // the states with probability 1 or 0 (depending on whether we maximize or minimize).
612 // We also need to define some arbitrary choice for the remaining states to obtain a fully defined scheduler.
613 if (goal.minimize()) {
614 storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.statesWithProbability0, transitionMatrix, scheduler);
615 for (auto prob1State : qualitativeStateSets.statesWithProbability1) {
616 scheduler.setChoice(0, prob1State);
617 }
618 } else {
619 storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates,
620 scheduler);
621 for (auto prob0State : qualitativeStateSets.statesWithProbability0) {
622 scheduler.setChoice(0, prob0State);
623 }
624 }
625}
626
627template<typename ValueType, typename SolutionType>
629 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
630 QualitativeStateSetsUntilProbabilities const& qualitativeStateSets,
631 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b) {
632 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
633 // For non-interval based models, we can eliminate the rows and columns from the original transition probability matrix for states
634 // whose probabilities are already known... However, there is information in the transition to those states.
635 // Thus, we cannot eliminate them all.
636 // We can however drop all the outgoing transitions from these states.
637 // TODO: we can drop more than those entries and actually remove many states (all but the ones reachable in one step from the maybe states),
638 // TODO ctned: however, there is quite some bookkeeping involved in projecting the right vectors.
639 // TODO ctned: Instead is likely easier to just do a pass and make a unique sink and a unique target state.
640 // TODO ctned: If this is ever changed, extractSchedulerChoices must also be updated.
641 submatrix = transitionMatrix.filterEntries(transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates));
642
643 // Prepare the right-hand side of the equation system. For entry i this corresponds to
644 // the accumulated probability of going from state i to some state that has probability 1.
645 storm::utility::vector::setAllValues(b, transitionMatrix.getRowFilter(qualitativeStateSets.statesWithProbability1));
646 } else {
647 // First, we can eliminate the rows and columns from the original transition probability matrix for states
648 // whose probabilities are already known.
649 submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false);
650
651 // Prepare the right-hand side of the equation system. For entry i this corresponds to
652 // the accumulated probability of going from state i to some state that has probability 1.
653 b = transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.statesWithProbability1);
654 }
655 // If the solve goal has relevant values, we need to adjust them.
656 goal.restrictRelevantValues(qualitativeStateSets.maybeStates);
657}
658
659template<typename ValueType, typename SolutionType>
660boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(
662 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets,
663 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, bool produceScheduler) {
664 // Get the set of states that (under some scheduler) can stay in the set of maybestates forever
666 transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates);
667
668 bool doDecomposition = !candidateStates.empty();
669
671 if (doDecomposition) {
672 // Compute the states that are in MECs.
673 endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(transitionMatrix, backwardTransitions, candidateStates);
674 STORM_LOG_INFO(endComponentDecomposition.statistics(transitionMatrix.getRowGroupCount()));
675 }
676
677 // Only do more work if there are actually end-components.
678 if (doDecomposition && !endComponentDecomposition.empty()) {
679 STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s).");
681 endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr,
682 submatrix, &b, nullptr, produceScheduler);
683
684 // If the solve goal has relevant values, we need to adjust them.
685 if (goal.hasRelevantValues()) {
686 storm::storage::BitVector newRelevantValues(submatrix.getRowGroupCount());
687 for (auto state : goal.relevantValues()) {
688 if (qualitativeStateSets.maybeStates.get(state)) {
689 newRelevantValues.set(result.getRowGroupAfterElimination(state));
690 }
691 }
692 if (!newRelevantValues.empty()) {
693 goal.setRelevantValues(std::move(newRelevantValues));
694 }
695 }
696
697 return result;
698 } else {
699 STORM_LOG_DEBUG("Not eliminating ECs as there are none.");
700 computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b);
701
702 return boost::none;
703 }
704}
705
706template<typename ValueType, typename SolutionType>
709 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates,
710 bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) {
711 STORM_LOG_THROW(!qualitative || !produceScheduler, storm::exceptions::InvalidSettingsException,
712 "Cannot produce scheduler when performing qualitative model checking only.");
713
714 // Prepare resulting vector.
715 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
716
717 // We need to identify the maybe states (states which have a probability for satisfying the until formula
718 // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively.
719 QualitativeStateSetsUntilProbabilities qualitativeStateSets =
720 getQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, hint);
721
722 STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.statesWithProbability1.getNumberOfSetBits() << " states with probability 1, "
723 << qualitativeStateSets.statesWithProbability0.getNumberOfSetBits() << " with probability 0 ("
724 << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
725
726 // Set values of resulting vector that are known exactly.
727 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.statesWithProbability1, storm::utility::one<SolutionType>());
728
729 // Check if the values of the maybe states are relevant for the SolveGoal
730 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
731
732 // If requested, we will produce a scheduler.
733 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
734 if (produceScheduler) {
735 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.getRowGroupCount());
736 // If maybeStatesNotRelevant is true, we have to set the scheduler for maybe states as "dontCare"
737 if (maybeStatesNotRelevant) {
738 for (auto state : qualitativeStateSets.maybeStates) {
739 scheduler->setDontCare(state);
740 }
741 }
742 }
743
744 // Check whether we need to compute exact probabilities for some states.
745 if (qualitative || maybeStatesNotRelevant) {
746 // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
747 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, storm::utility::convertNumber<SolutionType>(0.5));
748 } else {
749 if (!qualitativeStateSets.maybeStates.empty()) {
750 // In this case we have have to compute the remaining probabilities.
751
752 // Obtain proper hint information either from the provided hint or from requirements of the solver.
753 SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
754 env, SemanticSolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
755 phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler);
756
757 // Declare the components of the equation system we will solve.
759 std::vector<ValueType> b;
760
761 // If the hint information tells us that we have to eliminate MECs, we do so now.
762 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
763 if (hintInformation.getEliminateEndComponents()) {
764 ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions,
765 qualitativeStateSets, submatrix, b, produceScheduler);
766 } else {
767 // Otherwise, we compute the standard equations.
768 computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b);
769 }
770
771 // Now compute the results for the maybe states.
772 MaybeStateResult<SolutionType> resultForMaybeStates =
773 computeValuesForMaybeStates(env, std::move(goal), std::move(submatrix), b, produceScheduler, hintInformation);
774
775 // If we eliminated end components, we need to extract the result differently.
776 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
777 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
778 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support this end component with interval models.");
779 } else {
780 ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
781 if (produceScheduler) {
782 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions,
783 resultForMaybeStates.getScheduler());
784 }
785 }
786 } else {
787 // Set values of resulting vector according to result.
788 if constexpr (!std::is_same_v<ValueType, storm::Interval>) {
789 // For non-interval models, we only operated on the maybe states, and we must recover the qualitative values for the other state.
790 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
791 } else {
792 // For interval models, the result for maybe states indeed also holds values for all qualitative states.
793 STORM_LOG_ASSERT(resultForMaybeStates.getValues().size() == transitionMatrix.getColumnCount(), "Dimensions do not match");
794 result = resultForMaybeStates.getValues();
795 }
796 if (produceScheduler) {
797 extractSchedulerChoices<SolutionType, !std::is_same_v<ValueType, storm::Interval>>(*scheduler, resultForMaybeStates.getScheduler(),
798 qualitativeStateSets.maybeStates);
799 }
800 }
801 }
802 }
803
804 // Extend scheduler with choices for the states in the qualitative state sets.
805 if (produceScheduler) {
806 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, phiStates, psiStates);
807 }
808
809 // Sanity check for created scheduler.
810 STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained.");
811 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler");
812 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler");
813 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler");
814
815 // Return result.
816 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result), std::move(scheduler));
817}
818
819template<typename ValueType, typename SolutionType>
822 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler,
823 bool useMecBasedTechnique) {
824 if (useMecBasedTechnique) {
825 // TODO: does this really work for minimizing objectives?
826 storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(transitionMatrix, backwardTransitions, psiStates);
827 storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount());
828 for (auto const& mec : mecDecomposition) {
829 for (auto const& stateActionsPair : mec) {
830 statesInPsiMecs.set(stateActionsPair.first, true);
831 }
832 }
833
834 return computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative,
835 produceScheduler);
836 } else {
837 goal.oneMinus();
838 auto result =
839 computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions,
840 storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, produceScheduler);
841 for (auto& element : result.values) {
842 element = storm::utility::one<SolutionType>() - element;
843 }
844 return result;
845 }
846}
847
848template<typename ValueType, typename SolutionType>
849template<typename RewardModelType>
852 RewardModelType const& rewardModel, uint_fast64_t stepCount) {
853 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
854 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support instantenous rewards with interval models.");
855 } else {
856 // Only compute the result if the model has a state-based reward this->getModel().
857 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
858 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
859 // Initialize result to state rewards of the this->getModel().
860 std::vector<SolutionType> result(rewardModel.getStateRewardVector());
861
862 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
863 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, nullptr, stepCount);
864
865 return result;
866 }
867}
868
869template<typename ValueType, typename SolutionType>
870template<typename RewardModelType>
873 RewardModelType const& rewardModel, uint_fast64_t stepBound) {
874 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
875 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support cumulative rewards with interval models.");
876 } else {
877 // Only compute the result if the model has at least one reward this->getModel().
878 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
879
880 // Compute the reward vector to add in each step based on the available reward models.
881 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
882
883 // Initialize result to the zero vector.
884 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
885
886 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
887 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound);
888
889 return result;
890 }
891}
892
893template<typename ValueType, typename SolutionType>
894template<typename RewardModelType>
897 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, bool produceScheduler,
898 ModelCheckerHint const& hint) {
899 STORM_LOG_THROW(!rewardModel.hasNegativeRewards(), storm::exceptions::NotImplementedException,
900 "The reward model contains negative rewards. This is not implemented by the total rewards computation.");
901 // Reduce to reachability rewards
902 if (goal.minimize()) {
903 // Identify the states from which no reward can be collected under some scheduler
904 storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix);
905 storm::storage::BitVector statesWithZeroRewardChoice(transitionMatrix.getRowGroupCount(), false);
906 for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) {
907 if (choicesWithoutReward.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]) < transitionMatrix.getRowGroupIndices()[state + 1]) {
908 statesWithZeroRewardChoice.set(state);
909 }
910 }
911 storm::storage::BitVector rew0EStates =
912 storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions,
913 statesWithZeroRewardChoice, ~statesWithZeroRewardChoice, false, 0, choicesWithoutReward);
914 rew0EStates.complement();
915 auto result = computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0EStates, qualitative,
916 produceScheduler, hint);
917 if (result.scheduler) {
918 storm::utility::graph::computeSchedulerStayingInStates(rew0EStates, transitionMatrix, *result.scheduler, choicesWithoutReward);
919 }
920 return result;
921 } else {
922 // Identify the states from which only states with zero reward are reachable.
923 storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix);
924 storm::storage::BitVector rew0AStates = storm::utility::graph::performProbGreater0E(backwardTransitions, statesWithoutReward, ~statesWithoutReward);
925 rew0AStates.complement();
926
927 // There might be end components that consists only of states/choices with zero rewards. The reachability reward semantics would assign such
928 // end components reward infinity. To avoid this, we potentially need to eliminate such end components
929 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
930 if (storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, rew0AStates)
931 .full()) {
932 return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0AStates, qualitative,
933 produceScheduler, hint);
934 } else {
935 // The transformation of schedulers for the ec-eliminated system back to the original one is not implemented.
936 STORM_LOG_ERROR_COND(!produceScheduler, "Can not produce scheduler for this property (functionality not implemented");
937 storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix);
939 transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), choicesWithoutReward, rew0AStates, true);
940 storm::storage::BitVector newRew0AStates(ecElimResult.matrix.getRowGroupCount(), false);
941 for (auto oldRew0AState : rew0AStates) {
942 newRew0AStates.set(ecElimResult.oldToNewStateMapping[oldRew0AState]);
943 }
944
945 if (goal.hasRelevantValues()) {
946 storm::storage::BitVector newRelevantValues(ecElimResult.matrix.getRowGroupCount(), false);
947 for (auto oldRelevantState : goal.relevantValues()) {
948 newRelevantValues.set(ecElimResult.oldToNewStateMapping[oldRelevantState]);
949 }
950 goal.relevantValues() = std::move(newRelevantValues);
951 }
952
953 MDPSparseModelCheckingHelperReturnType<SolutionType> result = computeReachabilityRewardsHelper(
954 env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(true),
955 [&](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix, storm::storage::BitVector const& maybeStates) {
956 std::vector<ValueType> result;
957 std::vector<ValueType> oldChoiceRewards = rewardModel.getTotalRewardVector(transitionMatrix);
958 result.reserve(rowCount);
959 for (uint64_t newState : maybeStates) {
960 for (auto newChoice : newTransitionMatrix.getRowGroupIndices(newState)) {
961 uint64_t oldChoice = ecElimResult.newToOldRowMapping[newChoice];
962 result.push_back(oldChoiceRewards[oldChoice]);
963 }
964 }
965 STORM_LOG_ASSERT(result.size() == rowCount, "Unexpected size of reward vector.");
966 return result;
967 },
968 newRew0AStates, qualitative, false,
969 [&]() {
970 storm::storage::BitVector newStatesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false);
971 for (auto oldStateWithoutRew : statesWithoutReward) {
972 newStatesWithoutReward.set(ecElimResult.oldToNewStateMapping[oldStateWithoutRew]);
973 }
974 return newStatesWithoutReward;
975 },
976 [&]() {
977 storm::storage::BitVector newChoicesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false);
978 for (uint64_t newChoice = 0; newChoice < ecElimResult.matrix.getRowCount(); ++newChoice) {
979 if (choicesWithoutReward.get(ecElimResult.newToOldRowMapping[newChoice])) {
980 newChoicesWithoutReward.set(newChoice);
981 }
982 }
983 return newChoicesWithoutReward;
984 });
985
986 std::vector<SolutionType> resultInEcQuotient = std::move(result.values);
987 result.values.resize(ecElimResult.oldToNewStateMapping.size());
988 storm::utility::vector::selectVectorValues(result.values, ecElimResult.oldToNewStateMapping, resultInEcQuotient);
989 return result;
990 }
991 }
992}
993
994template<typename ValueType, typename SolutionType>
995template<typename RewardModelType>
998 RewardModelType const& rewardModel, uint_fast64_t stepBound, ValueType discountFactor) {
999 // Only compute the result if the model has at least one reward this->getModel().
1000 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
1001
1002 // Compute the reward vector to add in each step based on the available reward models.
1003 std::vector<SolutionType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
1004
1005 // Initialize result to the zero vector.
1006 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
1007
1008 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
1009 multiplier->repeatedMultiplyAndReduceWithFactor(env, goal.direction(), result, &totalRewardVector, stepBound, discountFactor);
1010
1011 return result;
1012}
1013
1014template<typename ValueType, typename SolutionType>
1015template<typename RewardModelType>
1018 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, bool produceScheduler,
1019 ValueType discountFactor, ModelCheckerHint const& hint) {
1020 // If the solver is set to force exact results, throw an error
1021 STORM_LOG_THROW(!env.solver().isForceExact(), storm::exceptions::NotSupportedException,
1022 "Exact solving of discounted total reward objectives is currently not supported.");
1023
1024 std::vector<ValueType> b;
1025
1026 std::vector<SolutionType> x = std::vector<SolutionType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
1027 b = rewardModel.getTotalRewardVector(transitionMatrix);
1028 storm::modelchecker::helper::DiscountingHelper<ValueType> discountingHelper(transitionMatrix, discountFactor, produceScheduler);
1029
1030 discountingHelper.solveWithDiscountedValueIteration(env, goal.direction(), x, b);
1031
1032 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
1033 if (produceScheduler) {
1034 scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(discountingHelper.computeScheduler());
1035 }
1036 STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained.");
1037 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler");
1038 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler");
1039 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler");
1040 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(x), std::move(scheduler));
1041}
1042
1043template<typename ValueType, typename SolutionType>
1044template<typename RewardModelType>
1047 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates,
1048 bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) {
1049 // Only compute the result if the model has at least one reward this->getModel().
1050 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Reward model for formula is empty. Skipping formula.");
1051 return computeReachabilityRewardsHelper(
1052 env, std::move(goal), transitionMatrix, backwardTransitions,
1053 [&rewardModel](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
1054 return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
1055 },
1056 targetStates, qualitative, produceScheduler, [&]() { return rewardModel.getStatesWithZeroReward(transitionMatrix); },
1057 [&]() { return rewardModel.getChoicesWithZeroReward(transitionMatrix); }, hint);
1058}
1059
1060template<typename ValueType, typename SolutionType>
1063 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler,
1064 ModelCheckerHint const& hint) {
1065 return computeReachabilityRewardsHelper(
1066 env, std::move(goal), transitionMatrix, backwardTransitions,
1067 [](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&) {
1068 return std::vector<ValueType>(rowCount, storm::utility::one<ValueType>());
1069 },
1070 targetStates, qualitative, produceScheduler, [&]() { return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); },
1071 [&]() { return storm::storage::BitVector(transitionMatrix.getRowCount(), false); }, hint);
1072}
1073
1074#ifdef STORM_HAVE_CARL
1075template<typename ValueType, typename SolutionType>
1079 bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative) {
1080 // Only compute the result if the reward model is not empty.
1081 STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
1082 return computeReachabilityRewardsHelper(
1083 env, std::move(goal), transitionMatrix, backwardTransitions,
1084 [&](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
1085 std::vector<ValueType> result;
1086 result.reserve(rowCount);
1087 std::vector<storm::Interval> subIntervalVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
1088 for (auto const& interval : subIntervalVector) {
1089 result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper());
1090 }
1091 return result;
1092 },
1093 targetStates, qualitative, false,
1094 [&]() {
1095 return intervalRewardModel.getStatesWithFilter(
1096 transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); });
1097 },
1098 [&]() {
1099 return intervalRewardModel.getChoicesWithFilter(
1100 transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); });
1101 })
1102 .values;
1103}
1104
1105template<>
1106std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(
1109 storm::storage::BitVector const&, bool) {
1110 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Computing reachability rewards is unsupported for this data type.");
1111}
1112#endif
1113
1119
1120template<typename ValueType>
1122 storm::storage::BitVector const& targetStates) {
1124 result.maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
1125
1126 // Treat the states with reward zero/infinity.
1127 std::vector<ValueType> const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
1130 storm::storage::BitVector nonMaybeStates = ~result.maybeStates;
1131 for (auto state : nonMaybeStates) {
1132 if (storm::utility::isZero(resultsForNonMaybeStates[state])) {
1133 result.rewardZeroStates.set(state, true);
1134 } else {
1135 STORM_LOG_THROW(storm::utility::isInfinity(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException,
1136 "Expected that the result hint specifies probabilities in {0,infinity} for non-maybe states");
1137 result.infinityStates.set(state, true);
1138 }
1139 }
1140 return result;
1141}
1142
1143template<typename ValueType, typename SolutionType>
1146 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates,
1147 std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
1149 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
1150 if (goal.minimize()) {
1151 result.infinityStates =
1152 storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates);
1153 } else {
1154 result.infinityStates =
1155 storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates);
1156 }
1157 result.infinityStates.complement();
1158
1159 if (storm::settings::getModule<storm::settings::modules::ModelCheckerSettings>().isFilterRewZeroSet()) {
1160 if (goal.minimize()) {
1161 result.rewardZeroStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions,
1162 trueStates, targetStates, zeroRewardChoicesGetter());
1163 } else {
1164 result.rewardZeroStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions,
1165 zeroRewardStatesGetter(), targetStates);
1166 }
1167 } else {
1168 result.rewardZeroStates = targetStates;
1169 }
1170 result.maybeStates = ~(result.rewardZeroStates | result.infinityStates);
1171 return result;
1172}
1173
1174template<typename ValueType, typename SolutionType>
1176 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
1177 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
1178 storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint,
1179 std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter,
1180 std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
1181 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
1182 return getQualitativeStateSetsReachabilityRewardsFromHint<ValueType>(hint, targetStates);
1183 } else {
1184 return computeQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, zeroRewardStatesGetter,
1185 zeroRewardChoicesGetter);
1186 }
1187}
1188
1189template<typename ValueType, typename SolutionType>
1191 QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
1192 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates,
1193 std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
1194 // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
1195 // the states with reward zero/infinity.
1196 if (goal.minimize()) {
1197 storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.rewardZeroStates, transitionMatrix, backwardTransitions,
1198 qualitativeStateSets.rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter());
1199 for (auto state : qualitativeStateSets.infinityStates) {
1200 scheduler.setChoice(0, state);
1201 }
1202 } else {
1203 storm::utility::graph::computeSchedulerRewInf(qualitativeStateSets.infinityStates, transitionMatrix, backwardTransitions, scheduler);
1204 for (auto state : qualitativeStateSets.rewardZeroStates) {
1205 scheduler.setChoice(0, state);
1206 }
1207 }
1208}
1209
1210template<typename ValueType, typename SolutionType>
1212 std::vector<uint_fast64_t> const& subChoices, storm::storage::BitVector const& maybeStates,
1213 boost::optional<storm::storage::BitVector> const& selectedChoices) {
1214 auto subChoiceIt = subChoices.begin();
1215 if (selectedChoices) {
1216 for (auto maybeState : maybeStates) {
1217 // find the rowindex that corresponds to the selected row of the submodel
1218 uint_fast64_t firstRowIndex = transitionMatrix.getRowGroupIndices()[maybeState];
1219 uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex);
1220 for (uint_fast64_t choice = 0; choice < *subChoiceIt; ++choice) {
1221 selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1);
1222 }
1223 scheduler.setChoice(selectedRowIndex - firstRowIndex, maybeState);
1224 ++subChoiceIt;
1225 }
1226 } else {
1227 for (auto maybeState : maybeStates) {
1228 scheduler.setChoice(*subChoiceIt, maybeState);
1229 ++subChoiceIt;
1230 }
1231 }
1232 assert(subChoiceIt == subChoices.end());
1233}
1234
1235template<typename ValueType, typename SolutionType>
1238 QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional<storm::storage::BitVector> const& selectedChoices,
1239 std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const&
1240 totalStateRewardVectorGetter,
1241 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, std::vector<ValueType>* oneStepTargetProbabilities = nullptr) {
1242 // Remove rows and columns from the original transition probability matrix for states whose reward values are already known.
1243 // If there are infinity states, we additionally have to remove choices of maybeState that lead to infinity.
1244 if (qualitativeStateSets.infinityStates.empty()) {
1245 submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false);
1246 b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, qualitativeStateSets.maybeStates);
1247 if (oneStepTargetProbabilities) {
1248 (*oneStepTargetProbabilities) =
1249 transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.rewardZeroStates);
1250 }
1251 } else {
1252 submatrix = transitionMatrix.getSubmatrix(false, *selectedChoices, qualitativeStateSets.maybeStates, false);
1253 b = totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix,
1254 storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true));
1256 if (oneStepTargetProbabilities) {
1257 (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowSumVector(*selectedChoices, qualitativeStateSets.rewardZeroStates);
1258 }
1259 }
1260
1261 // If the solve goal has relevant values, we need to adjust them.
1262 goal.restrictRelevantValues(qualitativeStateSets.maybeStates);
1263}
1264
1265template<typename ValueType, typename SolutionType>
1266boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(
1268 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets,
1269 boost::optional<storm::storage::BitVector> const& selectedChoices,
1270 std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const&
1271 totalStateRewardVectorGetter,
1272 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, boost::optional<std::vector<ValueType>>& oneStepTargetProbabilities,
1273 bool produceScheduler) {
1274 // Start by computing the choices with reward 0, as we only want ECs within this fragment.
1275 storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount());
1276
1277 // Get the rewards of all choices.
1278 std::vector<ValueType> rewardVector =
1279 totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true));
1280
1281 uint64_t index = 0;
1282 for (auto const& e : rewardVector) {
1283 if (storm::utility::isZero(e)) {
1284 zeroRewardChoices.set(index);
1285 }
1286 ++index;
1287 }
1288
1289 // Compute the states that have some zero reward choice.
1290 storm::storage::BitVector candidateStates(qualitativeStateSets.maybeStates);
1291 for (auto state : qualitativeStateSets.maybeStates) {
1292 bool keepState = false;
1293
1294 for (auto row = transitionMatrix.getRowGroupIndices()[state], rowEnd = transitionMatrix.getRowGroupIndices()[state + 1]; row < rowEnd; ++row) {
1295 if (zeroRewardChoices.get(row)) {
1296 keepState = true;
1297 break;
1298 }
1299 }
1300
1301 if (!keepState) {
1302 candidateStates.set(state, false);
1303 }
1304 }
1305
1306 // Only keep the candidate states that (under some scheduler) can stay in the set of candidates forever
1307 candidateStates =
1308 storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates);
1309
1310 bool doDecomposition = !candidateStates.empty();
1311
1313 if (doDecomposition) {
1314 // Then compute the states that are in MECs with zero reward.
1315 endComponentDecomposition =
1316 storm::storage::MaximalEndComponentDecomposition<ValueType>(transitionMatrix, backwardTransitions, candidateStates, zeroRewardChoices);
1317 STORM_LOG_INFO(endComponentDecomposition.statistics(transitionMatrix.getRowGroupCount()));
1318 }
1319
1320 // Only do more work if there are actually end-components.
1321 if (doDecomposition && !endComponentDecomposition.empty()) {
1322 STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs.");
1324 endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates,
1325 oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector,
1326 submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler);
1327
1328 // If the solve goal has relevant values, we need to adjust them.
1329 if (goal.hasRelevantValues()) {
1330 storm::storage::BitVector newRelevantValues(submatrix.getRowGroupCount());
1331 for (auto state : goal.relevantValues()) {
1332 if (qualitativeStateSets.maybeStates.get(state)) {
1333 newRelevantValues.set(result.getRowGroupAfterElimination(state));
1334 }
1335 }
1336 if (!newRelevantValues.empty()) {
1337 goal.setRelevantValues(std::move(newRelevantValues));
1338 }
1339 }
1340
1341 return result;
1342 } else {
1343 STORM_LOG_DEBUG("Not eliminating ECs as there are none.");
1344 computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b,
1345 oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
1346 return boost::none;
1347 }
1348}
1349
1350template<typename ValueType, typename SolutionType>
1352 storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& choiceRewards,
1353 std::vector<ValueType> const& oneStepTargetProbabilities) {
1354 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1355 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing upper reward bounds with interval models.");
1356 } else {
1357 // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
1358 if (direction == storm::OptimizationDirection::Minimize) {
1359 DsMpiMdpUpperRewardBoundsComputer<ValueType> dsmpi(submatrix, choiceRewards, oneStepTargetProbabilities);
1360 hintInformation.upperResultBounds = dsmpi.computeUpperBounds();
1361 } else {
1362 BaierUpperRewardBoundsComputer<ValueType> baier(submatrix, choiceRewards, oneStepTargetProbabilities);
1363 hintInformation.upperResultBound = baier.computeUpperBound();
1364 }
1365 }
1366}
1367
1368template<typename ValueType, typename SolutionType>
1369MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeReachabilityRewardsHelper(
1371 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
1372 std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const&
1373 totalStateRewardVectorGetter,
1374 storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler,
1375 std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter,
1376 ModelCheckerHint const& hint) {
1377 // Prepare resulting vector.
1378 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
1379
1380 // Determine which states have a reward that is infinity or less than infinity.
1381 QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(
1382 goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter);
1383
1384 STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() << " states with reward infinity, "
1385 << qualitativeStateSets.rewardZeroStates.getNumberOfSetBits() << " states with reward zero ("
1386 << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
1387
1388 storm::utility::vector::setVectorValues(result, qualitativeStateSets.infinityStates, storm::utility::infinity<SolutionType>());
1389
1390 // If requested, we will produce a scheduler.
1391 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
1392 if (produceScheduler) {
1393 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1394 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support producing schedulers in this function with interval models.");
1395 } else {
1396 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.getRowGroupCount());
1397 }
1398 }
1399
1400 // Check if the values of the maybe states are relevant for the SolveGoal
1401 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
1402
1403 // Check whether we need to compute exact rewards for some states.
1404 if (qualitative || maybeStatesNotRelevant) {
1405 STORM_LOG_INFO("The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
1406 // Set the values for all maybe-states to 1 to indicate that their reward values
1407 // are neither 0 nor infinity.
1408 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, storm::utility::one<SolutionType>());
1409 } else {
1410 if (!qualitativeStateSets.maybeStates.empty()) {
1411 // In this case we have to compute the reward values for the remaining states.
1412
1413 // Store the choices that lead to non-infinity values. If none, all choices im maybe states can be selected.
1414 boost::optional<storm::storage::BitVector> selectedChoices;
1415 if (!qualitativeStateSets.infinityStates.empty()) {
1416 selectedChoices = transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates, ~qualitativeStateSets.infinityStates);
1417 }
1418
1419 // Obtain proper hint information either from the provided hint or from requirements of the solver.
1420 SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
1421 env, SemanticSolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
1422 ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, produceScheduler, selectedChoices);
1423
1424 // Declare the components of the equation system we will solve.
1426 std::vector<ValueType> b;
1427
1428 // If we need to compute upper bounds on the reward values, we need the one step probabilities
1429 // to a target state.
1430 boost::optional<std::vector<ValueType>> oneStepTargetProbabilities;
1431 if (hintInformation.getComputeUpperBounds()) {
1432 oneStepTargetProbabilities = std::vector<ValueType>();
1433 }
1434
1435 // If the hint information tells us that we have to eliminate MECs, we do so now.
1436 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
1437 if (hintInformation.getEliminateEndComponents()) {
1438 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1439 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models.");
1440 } else {
1442 goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b,
1443 oneStepTargetProbabilities, produceScheduler);
1444 }
1445 } else {
1446 // Otherwise, we compute the standard equations.
1447 computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter,
1448 submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
1449 }
1450
1451 // If we need to compute upper bounds, do so now.
1452 if (hintInformation.getComputeUpperBounds()) {
1453 STORM_LOG_ASSERT(oneStepTargetProbabilities, "Expecting one step target probability vector to be available.");
1454 computeUpperRewardBounds(hintInformation, goal.direction(), submatrix, b, oneStepTargetProbabilities.get());
1455 }
1456
1457 // Now compute the results for the maybe states.
1458 MaybeStateResult<SolutionType> resultForMaybeStates =
1459 computeValuesForMaybeStates(env, std::move(goal), std::move(submatrix), b, produceScheduler, hintInformation);
1460
1461 // If we eliminated end components, we need to extract the result differently.
1462 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
1463 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1464 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models.");
1465 } else {
1466 ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1467 if (produceScheduler) {
1468 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions,
1469 resultForMaybeStates.getScheduler());
1470 }
1471 }
1472 } else {
1473 // Set values of resulting vector according to result.
1474 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1475 if (produceScheduler) {
1476 extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates,
1477 selectedChoices);
1478 }
1479 }
1480 }
1481 }
1482
1483 // Extend scheduler with choices for the states in the qualitative state sets.
1484 if (produceScheduler) {
1485 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter);
1486 }
1487
1488 // Sanity check for created scheduler.
1489 STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained.");
1490 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler");
1491 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler");
1492 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler");
1493
1494 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1495 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result));
1496 } else {
1497 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result), std::move(scheduler));
1498 }
1499}
1500
1501template class SparseMdpPrctlHelper<double>;
1502template std::vector<double> SparseMdpPrctlHelper<double>::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<double>&& goal,
1503 storm::storage::SparseMatrix<double> const& transitionMatrix,
1505 uint_fast64_t stepCount);
1506template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<double>&& goal,
1507 storm::storage::SparseMatrix<double> const& transitionMatrix,
1509 uint_fast64_t stepBound);
1510template std::vector<double> SparseMdpPrctlHelper<double>::computeDiscountedCumulativeRewards(
1511 Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& transitionMatrix,
1512 storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, double discountFactor);
1513template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(
1514 Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& transitionMatrix,
1516 storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint);
1517template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeTotalRewards(
1518 Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& transitionMatrix,
1519 storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, bool qualitative,
1520 bool produceScheduler, ModelCheckerHint const& hint);
1521template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<double>::computeDiscountedTotalRewards(
1522 Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& transitionMatrix,
1523 storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, bool qualitative,
1524 bool produceScheduler, double discountFactor, ModelCheckerHint const& hint);
1525
1526#ifdef STORM_HAVE_CARL
1527template class SparseMdpPrctlHelper<storm::RationalNumber>;
1528template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(
1530 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepCount);
1531template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(
1533 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound);
1534template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeDiscountedCumulativeRewards(
1536 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound, storm::RationalNumber discountFactor);
1537template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(
1539 storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions,
1540 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative,
1541 bool produceScheduler, ModelCheckerHint const& hint);
1542template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeTotalRewards(
1544 storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions,
1545 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, bool qualitative, bool produceScheduler,
1546 ModelCheckerHint const& hint);
1547template MDPSparseModelCheckingHelperReturnType<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeDiscountedTotalRewards(
1549 storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions,
1550 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, bool qualitative, bool produceScheduler,
1551 storm::RationalNumber discountFactor, ModelCheckerHint const& hint);
1552#endif
1553
1554template class SparseMdpPrctlHelper<storm::Interval, double>;
1555template std::vector<double> SparseMdpPrctlHelper<storm::Interval, double>::computeInstantaneousRewards(
1556 Environment const& env, storm::solver::SolveGoal<storm::Interval, double>&& goal, storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix,
1557 storm::models::sparse::StandardRewardModel<storm::Interval> const& rewardModel, uint_fast64_t stepCount);
1558template std::vector<double> SparseMdpPrctlHelper<storm::Interval, double>::computeCumulativeRewards(
1559 Environment const& env, storm::solver::SolveGoal<storm::Interval, double>&& goal, storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix,
1560 storm::models::sparse::StandardRewardModel<storm::Interval> const& rewardModel, uint_fast64_t stepBound);
1561template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<storm::Interval, double>::computeReachabilityRewards(
1562 Environment const& env, storm::solver::SolveGoal<storm::Interval, double>&& goal, storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix,
1564 storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint);
1565template MDPSparseModelCheckingHelperReturnType<double> SparseMdpPrctlHelper<storm::Interval, double>::computeTotalRewards(
1566 Environment const& env, storm::solver::SolveGoal<storm::Interval, double>&& goal, storm::storage::SparseMatrix<storm::Interval> const& transitionMatrix,
1568 bool qualitative, bool produceScheduler, ModelCheckerHint const& hint);
1569
1570} // namespace helper
1571} // namespace modelchecker
1572} // namespace storm
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
void setPrecision(storm::RationalNumber value)
MinMaxSolverEnvironment & minMax()
This class contains information that might accelerate the model checking process.
ExplicitModelCheckerHint< ValueType > & asExplicitModelCheckerHint()
ValueType computeUpperBound()
Computes an upper bound on the expected rewards.
storm::storage::Scheduler< ValueType > computeScheduler() const
Retrieves the generated scheduler.
bool solveWithDiscountedValueIteration(Environment const &env, std::optional< OptimizationDirection > dir, std::vector< ValueType > &x, std::vector< ValueType > const &b) const
std::vector< ValueType > computeUpperBounds()
Computes upper bounds on the expected rewards.
uint64_t getRowGroupAfterElimination(uint64_t state) const
Retrieves the row group of the state after end component elimination.
static SparseMdpEndComponentInformation< ValueType > eliminateEndComponents(storm::storage::MaximalEndComponentDecomposition< ValueType > const &endComponentDecomposition, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const *sumColumns, storm::storage::BitVector const *selectedChoices, std::vector< ValueType > const *summand, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > *columnSumVector, std::vector< ValueType > *summandResultVector, bool gatherExitChoices=false)
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeGloballyProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &psiStates, bool qualitative, bool produceScheduler, bool useMecBasedTechnique=false)
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeTotalRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const &hint=ModelCheckerHint())
static std::vector< SolutionType > computeCumulativeRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepBound)
static std::vector< SolutionType > computeInstantaneousRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepCount)
static std::map< storm::storage::sparse::state_type, SolutionType > computeRewardBoundedValues(Environment const &env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding< ValueType, true > &rewardUnfolding, storm::storage::BitVector const &initialStates)
static std::vector< SolutionType > computeNextProbabilities(Environment const &env, OptimizationDirection dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &nextStates)
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeUntilProbabilities(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool qualitative, bool produceScheduler, ModelCheckerHint const &hint=ModelCheckerHint())
uint64_t getDimensionOfEpoch(Epoch const &epoch, uint64_t const &dimension) const
Epoch getStartEpoch(bool setUnknownDimsToBottom=false)
Retrieves the desired epoch that needs to be analyzed to compute the reward bounded values.
EpochModel< ValueType, SingleObjectiveMode > & setCurrentEpoch(Epoch const &epoch)
std::vector< Epoch > getEpochComputationOrder(Epoch const &startEpoch, bool stopAtComputedEpochs=false)
Computes a sequence of epochs that need to be analyzed to get a result at the start epoch.
ValueType getRequiredEpochModelPrecision(Epoch const &startEpoch, ValueType const &precision)
Returns the precision required for the analyzis of each epoch model in order to achieve the given ove...
boost::optional< ValueType > getUpperObjectiveBound(uint64_t objectiveIndex=0)
Returns an upper/lower bound for the objective result in every state (if this bound could be computed...
bool empty() const
Retrieves whether the reward model is empty, i.e.
std::vector< ValueType > getTotalRewardVector(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix) const
Creates a vector representing the complete reward vector based on the state-, state-action- and trans...
storm::storage::BitVector getChoicesWithFilter(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::function< bool(ValueType const &)> const &filter) const
Returns the set of choices for which all associated rewards (state, action or transition rewards) sat...
storm::storage::BitVector getStatesWithFilter(storm::storage::SparseMatrix< MatrixValueType > const &transitionMatrix, std::function< bool(ValueType const &)> const &filter) const
Returns the set of states for which all associated rewards (state, action or transition rewards) sati...
MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, bool hasUniqueSolution=false, bool hasNoEndComponents=false, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool hasInitialScheduler=false, bool trackScheduler=false) const
Retrieves the requirements of the solver that would be created when calling create() right now.
std::string getEnabledRequirementsAsString() const
Returns a string that enumerates the enabled requirements.
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
bool hasRelevantValues() const
void restrictRelevantValues(storm::storage::BitVector const &filter)
storm::storage::BitVector & relevantValues()
void setRelevantValues(storm::storage::BitVector &&values)
OptimizationDirection direction() const
Definition SolveGoal.cpp:92
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
void complement()
Negates all bits in the bit vector.
uint64_t getNextSetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool isDisjointFrom(BitVector const &other) const
Checks whether none of the bits that are set in the current bit vector are also set in the given bit ...
bool full() const
Retrieves whether all bits are set in this bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
void set(uint64_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(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
bool empty() const
Checks if the decomposition is empty.
std::size_t size() const
Retrieves the number of blocks of this decomposition.
This class represents the decomposition of a nondeterministic model into its maximal end components.
std::string statistics(uint64_t totalNumberOfStates) const
Returns a string containing statistics about the MEC decomposition, e.g., the number of (trivial/non-...
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
SchedulerChoice< ValueType > const & getChoice(uint_fast64_t modelState, uint_fast64_t memoryState=0) const
Gets the choice defined by the scheduler for the given model and memory state.
Definition Scheduler.cpp:86
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.
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 ...
std::vector< value_type > getConstrainedRowSumVector(storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint) const
Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only thos...
SparseMatrix< ValueType > transposeSelectedRowsFromRowGroups(std::vector< uint64_t > const &rowGroupChoices, bool keepZeros=false) const
Transposes the matrix w.r.t.
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
index_type getColumnCount() const
Returns the number of columns of the matrix.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
std::vector< value_type > getConstrainedRowGroupSumVector(storm::storage::BitVector const &rowGroupConstraint, storm::storage::BitVector const &columnConstraint) const
Computes a vector whose entries represent the sums of selected columns for all rows in selected row g...
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 ...
SparseMatrix filterEntries(storm::storage::BitVector const &rowFilter) const
Returns a copy of this matrix that only considers entries in the selected rows.
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)
A class that provides convenience operations to display run times.
bool updateProgress(uint64_t count)
Updates the progress to the current count and prints it if the delay passed.
void setMaxCount(uint64_t maxCount)
Sets the maximal possible count.
void startNewMeasurement(uint64_t startCount)
Starts a new measurement, dropping all progress information collected so far.
A class that provides convenience operations to display run times.
Definition Stopwatch.h:14
void start()
Start stopwatch (again) and start measuring time.
Definition Stopwatch.cpp:48
void stop()
Stop stopwatch and add measured time to total time.
Definition Stopwatch.cpp:42
#define STORM_LOG_INFO(message)
Definition logging.h:24
#define STORM_LOG_WARN(message)
Definition logging.h:25
#define STORM_LOG_DEBUG(message)
Definition logging.h:18
#define STORM_LOG_TRACE(message)
Definition logging.h:12
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_ERROR_COND(cond, message)
Definition macros.h:52
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
#define STORM_PRINT_AND_LOG(message)
Definition macros.h:68
void extractSchedulerChoices(storm::storage::Scheduler< SolutionType > &scheduler, std::vector< uint64_t > const &subChoices, storm::storage::BitVector const &maybeStates)
boost::optional< SparseMdpEndComponentInformation< ValueType > > computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, bool produceScheduler)
QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
QualitativeStateSetsUntilProbabilities computeQualitativeStateSetsUntilProbabilities(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
void extractValueAndSchedulerHint(SparseMdpHintType< SolutionType > &hintStorage, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, boost::optional< storm::storage::BitVector > const &selectedChoices, ModelCheckerHint const &hint, bool skipECWithinMaybeStatesCheck)
std::vector< uint_fast64_t > computeValidSchedulerHint(Environment const &env, SemanticSolutionType const &type, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &filterStates, storm::storage::BitVector const &targetStates, boost::optional< storm::storage::BitVector > const &selectedChoices)
SparseMdpHintType< SolutionType > computeHints(Environment const &env, SemanticSolutionType const &type, ModelCheckerHint const &hint, storm::OptimizationDirection const &dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &targetStates, bool produceScheduler, boost::optional< storm::storage::BitVector > const &selectedChoices=boost::none)
QualitativeStateSetsUntilProbabilities getQualitativeStateSetsUntilProbabilitiesFromHint(ModelCheckerHint const &hint)
std::vector< ValueType > computeUpperRewardBounds(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &rewards, std::vector< ValueType > const &oneStepTargetProbabilities)
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, ModelCheckerHint const &hint, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)
void computeFixedPointSystemUntilProbabilities(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b)
MaybeStateResult< SolutionType > computeValuesForMaybeStates(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > &&submatrix, std::vector< ValueType > const &b, bool produceScheduler, SparseMdpHintType< SolutionType > &hint)
void extendScheduler(storm::storage::Scheduler< SolutionType > &scheduler, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewardsFromHint(ModelCheckerHint const &hint, storm::storage::BitVector const &targetStates)
boost::optional< SparseMdpEndComponentInformation< ValueType > > computeFixedPointSystemReachabilityRewardsEliminateEndComponents(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, boost::optional< std::vector< ValueType > > &oneStepTargetProbabilities, bool produceScheduler)
QualitativeStateSetsUntilProbabilities getQualitativeStateSetsUntilProbabilities(storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, ModelCheckerHint const &hint)
void computeFixedPointSystemReachabilityRewards(storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, std::vector< ValueType > *oneStepTargetProbabilities=nullptr)
std::unique_ptr< storm::solver::MinMaxLinearEquationSolver< ValueType, SolutionType > > configureMinMaxLinearEquationSolver(Environment const &env, SolveGoal< ValueType, SolutionType > &&goal, storm::solver::MinMaxLinearEquationSolverFactory< ValueType, SolutionType > const &factory, MatrixType &&matrix)
Definition SolveGoal.h:107
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Max(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)
Definition graph.cpp:825
void computeSchedulerStayingInStates(storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the given states that chooses an action that stays completely in the very sa...
Definition graph.cpp:489
void computeSchedulerProbGreater0E(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates...
Definition graph.cpp:541
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:847
void computeSchedulerProb1E(storm::storage::BitVector const &prob1EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter)
Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates a...
Definition graph.cpp:614
storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 1 of satisfying phi until psi under all possible re...
Definition graph.cpp:987
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:679
storm::storage::BitVector performProb1(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
Computes the set of states of the given model for which all paths lead to the given set of target sta...
Definition graph.cpp:382
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:966
void computeSchedulerProb0E(storm::storage::BitVector const &prob0EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Computes a scheduler for the given states that have a scheduler that has a probability 0.
Definition graph.cpp:592
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01Min(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)
Definition graph.cpp:1069
storm::storage::BitVector performProb1E(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, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability 1 of satisfying phi until psi under at least one po...
Definition graph.cpp:747
void computeSchedulerRewInf(storm::storage::BitVector const &rewInfStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::Scheduler< SchedulerValueType > &scheduler)
Computes a scheduler for the given states that have a scheduler that has a reward infinity.
Definition graph.cpp:598
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
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 setAllValues(std::vector< T > &vec, storm::storage::BitVector const &positions, T const &positiveValue=storm::utility::one< T >(), T const &negativeValue=storm::utility::zero< T >())
Definition vector.h:57
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 filterVectorInPlace(std::vector< Type > &v, storm::storage::BitVector const &filter)
Definition vector.h:1075
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:37
bool isZero(ValueType const &a)
Definition constants.cpp:42
bool isInfinity(ValueType const &a)
Definition constants.cpp:72
LabParser.cpp.
boost::optional< std::vector< uint64_t > > scheduler
MaybeStateResult(std::vector< ValueType > &&values)
std::vector< uint64_t > const & getScheduler() const
std::vector< ValueType > const & getValues() const
boost::optional< std::vector< uint64_t > > schedulerHint
boost::optional< std::vector< ValueType > > valueHint
std::vector< ValueType > const & getUpperResultBounds() const
boost::optional< std::vector< ValueType > > upperResultBounds