Storm 1.10.0.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
12
14
16
17#include "storm/utility/graph.h"
20
24
28
34
35#include "storm/io/export.h"
40
42
44
52
53namespace storm {
54namespace modelchecker {
55namespace helper {
56
57template<typename ValueType, typename SolutionType>
58std::map<storm::storage::sparse::state_type, SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeRewardBoundedValues(
60 storm::storage::BitVector const& initialStates) {
61 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
62 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing reward bounded values with interval models.");
63 } else {
64 storm::utility::Stopwatch swAll(true), swBuild, swCheck;
65
66 // Get lower and upper bounds for the solution.
67 auto lowerBound = rewardUnfolding.getLowerObjectiveBound();
68 auto upperBound = rewardUnfolding.getUpperObjectiveBound();
69
70 // Initialize epoch models
71 auto initEpoch = rewardUnfolding.getStartEpoch();
72 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
73
74 // initialize data that will be needed for each epoch
75 std::vector<ValueType> x, b;
76 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
77
78 ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(
79 initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
80 Environment preciseEnv = env;
81 preciseEnv.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(precision));
82
83 // In case of cdf export we store the necessary data.
84 std::vector<std::vector<ValueType>> cdfData;
85
86 storm::utility::ProgressMeasurement progress("epochs");
87 progress.setMaxCount(epochOrder.size());
88 progress.startNewMeasurement(0);
89 uint64_t numCheckedEpochs = 0;
90 for (auto const& epoch : epochOrder) {
91 swBuild.start();
92 auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
93 swBuild.stop();
94 swCheck.start();
95 rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, dir, x, b, minMaxSolver, lowerBound, upperBound));
96 swCheck.stop();
98 !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
99 std::vector<ValueType> cdfEntry;
100 for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) {
101 uint64_t offset = rewardUnfolding.getDimension(i).boundType == helper::rewardbounded::DimensionBoundType::LowerBound ? 1 : 0;
102 cdfEntry.push_back(storm::utility::convertNumber<ValueType>(rewardUnfolding.getEpochManager().getDimensionOfEpoch(epoch, i) + offset) *
103 rewardUnfolding.getDimension(i).scalingFactor);
104 }
105 cdfEntry.push_back(rewardUnfolding.getInitialStateResult(epoch));
106 cdfData.push_back(std::move(cdfEntry));
107 }
108 ++numCheckedEpochs;
109 progress.updateProgress(numCheckedEpochs);
111 break;
112 }
113 }
114
115 std::map<storm::storage::sparse::state_type, ValueType> result;
116 for (auto initState : initialStates) {
117 result[initState] = rewardUnfolding.getInitialStateResult(initEpoch, initState);
118 }
119
120 swAll.stop();
121
123 std::vector<std::string> headers;
124 for (uint64_t i = 0; i < rewardUnfolding.getEpochManager().getDimensionCount(); ++i) {
125 headers.push_back(rewardUnfolding.getDimension(i).formula->toString());
126 }
127 headers.push_back("Result");
128 storm::io::exportDataToCSVFile<ValueType, std::string, std::string>(
129 storm::settings::getModule<storm::settings::modules::IOSettings>().getExportCdfDirectory() + "cdf.csv", cdfData, headers);
130 }
131
133 STORM_PRINT_AND_LOG("---------------------------------\n");
134 STORM_PRINT_AND_LOG("Statistics:\n");
135 STORM_PRINT_AND_LOG("---------------------------------\n");
136 STORM_PRINT_AND_LOG(" #checked epochs: " << epochOrder.size() << ".\n");
137 STORM_PRINT_AND_LOG(" overall Time: " << swAll << ".\n");
138 STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << ".\n");
139 STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << ".\n");
140 STORM_PRINT_AND_LOG("---------------------------------\n");
141 }
142
143 return result;
144 }
145}
146
147template<typename ValueType, typename SolutionType>
149 Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
150 storm::storage::BitVector const& nextStates) {
151 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
152 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support next probabilities with reward models.");
153 } else {
154 // Create the vector with which to multiply and initialize it correctly.
155 std::vector<ValueType> result(transitionMatrix.getRowGroupCount());
156 storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
157
158 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
159 multiplier->multiplyAndReduce(env, dir, result, nullptr, result);
160
161 return result;
162 }
163}
164
165template<typename ValueType, typename SolutionType = ValueType>
166std::vector<uint_fast64_t> computeValidSchedulerHint(Environment const& env, SemanticSolutionType const& type,
167 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
168 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
169 storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates,
170 storm::storage::BitVector const& targetStates,
171 boost::optional<storm::storage::BitVector> const& selectedChoices) {
172 storm::storage::Scheduler<SolutionType> validScheduler(maybeStates.size());
173
175 storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler,
176 selectedChoices);
177 } else if (type == SemanticSolutionType::ExpectedRewards) {
178 storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates,
179 validScheduler, selectedChoices);
180 } else {
181 STORM_LOG_ASSERT(false, "Unexpected equation system type.");
182 }
183
184 // Extract the relevant parts of the scheduler for the solver.
185 std::vector<uint64_t> schedulerHint;
186 schedulerHint.reserve(maybeStates.getNumberOfSetBits());
187 if (selectedChoices) {
188 // There might be unselected choices so the local choice indices from the scheduler need to be adapted
189 for (auto maybeState : maybeStates) {
190 auto choice = validScheduler.getChoice(maybeState).getDeterministicChoice();
191 auto const groupStart = transitionMatrix.getRowGroupIndices()[maybeState];
192 auto const origGlobalChoiceIndex = groupStart + choice;
193 STORM_LOG_ASSERT(selectedChoices->get(origGlobalChoiceIndex), "The computed scheduler selects an illegal choice.");
194 // Count the number of unselected choices in [groupStart, origGlobalChoiceIndex) and subtract that from choice
195 for (auto pos = selectedChoices->getNextUnsetIndex(groupStart); pos < origGlobalChoiceIndex; pos = selectedChoices->getNextUnsetIndex(pos + 1)) {
196 --choice;
197 }
198 schedulerHint.push_back(choice);
199 }
200 } else {
201 for (auto maybeState : maybeStates) {
202 schedulerHint.push_back(validScheduler.getChoice(maybeState).getDeterministicChoice());
203 }
204 }
205 return schedulerHint;
206}
207
208template<typename ValueType>
211 // Intentionally left empty.
212 }
213
214 bool hasSchedulerHint() const {
215 return static_cast<bool>(schedulerHint);
216 }
217
218 bool hasValueHint() const {
219 return static_cast<bool>(valueHint);
220 }
221
222 bool hasLowerResultBound() const {
223 return static_cast<bool>(lowerResultBound);
224 }
225
226 ValueType const& getLowerResultBound() const {
227 return lowerResultBound.get();
228 }
229
230 bool hasUpperResultBound() const {
231 return static_cast<bool>(upperResultBound);
232 }
233
234 bool hasUpperResultBounds() const {
235 return static_cast<bool>(upperResultBounds);
236 }
237
238 ValueType const& getUpperResultBound() const {
239 return upperResultBound.get();
240 }
241
242 std::vector<ValueType>& getUpperResultBounds() {
243 return upperResultBounds.get();
244 }
245
246 std::vector<ValueType> const& getUpperResultBounds() const {
247 return upperResultBounds.get();
248 }
249
250 std::vector<uint64_t>& getSchedulerHint() {
251 return schedulerHint.get();
252 }
253
254 std::vector<ValueType>& getValueHint() {
255 return valueHint.get();
256 }
257
260 }
261
263 return computeUpperBounds;
264 }
265
266 bool hasUniqueSolution() const {
267 return uniqueSolution;
268 }
269
270 bool hasNoEndComponents() const {
271 return noEndComponents;
272 }
273
274 boost::optional<std::vector<uint64_t>> schedulerHint;
275 boost::optional<std::vector<ValueType>> valueHint;
276 boost::optional<ValueType> lowerResultBound;
277 boost::optional<ValueType> upperResultBound;
278 boost::optional<std::vector<ValueType>> upperResultBounds;
283};
284
285template<typename ValueType, typename SolutionType>
287 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates,
288 boost::optional<storm::storage::BitVector> const& selectedChoices, ModelCheckerHint const& hint,
289 bool skipECWithinMaybeStatesCheck) {
290 // Deal with scheduler hint.
291 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint()) {
292 if (hintStorage.hasSchedulerHint()) {
293 STORM_LOG_WARN("A scheduler hint was provided, but the solver requires a specific one. The provided scheduler hint will be ignored.");
294 } else {
295 auto const& schedulerHint = hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint();
296 std::vector<uint64_t> hintChoices;
297
298 // The scheduler hint is only applicable if it induces no BSCC consisting of maybe states.
299 bool hintApplicable;
300 if (!skipECWithinMaybeStatesCheck) {
301 hintChoices.reserve(maybeStates.size());
302 for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) {
303 hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice());
304 }
305 hintApplicable =
306 storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full();
307 } else {
308 hintApplicable = true;
309 }
310
311 if (hintApplicable) {
312 // Compute the hint w.r.t. the given subsystem.
313 hintChoices.clear();
314 hintChoices.reserve(maybeStates.getNumberOfSetBits());
315 for (auto state : maybeStates) {
316 uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice();
317 if (selectedChoices) {
318 uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state];
319 uint_fast64_t lastChoice = firstChoice + hintChoice;
320 hintChoice = 0;
321 for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice;
322 choice = selectedChoices->getNextSetIndex(choice + 1)) {
323 ++hintChoice;
324 }
325 }
326 hintChoices.push_back(hintChoice);
327 }
328 hintStorage.schedulerHint = std::move(hintChoices);
329 }
330 }
331 }
332
333 // Deal with solution value hint. Only applicable if there are no End Components consisting of maybe states.
334 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint() &&
335 (skipECWithinMaybeStatesCheck || hintStorage.hasSchedulerHint() ||
336 storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)
337 .full())) {
338 hintStorage.valueHint = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<SolutionType>().getResultHint(), maybeStates);
339 }
340}
341
342template<typename ValueType, typename SolutionType>
345 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates,
346 storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, bool produceScheduler,
347 boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
349
350 // There are no end components if we minimize until probabilities or
351 // maximize reachability rewards or if the hint tells us so.
352 result.noEndComponents = (dir == storm::solver::OptimizationDirection::Minimize && type == SemanticSolutionType::UntilProbabilities) ||
353 (dir == storm::solver::OptimizationDirection::Maximize && type == SemanticSolutionType::ExpectedRewards) ||
354 (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
355
356 // If there are no end components, the solution is unique. (Note that the other direction does not hold,
357 // e.g., end components in which infinite reward is collected.
358 result.uniqueSolution = result.hasNoEndComponents();
359
360 // Check for requirements of the solver.
361 bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint();
364 minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, result.noEndComponents, dir, hasSchedulerHint, produceScheduler);
365 if (requirements.hasEnabledRequirement()) {
366 // If the solver still requires no end-components, we have to eliminate them later.
367 if (requirements.uniqueSolution()) {
369 "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
370 STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires a unique solution.");
371 result.eliminateEndComponents = true;
372 // If end components have been eliminated we can assume a unique solution.
373 result.uniqueSolution = true;
374 requirements.clearUniqueSolution();
375 // If we compute until probabilities, we can even assume the absence of end components.
376 // Note that in the case of minimizing expected rewards there might still be end components in which reward is collected.
378 }
379
380 // If the solver requires an initial scheduler, compute one now. Note that any scheduler is valid if there are no end components.
381 if (requirements.validInitialScheduler() && !result.noEndComponents) {
382 STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
383 result.schedulerHint = computeValidSchedulerHint<ValueType, SolutionType>(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates,
384 targetStates, selectedChoices);
385 requirements.clearValidInitialScheduler();
386 }
387
388 // Finally, we have information on the bounds depending on the problem type.
390 requirements.clearBounds();
391 } else if (type == SemanticSolutionType::ExpectedRewards) {
392 requirements.clearLowerBounds();
393 }
394 if (requirements.upperBounds()) {
395 result.computeUpperBounds = true;
396 requirements.clearUpperBounds();
397 }
398 STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException,
399 "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
400 } else {
401 STORM_LOG_DEBUG("Solver has no requirements.");
402 }
403
404 // Only if there is no end component decomposition that we will need to do later, we use value and scheduler
405 // hints from the provided hint.
406 if (!result.eliminateEndComponents) {
407 extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, result.uniqueSolution);
408 } else {
409 if (hint.isEmpty()) {
410 STORM_LOG_TRACE("Warn A non-empty hint was provided, but its information will be disregarded.");
411 }
412 }
413
414 // Only set bounds if we did not obtain them from the hint.
415 if (!result.hasLowerResultBound()) {
416 result.lowerResultBound = storm::utility::zero<SolutionType>();
417 }
419 result.upperResultBound = storm::utility::one<SolutionType>();
420 }
421
422 // If we received an upper bound, we can drop the requirement to compute one.
423 if (result.hasUpperResultBound()) {
424 result.computeUpperBounds = false;
425 }
426
427 return result;
428}
429
430template<typename ValueType>
432 MaybeStateResult(std::vector<ValueType>&& values) : values(std::move(values)) {
433 // Intentionally left empty.
434 }
435
436 bool hasScheduler() const {
437 return static_cast<bool>(scheduler);
438 }
439
440 std::vector<uint64_t> const& getScheduler() const {
441 return scheduler.get();
442 }
443
444 std::vector<ValueType> const& getValues() const {
445 return values;
446 }
447
448 std::vector<ValueType> values;
449 boost::optional<std::vector<uint64_t>> scheduler;
450};
451
452template<typename ValueType, typename SolutionType>
454 storm::storage::SparseMatrix<ValueType>&& submatrix, std::vector<ValueType> const& b,
455 bool produceScheduler, SparseMdpHintType<SolutionType>& hint) {
456 // Initialize the solution vector.
457 std::vector<SolutionType> x =
458 hint.hasValueHint() ? std::move(hint.getValueHint())
459 : std::vector<SolutionType>(submatrix.getRowGroupCount(),
460 hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero<SolutionType>());
461
462 // Set up the solver.
464 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType, SolutionType>> solver =
465 storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
466 solver->setRequirementsChecked();
467 solver->setUncertaintyIsRobust(goal.isRobust());
468 solver->setHasUniqueSolution(hint.hasUniqueSolution());
469 solver->setHasNoEndComponents(hint.hasNoEndComponents());
470 if (hint.hasLowerResultBound()) {
471 solver->setLowerBound(hint.getLowerResultBound());
472 }
473 if (hint.hasUpperResultBound()) {
474 solver->setUpperBound(hint.getUpperResultBound());
475 }
476 if (hint.hasUpperResultBounds()) {
477 solver->setUpperBounds(std::move(hint.getUpperResultBounds()));
478 }
479 if (hint.hasSchedulerHint()) {
480 solver->setInitialScheduler(std::move(hint.getSchedulerHint()));
481 }
482 solver->setTrackScheduler(produceScheduler);
483
484 // Solve the corresponding system of equations.
485 solver->solveEquations(env, x, b);
486
487#ifndef NDEBUG
488 // As a sanity check, make sure our local upper bounds were in fact correct.
490 auto resultIt = x.begin();
491 for (auto const& entry : solver->getUpperBounds()) {
493 *resultIt <= entry + storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision()),
494 "Expecting result value for state " << std::distance(x.begin(), resultIt) << " to be <= " << entry << ", but got " << *resultIt << ".");
495 ++resultIt;
496 }
497 }
498#endif
499
500 // Create result.
501 MaybeStateResult<SolutionType> result(std::move(x));
502
503 // If requested, return the requested scheduler.
504 if (produceScheduler) {
505 result.scheduler = std::move(solver->getSchedulerChoices());
506 }
507 return result;
508}
509
515
516template<typename ValueType>
519 result.maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
520
521 // Treat the states with probability zero/one.
522 std::vector<ValueType> const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
525 storm::storage::BitVector nonMaybeStates = ~result.maybeStates;
526 for (auto state : nonMaybeStates) {
527 if (storm::utility::isOne(resultsForNonMaybeStates[state])) {
528 result.statesWithProbability1.set(state, true);
529 } else {
530 STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException,
531 "Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
532 result.statesWithProbability0.set(state, true);
533 }
534 }
535
536 return result;
537}
538
539template<typename ValueType, typename SolutionType>
541 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
542 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
543 storm::storage::BitVector const& phiStates,
544 storm::storage::BitVector const& psiStates) {
546
547 // Get all states that have probability 0 and 1 of satisfying the until-formula.
548 std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
549 if (goal.minimize()) {
550 statesWithProbability01 =
551 storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
552 } else {
553 statesWithProbability01 =
554 storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
555 }
556 result.statesWithProbability0 = std::move(statesWithProbability01.first);
557 result.statesWithProbability1 = std::move(statesWithProbability01.second);
559
560 return result;
561}
562
563template<typename ValueType, typename SolutionType>
565 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
566 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
567 storm::storage::BitVector const& phiStates,
568 storm::storage::BitVector const& psiStates, ModelCheckerHint const& hint) {
569 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
570 return getQualitativeStateSetsUntilProbabilitiesFromHint<ValueType>(hint);
571 } else {
572 return computeQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates);
573 }
574}
575
576template<typename SolutionType, bool subChoicesCoverOnlyMaybeStates = true>
577void extractSchedulerChoices(storm::storage::Scheduler<SolutionType>& scheduler, std::vector<uint64_t> const& subChoices,
578 storm::storage::BitVector const& maybeStates) {
579 if constexpr (subChoicesCoverOnlyMaybeStates) {
580 auto subChoiceIt = subChoices.begin();
581 for (auto maybeState : maybeStates) {
582 scheduler.setChoice(*subChoiceIt, maybeState);
583 ++subChoiceIt;
584 }
585 assert(subChoiceIt == subChoices.end());
586 } else {
587 // See computeFixedPointSystemUntilProbabilities, where we create a different equation system.
588 // Consequentially, we run a slightly different code here for interval-based models.
589 STORM_LOG_ASSERT(maybeStates.size() == subChoices.size(), "Sizes do not coincide.");
590 for (auto maybeState : maybeStates) {
591 scheduler.setChoice(subChoices[maybeState], maybeState);
592 }
593 }
594}
595
596template<typename ValueType, typename SolutionType>
598 QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
599 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates,
600 storm::storage::BitVector const& psiStates) {
601 // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
602 // the states with probability 1 or 0 (depending on whether we maximize or minimize).
603 // We also need to define some arbitrary choice for the remaining states to obtain a fully defined scheduler.
604 if (goal.minimize()) {
605 storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.statesWithProbability0, transitionMatrix, scheduler);
606 for (auto prob1State : qualitativeStateSets.statesWithProbability1) {
607 scheduler.setChoice(0, prob1State);
608 }
609 } else {
610 storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.statesWithProbability1, transitionMatrix, backwardTransitions, phiStates, psiStates,
611 scheduler);
612 for (auto prob0State : qualitativeStateSets.statesWithProbability0) {
613 scheduler.setChoice(0, prob0State);
614 }
615 }
616}
617
618template<typename ValueType, typename SolutionType>
620 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
621 QualitativeStateSetsUntilProbabilities const& qualitativeStateSets,
622 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b) {
623 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
624 // For non-interval based models, we can eliminate the rows and columns from the original transition probability matrix for states
625 // whose probabilities are already known... However, there is information in the transition to those states.
626 // Thus, we cannot eliminate them all.
627 // We can however drop all the outgoing transitions from these states.
628 // 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),
629 // TODO ctned: however, there is quite some bookkeeping involved in projecting the right vectors.
630 // TODO ctned: Instead is likely easier to just do a pass and make a unique sink and a unique target state.
631 // TODO ctned: If this is ever changed, extractSchedulerChoices must also be updated.
632 submatrix = transitionMatrix.filterEntries(transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates));
633
634 // Prepare the right-hand side of the equation system. For entry i this corresponds to
635 // the accumulated probability of going from state i to some state that has probability 1.
636 storm::utility::vector::setAllValues(b, transitionMatrix.getRowFilter(qualitativeStateSets.statesWithProbability1));
637 } else {
638 // First, we can eliminate the rows and columns from the original transition probability matrix for states
639 // whose probabilities are already known.
640 submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false);
641
642 // Prepare the right-hand side of the equation system. For entry i this corresponds to
643 // the accumulated probability of going from state i to some state that has probability 1.
644 b = transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.statesWithProbability1);
645 }
646 // If the solve goal has relevant values, we need to adjust them.
647 goal.restrictRelevantValues(qualitativeStateSets.maybeStates);
648}
649
650template<typename ValueType, typename SolutionType>
651boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(
653 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets,
654 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, bool produceScheduler) {
655 // Get the set of states that (under some scheduler) can stay in the set of maybestates forever
657 transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, qualitativeStateSets.maybeStates, ~qualitativeStateSets.maybeStates);
658
659 bool doDecomposition = !candidateStates.empty();
660
662 if (doDecomposition) {
663 // Compute the states that are in MECs.
664 endComponentDecomposition = storm::storage::MaximalEndComponentDecomposition<ValueType>(transitionMatrix, backwardTransitions, candidateStates);
665 STORM_LOG_INFO(endComponentDecomposition.statistics(transitionMatrix.getRowGroupCount()));
666 }
667
668 // Only do more work if there are actually end-components.
669 if (doDecomposition && !endComponentDecomposition.empty()) {
670 STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " EC(s).");
672 endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates, &qualitativeStateSets.statesWithProbability1, nullptr, nullptr,
673 submatrix, &b, nullptr, produceScheduler);
674
675 // If the solve goal has relevant values, we need to adjust them.
676 if (goal.hasRelevantValues()) {
677 storm::storage::BitVector newRelevantValues(submatrix.getRowGroupCount());
678 for (auto state : goal.relevantValues()) {
679 if (qualitativeStateSets.maybeStates.get(state)) {
680 newRelevantValues.set(result.getRowGroupAfterElimination(state));
681 }
682 }
683 if (!newRelevantValues.empty()) {
684 goal.setRelevantValues(std::move(newRelevantValues));
685 }
686 }
687
688 return result;
689 } else {
690 STORM_LOG_DEBUG("Not eliminating ECs as there are none.");
691 computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b);
692
693 return boost::none;
694 }
695}
696
697template<typename ValueType, typename SolutionType>
700 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates,
701 bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) {
702 STORM_LOG_THROW(!qualitative || !produceScheduler, storm::exceptions::InvalidSettingsException,
703 "Cannot produce scheduler when performing qualitative model checking only.");
704
705 // Prepare resulting vector.
706 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
707
708 // We need to identify the maybe states (states which have a probability for satisfying the until formula
709 // that is strictly between 0 and 1) and the states that satisfy the formula with probablity 1 and 0, respectively.
710 QualitativeStateSetsUntilProbabilities qualitativeStateSets =
711 getQualitativeStateSetsUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, hint);
712
713 STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.statesWithProbability1.getNumberOfSetBits() << " states with probability 1, "
714 << qualitativeStateSets.statesWithProbability0.getNumberOfSetBits() << " with probability 0 ("
715 << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
716
717 // Set values of resulting vector that are known exactly.
718 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.statesWithProbability1, storm::utility::one<SolutionType>());
719
720 // Check if the values of the maybe states are relevant for the SolveGoal
721 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
722
723 // If requested, we will produce a scheduler.
724 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
725 if (produceScheduler) {
726 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.getRowGroupCount());
727 // If maybeStatesNotRelevant is true, we have to set the scheduler for maybe states as "dontCare"
728 if (maybeStatesNotRelevant) {
729 for (auto state : qualitativeStateSets.maybeStates) {
730 scheduler->setDontCare(state);
731 }
732 }
733 }
734
735 // Check whether we need to compute exact probabilities for some states.
736 if (qualitative || maybeStatesNotRelevant) {
737 // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
738 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, storm::utility::convertNumber<SolutionType>(0.5));
739 } else {
740 if (!qualitativeStateSets.maybeStates.empty()) {
741 // In this case we have have to compute the remaining probabilities.
742
743 // Obtain proper hint information either from the provided hint or from requirements of the solver.
744 SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
745 env, SemanticSolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
746 phiStates, qualitativeStateSets.statesWithProbability1, produceScheduler);
747
748 // Declare the components of the equation system we will solve.
750 std::vector<ValueType> b;
751
752 // If the hint information tells us that we have to eliminate MECs, we do so now.
753 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
754 if (hintInformation.getEliminateEndComponents()) {
755 ecInformation = computeFixedPointSystemUntilProbabilitiesEliminateEndComponents(goal, transitionMatrix, backwardTransitions,
756 qualitativeStateSets, submatrix, b, produceScheduler);
757 } else {
758 // Otherwise, we compute the standard equations.
759 computeFixedPointSystemUntilProbabilities(goal, transitionMatrix, qualitativeStateSets, submatrix, b);
760 }
761
762 // Now compute the results for the maybe states.
763 MaybeStateResult<SolutionType> resultForMaybeStates =
764 computeValuesForMaybeStates(env, std::move(goal), std::move(submatrix), b, produceScheduler, hintInformation);
765
766 // If we eliminated end components, we need to extract the result differently.
767 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
768 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
769 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support this end component with interval models.");
770 } else {
771 ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
772 if (produceScheduler) {
773 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions,
774 resultForMaybeStates.getScheduler());
775 }
776 }
777 } else {
778 // Set values of resulting vector according to result.
779 if constexpr (!std::is_same_v<ValueType, storm::Interval>) {
780 // For non-interval models, we only operated on the maybe states, and we must recover the qualitative values for the other state.
781 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
782 } else {
783 // For interval models, the result for maybe states indeed also holds values for all qualitative states.
784 STORM_LOG_ASSERT(resultForMaybeStates.getValues().size() == transitionMatrix.getColumnCount(), "Dimensions do not match");
785 result = resultForMaybeStates.getValues();
786 }
787 if (produceScheduler) {
788 extractSchedulerChoices<SolutionType, !std::is_same_v<ValueType, storm::Interval>>(*scheduler, resultForMaybeStates.getScheduler(),
789 qualitativeStateSets.maybeStates);
790 }
791 }
792 }
793 }
794
795 // Extend scheduler with choices for the states in the qualitative state sets.
796 if (produceScheduler) {
797 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, phiStates, psiStates);
798 }
799
800 // Sanity check for created scheduler.
801 STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained.");
802 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler");
803 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler");
804 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler");
805
806 // Return result.
807 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result), std::move(scheduler));
808}
809
810template<typename ValueType, typename SolutionType>
813 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler,
814 bool useMecBasedTechnique) {
815 if (useMecBasedTechnique) {
816 // TODO: does this really work for minimizing objectives?
817 storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(transitionMatrix, backwardTransitions, psiStates);
818 storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount());
819 for (auto const& mec : mecDecomposition) {
820 for (auto const& stateActionsPair : mec) {
821 statesInPsiMecs.set(stateActionsPair.first, true);
822 }
823 }
824
825 return computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative,
826 produceScheduler);
827 } else {
828 goal.oneMinus();
829 auto result =
830 computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions,
831 storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, produceScheduler);
832 for (auto& element : result.values) {
833 element = storm::utility::one<SolutionType>() - element;
834 }
835 return result;
836 }
837}
838
839template<typename ValueType, typename SolutionType>
840template<typename RewardModelType>
843 RewardModelType const& rewardModel, uint_fast64_t stepCount) {
844 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
845 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support instantenous rewards with interval models.");
846 } else {
847 // Only compute the result if the model has a state-based reward this->getModel().
848 STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException,
849 "Computing instantaneous rewards for a reward model that does not define any state-rewards. The result is trivially 0.");
850 // Initialize result to state rewards of the this->getModel().
851 std::vector<SolutionType> result(rewardModel.getStateRewardVector());
852
853 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
854 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, nullptr, stepCount);
855
856 return result;
857 }
858}
859
860template<typename ValueType, typename SolutionType>
861template<typename RewardModelType>
864 RewardModelType const& rewardModel, uint_fast64_t stepBound) {
865 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
866 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support cumulative rewards with interval models.");
867 } else {
868 // Only compute the result if the model has at least one reward this->getModel().
869 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
870
871 // Compute the reward vector to add in each step based on the available reward models.
872 std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix);
873
874 // Initialize result to the zero vector.
875 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
876
877 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
878 multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound);
879
880 return result;
881 }
882}
883
884template<typename ValueType, typename SolutionType>
885template<typename RewardModelType>
888 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, bool produceScheduler,
889 ModelCheckerHint const& hint) {
890 STORM_LOG_THROW(!rewardModel.hasNegativeRewards(), storm::exceptions::NotImplementedException,
891 "The reward model contains negative rewards. This is not implemented by the total rewards computation.");
892 // Reduce to reachability rewards
893 if (goal.minimize()) {
894 // Identify the states from which no reward can be collected under some scheduler
895 storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix);
896 storm::storage::BitVector statesWithZeroRewardChoice(transitionMatrix.getRowGroupCount(), false);
897 for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) {
898 if (choicesWithoutReward.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]) < transitionMatrix.getRowGroupIndices()[state + 1]) {
899 statesWithZeroRewardChoice.set(state);
900 }
901 }
902 storm::storage::BitVector rew0EStates =
903 storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions,
904 statesWithZeroRewardChoice, ~statesWithZeroRewardChoice, false, 0, choicesWithoutReward);
905 rew0EStates.complement();
906 auto result = computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0EStates, qualitative,
907 produceScheduler, hint);
908 if (result.scheduler) {
909 storm::utility::graph::computeSchedulerStayingInStates(rew0EStates, transitionMatrix, *result.scheduler, choicesWithoutReward);
910 }
911 return result;
912 } else {
913 // Identify the states from which only states with zero reward are reachable.
914 storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix);
915 storm::storage::BitVector rew0AStates = storm::utility::graph::performProbGreater0E(backwardTransitions, statesWithoutReward, ~statesWithoutReward);
916 rew0AStates.complement();
917
918 // There might be end components that consists only of states/choices with zero rewards. The reachability reward semantics would assign such
919 // end components reward infinity. To avoid this, we potentially need to eliminate such end components
920 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
921 if (storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, rew0AStates)
922 .full()) {
923 return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0AStates, qualitative,
924 produceScheduler, hint);
925 } else {
926 // The transformation of schedulers for the ec-eliminated system back to the original one is not implemented.
927 STORM_LOG_ERROR_COND(!produceScheduler, "Can not produce scheduler for this property (functionality not implemented");
928 storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix);
930 transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), choicesWithoutReward, rew0AStates, true);
931 storm::storage::BitVector newRew0AStates(ecElimResult.matrix.getRowGroupCount(), false);
932 for (auto oldRew0AState : rew0AStates) {
933 newRew0AStates.set(ecElimResult.oldToNewStateMapping[oldRew0AState]);
934 }
935
936 if (goal.hasRelevantValues()) {
937 storm::storage::BitVector newRelevantValues(ecElimResult.matrix.getRowGroupCount(), false);
938 for (auto oldRelevantState : goal.relevantValues()) {
939 newRelevantValues.set(ecElimResult.oldToNewStateMapping[oldRelevantState]);
940 }
941 goal.relevantValues() = std::move(newRelevantValues);
942 }
943
944 MDPSparseModelCheckingHelperReturnType<SolutionType> result = computeReachabilityRewardsHelper(
945 env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(true),
946 [&](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& newTransitionMatrix, storm::storage::BitVector const& maybeStates) {
947 std::vector<ValueType> result;
948 std::vector<ValueType> oldChoiceRewards = rewardModel.getTotalRewardVector(transitionMatrix);
949 result.reserve(rowCount);
950 for (uint64_t newState : maybeStates) {
951 for (auto newChoice : newTransitionMatrix.getRowGroupIndices(newState)) {
952 uint64_t oldChoice = ecElimResult.newToOldRowMapping[newChoice];
953 result.push_back(oldChoiceRewards[oldChoice]);
954 }
955 }
956 STORM_LOG_ASSERT(result.size() == rowCount, "Unexpected size of reward vector.");
957 return result;
958 },
959 newRew0AStates, qualitative, false,
960 [&]() {
961 storm::storage::BitVector newStatesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false);
962 for (auto oldStateWithoutRew : statesWithoutReward) {
963 newStatesWithoutReward.set(ecElimResult.oldToNewStateMapping[oldStateWithoutRew]);
964 }
965 return newStatesWithoutReward;
966 },
967 [&]() {
968 storm::storage::BitVector newChoicesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false);
969 for (uint64_t newChoice = 0; newChoice < ecElimResult.matrix.getRowCount(); ++newChoice) {
970 if (choicesWithoutReward.get(ecElimResult.newToOldRowMapping[newChoice])) {
971 newChoicesWithoutReward.set(newChoice);
972 }
973 }
974 return newChoicesWithoutReward;
975 });
976
977 std::vector<SolutionType> resultInEcQuotient = std::move(result.values);
978 result.values.resize(ecElimResult.oldToNewStateMapping.size());
979 storm::utility::vector::selectVectorValues(result.values, ecElimResult.oldToNewStateMapping, resultInEcQuotient);
980 return result;
981 }
982 }
983}
984
985template<typename ValueType, typename SolutionType>
986template<typename RewardModelType>
989 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates,
990 bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) {
991 // Only compute the result if the model has at least one reward this->getModel().
992 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Reward model for formula is empty. Skipping formula.");
993 return computeReachabilityRewardsHelper(
994 env, std::move(goal), transitionMatrix, backwardTransitions,
995 [&rewardModel](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
996 return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
997 },
998 targetStates, qualitative, produceScheduler, [&]() { return rewardModel.getStatesWithZeroReward(transitionMatrix); },
999 [&]() { return rewardModel.getChoicesWithZeroReward(transitionMatrix); }, hint);
1000}
1001
1002template<typename ValueType, typename SolutionType>
1005 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler,
1006 ModelCheckerHint const& hint) {
1007 return computeReachabilityRewardsHelper(
1008 env, std::move(goal), transitionMatrix, backwardTransitions,
1009 [](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&) {
1010 return std::vector<ValueType>(rowCount, storm::utility::one<ValueType>());
1011 },
1012 targetStates, qualitative, produceScheduler, [&]() { return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); },
1013 [&]() { return storm::storage::BitVector(transitionMatrix.getRowCount(), false); }, hint);
1014}
1015
1016#ifdef STORM_HAVE_CARL
1017template<typename ValueType, typename SolutionType>
1021 bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative) {
1022 // Only compute the result if the reward model is not empty.
1023 STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
1024 return computeReachabilityRewardsHelper(
1025 env, std::move(goal), transitionMatrix, backwardTransitions,
1026 [&](uint_fast64_t rowCount, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates) {
1027 std::vector<ValueType> result;
1028 result.reserve(rowCount);
1029 std::vector<storm::Interval> subIntervalVector = intervalRewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates);
1030 for (auto const& interval : subIntervalVector) {
1031 result.push_back(lowerBoundOfIntervals ? interval.lower() : interval.upper());
1032 }
1033 return result;
1034 },
1035 targetStates, qualitative, false,
1036 [&]() {
1037 return intervalRewardModel.getStatesWithFilter(
1038 transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); });
1039 },
1040 [&]() {
1041 return intervalRewardModel.getChoicesWithFilter(
1042 transitionMatrix, [&](storm::Interval const& i) { return storm::utility::isZero(lowerBoundOfIntervals ? i.lower() : i.upper()); });
1043 })
1044 .values;
1045}
1046
1047template<>
1048std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(
1051 storm::storage::BitVector const&, bool) {
1052 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Computing reachability rewards is unsupported for this data type.");
1053}
1054#endif
1055
1061
1062template<typename ValueType>
1064 storm::storage::BitVector const& targetStates) {
1066 result.maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
1067
1068 // Treat the states with reward zero/infinity.
1069 std::vector<ValueType> const& resultsForNonMaybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getResultHint();
1072 storm::storage::BitVector nonMaybeStates = ~result.maybeStates;
1073 for (auto state : nonMaybeStates) {
1074 if (storm::utility::isZero(resultsForNonMaybeStates[state])) {
1075 result.rewardZeroStates.set(state, true);
1076 } else {
1077 STORM_LOG_THROW(storm::utility::isInfinity(resultsForNonMaybeStates[state]), storm::exceptions::IllegalArgumentException,
1078 "Expected that the result hint specifies probabilities in {0,infinity} for non-maybe states");
1079 result.infinityStates.set(state, true);
1080 }
1081 }
1082 return result;
1083}
1084
1085template<typename ValueType, typename SolutionType>
1088 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates,
1089 std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
1091 storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
1092 if (goal.minimize()) {
1093 result.infinityStates =
1094 storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates);
1095 } else {
1096 result.infinityStates =
1097 storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates);
1098 }
1099 result.infinityStates.complement();
1100
1102 if (goal.minimize()) {
1103 result.rewardZeroStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions,
1104 trueStates, targetStates, zeroRewardChoicesGetter());
1105 } else {
1106 result.rewardZeroStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions,
1107 zeroRewardStatesGetter(), targetStates);
1108 }
1109 } else {
1110 result.rewardZeroStates = targetStates;
1111 }
1112 result.maybeStates = ~(result.rewardZeroStates | result.infinityStates);
1113 return result;
1114}
1115
1116template<typename ValueType, typename SolutionType>
1118 storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
1119 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
1120 storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint,
1121 std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter,
1122 std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
1123 if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
1124 return getQualitativeStateSetsReachabilityRewardsFromHint<ValueType>(hint, targetStates);
1125 } else {
1126 return computeQualitativeStateSetsReachabilityRewards(goal, transitionMatrix, backwardTransitions, targetStates, zeroRewardStatesGetter,
1127 zeroRewardChoicesGetter);
1128 }
1129}
1130
1131template<typename ValueType, typename SolutionType>
1133 QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
1134 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates,
1135 std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
1136 // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
1137 // the states with reward zero/infinity.
1138 if (goal.minimize()) {
1139 storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.rewardZeroStates, transitionMatrix, backwardTransitions,
1140 qualitativeStateSets.rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter());
1141 for (auto state : qualitativeStateSets.infinityStates) {
1142 scheduler.setChoice(0, state);
1143 }
1144 } else {
1145 storm::utility::graph::computeSchedulerRewInf(qualitativeStateSets.infinityStates, transitionMatrix, backwardTransitions, scheduler);
1146 for (auto state : qualitativeStateSets.rewardZeroStates) {
1147 scheduler.setChoice(0, state);
1148 }
1149 }
1150}
1151
1152template<typename ValueType, typename SolutionType>
1154 std::vector<uint_fast64_t> const& subChoices, storm::storage::BitVector const& maybeStates,
1155 boost::optional<storm::storage::BitVector> const& selectedChoices) {
1156 auto subChoiceIt = subChoices.begin();
1157 if (selectedChoices) {
1158 for (auto maybeState : maybeStates) {
1159 // find the rowindex that corresponds to the selected row of the submodel
1160 uint_fast64_t firstRowIndex = transitionMatrix.getRowGroupIndices()[maybeState];
1161 uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex);
1162 for (uint_fast64_t choice = 0; choice < *subChoiceIt; ++choice) {
1163 selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1);
1164 }
1165 scheduler.setChoice(selectedRowIndex - firstRowIndex, maybeState);
1166 ++subChoiceIt;
1167 }
1168 } else {
1169 for (auto maybeState : maybeStates) {
1170 scheduler.setChoice(*subChoiceIt, maybeState);
1171 ++subChoiceIt;
1172 }
1173 }
1174 assert(subChoiceIt == subChoices.end());
1175}
1176
1177template<typename ValueType, typename SolutionType>
1180 QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, boost::optional<storm::storage::BitVector> const& selectedChoices,
1181 std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const&
1182 totalStateRewardVectorGetter,
1183 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, std::vector<ValueType>* oneStepTargetProbabilities = nullptr) {
1184 // Remove rows and columns from the original transition probability matrix for states whose reward values are already known.
1185 // If there are infinity states, we additionally have to remove choices of maybeState that lead to infinity.
1186 if (qualitativeStateSets.infinityStates.empty()) {
1187 submatrix = transitionMatrix.getSubmatrix(true, qualitativeStateSets.maybeStates, qualitativeStateSets.maybeStates, false);
1188 b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, qualitativeStateSets.maybeStates);
1189 if (oneStepTargetProbabilities) {
1190 (*oneStepTargetProbabilities) =
1191 transitionMatrix.getConstrainedRowGroupSumVector(qualitativeStateSets.maybeStates, qualitativeStateSets.rewardZeroStates);
1192 }
1193 } else {
1194 submatrix = transitionMatrix.getSubmatrix(false, *selectedChoices, qualitativeStateSets.maybeStates, false);
1195 b = totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix,
1196 storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true));
1198 if (oneStepTargetProbabilities) {
1199 (*oneStepTargetProbabilities) = transitionMatrix.getConstrainedRowSumVector(*selectedChoices, qualitativeStateSets.rewardZeroStates);
1200 }
1201 }
1202
1203 // If the solve goal has relevant values, we need to adjust them.
1204 goal.restrictRelevantValues(qualitativeStateSets.maybeStates);
1205}
1206
1207template<typename ValueType, typename SolutionType>
1208boost::optional<SparseMdpEndComponentInformation<ValueType>> computeFixedPointSystemReachabilityRewardsEliminateEndComponents(
1210 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets,
1211 boost::optional<storm::storage::BitVector> const& selectedChoices,
1212 std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const&
1213 totalStateRewardVectorGetter,
1214 storm::storage::SparseMatrix<ValueType>& submatrix, std::vector<ValueType>& b, boost::optional<std::vector<ValueType>>& oneStepTargetProbabilities,
1215 bool produceScheduler) {
1216 // Start by computing the choices with reward 0, as we only want ECs within this fragment.
1217 storm::storage::BitVector zeroRewardChoices(transitionMatrix.getRowCount());
1218
1219 // Get the rewards of all choices.
1220 std::vector<ValueType> rewardVector =
1221 totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true));
1222
1223 uint64_t index = 0;
1224 for (auto const& e : rewardVector) {
1225 if (storm::utility::isZero(e)) {
1226 zeroRewardChoices.set(index);
1227 }
1228 ++index;
1229 }
1230
1231 // Compute the states that have some zero reward choice.
1232 storm::storage::BitVector candidateStates(qualitativeStateSets.maybeStates);
1233 for (auto state : qualitativeStateSets.maybeStates) {
1234 bool keepState = false;
1235
1236 for (auto row = transitionMatrix.getRowGroupIndices()[state], rowEnd = transitionMatrix.getRowGroupIndices()[state + 1]; row < rowEnd; ++row) {
1237 if (zeroRewardChoices.get(row)) {
1238 keepState = true;
1239 break;
1240 }
1241 }
1242
1243 if (!keepState) {
1244 candidateStates.set(state, false);
1245 }
1246 }
1247
1248 // Only keep the candidate states that (under some scheduler) can stay in the set of candidates forever
1249 candidateStates =
1250 storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates);
1251
1252 bool doDecomposition = !candidateStates.empty();
1253
1255 if (doDecomposition) {
1256 // Then compute the states that are in MECs with zero reward.
1257 endComponentDecomposition =
1258 storm::storage::MaximalEndComponentDecomposition<ValueType>(transitionMatrix, backwardTransitions, candidateStates, zeroRewardChoices);
1259 STORM_LOG_INFO(endComponentDecomposition.statistics(transitionMatrix.getRowGroupCount()));
1260 }
1261
1262 // Only do more work if there are actually end-components.
1263 if (doDecomposition && !endComponentDecomposition.empty()) {
1264 STORM_LOG_DEBUG("Eliminating " << endComponentDecomposition.size() << " ECs.");
1266 endComponentDecomposition, transitionMatrix, qualitativeStateSets.maybeStates,
1267 oneStepTargetProbabilities ? &qualitativeStateSets.rewardZeroStates : nullptr, selectedChoices ? &selectedChoices.get() : nullptr, &rewardVector,
1268 submatrix, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr, &b, produceScheduler);
1269
1270 // If the solve goal has relevant values, we need to adjust them.
1271 if (goal.hasRelevantValues()) {
1272 storm::storage::BitVector newRelevantValues(submatrix.getRowGroupCount());
1273 for (auto state : goal.relevantValues()) {
1274 if (qualitativeStateSets.maybeStates.get(state)) {
1275 newRelevantValues.set(result.getRowGroupAfterElimination(state));
1276 }
1277 }
1278 if (!newRelevantValues.empty()) {
1279 goal.setRelevantValues(std::move(newRelevantValues));
1280 }
1281 }
1282
1283 return result;
1284 } else {
1285 STORM_LOG_DEBUG("Not eliminating ECs as there are none.");
1286 computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b,
1287 oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
1288 return boost::none;
1289 }
1290}
1291
1292template<typename ValueType, typename SolutionType>
1294 storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& choiceRewards,
1295 std::vector<ValueType> const& oneStepTargetProbabilities) {
1296 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1297 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing upper reward bounds with interval models.");
1298 } else {
1299 // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17).
1300 if (direction == storm::OptimizationDirection::Minimize) {
1301 DsMpiMdpUpperRewardBoundsComputer<ValueType> dsmpi(submatrix, choiceRewards, oneStepTargetProbabilities);
1302 hintInformation.upperResultBounds = dsmpi.computeUpperBounds();
1303 } else {
1304 BaierUpperRewardBoundsComputer<ValueType> baier(submatrix, choiceRewards, oneStepTargetProbabilities);
1305 hintInformation.upperResultBound = baier.computeUpperBound();
1306 }
1307 }
1308}
1309
1310template<typename ValueType, typename SolutionType>
1311MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueType, SolutionType>::computeReachabilityRewardsHelper(
1313 storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
1314 std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const&
1315 totalStateRewardVectorGetter,
1316 storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler,
1317 std::function<storm::storage::BitVector()> const& zeroRewardStatesGetter, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter,
1318 ModelCheckerHint const& hint) {
1319 // Prepare resulting vector.
1320 std::vector<SolutionType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<SolutionType>());
1321
1322 // Determine which states have a reward that is infinity or less than infinity.
1323 QualitativeStateSetsReachabilityRewards qualitativeStateSets = getQualitativeStateSetsReachabilityRewards(
1324 goal, transitionMatrix, backwardTransitions, targetStates, hint, zeroRewardStatesGetter, zeroRewardChoicesGetter);
1325
1326 STORM_LOG_INFO("Preprocessing: " << qualitativeStateSets.infinityStates.getNumberOfSetBits() << " states with reward infinity, "
1327 << qualitativeStateSets.rewardZeroStates.getNumberOfSetBits() << " states with reward zero ("
1328 << qualitativeStateSets.maybeStates.getNumberOfSetBits() << " states remaining).");
1329
1330 storm::utility::vector::setVectorValues(result, qualitativeStateSets.infinityStates, storm::utility::infinity<SolutionType>());
1331
1332 // If requested, we will produce a scheduler.
1333 std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
1334 if (produceScheduler) {
1335 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1336 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support producing schedulers in this function with interval models.");
1337 } else {
1338 scheduler = std::make_unique<storm::storage::Scheduler<SolutionType>>(transitionMatrix.getRowGroupCount());
1339 }
1340 }
1341
1342 // Check if the values of the maybe states are relevant for the SolveGoal
1343 bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
1344
1345 // Check whether we need to compute exact rewards for some states.
1346 if (qualitative || maybeStatesNotRelevant) {
1347 STORM_LOG_INFO("The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
1348 // Set the values for all maybe-states to 1 to indicate that their reward values
1349 // are neither 0 nor infinity.
1350 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, storm::utility::one<SolutionType>());
1351 } else {
1352 if (!qualitativeStateSets.maybeStates.empty()) {
1353 // In this case we have to compute the reward values for the remaining states.
1354
1355 // Store the choices that lead to non-infinity values. If none, all choices im maybe states can be selected.
1356 boost::optional<storm::storage::BitVector> selectedChoices;
1357 if (!qualitativeStateSets.infinityStates.empty()) {
1358 selectedChoices = transitionMatrix.getRowFilter(qualitativeStateSets.maybeStates, ~qualitativeStateSets.infinityStates);
1359 }
1360
1361 // Obtain proper hint information either from the provided hint or from requirements of the solver.
1362 SparseMdpHintType<SolutionType> hintInformation = computeHints<ValueType, SolutionType>(
1363 env, SemanticSolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates,
1364 ~qualitativeStateSets.rewardZeroStates, qualitativeStateSets.rewardZeroStates, produceScheduler, selectedChoices);
1365
1366 // Declare the components of the equation system we will solve.
1368 std::vector<ValueType> b;
1369
1370 // If we need to compute upper bounds on the reward values, we need the one step probabilities
1371 // to a target state.
1372 boost::optional<std::vector<ValueType>> oneStepTargetProbabilities;
1373 if (hintInformation.getComputeUpperBounds()) {
1374 oneStepTargetProbabilities = std::vector<ValueType>();
1375 }
1376
1377 // If the hint information tells us that we have to eliminate MECs, we do so now.
1378 boost::optional<SparseMdpEndComponentInformation<ValueType>> ecInformation;
1379 if (hintInformation.getEliminateEndComponents()) {
1380 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1381 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models.");
1382 } else {
1384 goal, transitionMatrix, backwardTransitions, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter, submatrix, b,
1385 oneStepTargetProbabilities, produceScheduler);
1386 }
1387 } else {
1388 // Otherwise, we compute the standard equations.
1389 computeFixedPointSystemReachabilityRewards(goal, transitionMatrix, qualitativeStateSets, selectedChoices, totalStateRewardVectorGetter,
1390 submatrix, b, oneStepTargetProbabilities ? &oneStepTargetProbabilities.get() : nullptr);
1391 }
1392
1393 // If we need to compute upper bounds, do so now.
1394 if (hintInformation.getComputeUpperBounds()) {
1395 STORM_LOG_ASSERT(oneStepTargetProbabilities, "Expecting one step target probability vector to be available.");
1396 computeUpperRewardBounds(hintInformation, goal.direction(), submatrix, b, oneStepTargetProbabilities.get());
1397 }
1398
1399 // Now compute the results for the maybe states.
1400 MaybeStateResult<SolutionType> resultForMaybeStates =
1401 computeValuesForMaybeStates(env, std::move(goal), std::move(submatrix), b, produceScheduler, hintInformation);
1402
1403 // If we eliminated end components, we need to extract the result differently.
1404 if (ecInformation && ecInformation.get().getEliminatedEndComponents()) {
1405 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1406 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support eliminating end components with interval models.");
1407 } else {
1408 ecInformation.get().setValues(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1409 if (produceScheduler) {
1410 ecInformation.get().setScheduler(*scheduler, qualitativeStateSets.maybeStates, transitionMatrix, backwardTransitions,
1411 resultForMaybeStates.getScheduler());
1412 }
1413 }
1414 } else {
1415 // Set values of resulting vector according to result.
1416 storm::utility::vector::setVectorValues<SolutionType>(result, qualitativeStateSets.maybeStates, resultForMaybeStates.getValues());
1417 if (produceScheduler) {
1418 extractSchedulerChoices(*scheduler, transitionMatrix, resultForMaybeStates.getScheduler(), qualitativeStateSets.maybeStates,
1419 selectedChoices);
1420 }
1421 }
1422 }
1423 }
1424
1425 // Extend scheduler with choices for the states in the qualitative state sets.
1426 if (produceScheduler) {
1427 extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter);
1428 }
1429
1430 // Sanity check for created scheduler.
1431 STORM_LOG_ASSERT(!produceScheduler || scheduler, "Expected that a scheduler was obtained.");
1432 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || !scheduler->isPartialScheduler(), "Expected a fully defined scheduler");
1433 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isDeterministicScheduler(), "Expected a deterministic scheduler");
1434 STORM_LOG_ASSERT((!produceScheduler && !scheduler) || scheduler->isMemorylessScheduler(), "Expected a memoryless scheduler");
1435
1436 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1437 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result));
1438 } else {
1439 return MDPSparseModelCheckingHelperReturnType<SolutionType>(std::move(result), std::move(scheduler));
1440 }
1441}
1442
1443template<typename ValueType, typename SolutionType>
1446 storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates,
1447 storm::storage::BitVector const& conditionStates) {
1448 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
1449 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We do not support computing conditional probabilities with interval models.");
1450 } else {
1451 std::chrono::high_resolution_clock::time_point start = std::chrono::high_resolution_clock::now();
1452
1453 // For the max-case, we can simply take the given target states. For the min-case, however, we need to
1454 // find the MECs of non-target states and make them the new target states.
1455 storm::storage::BitVector fixedTargetStates;
1456 if (!goal.minimize()) {
1457 fixedTargetStates = targetStates;
1458 } else {
1459 fixedTargetStates = storm::storage::BitVector(targetStates.size());
1460 storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(transitionMatrix, backwardTransitions, ~targetStates);
1461 for (auto const& mec : mecDecomposition) {
1462 for (auto const& stateActionsPair : mec) {
1463 fixedTargetStates.set(stateActionsPair.first);
1464 }
1465 }
1466 }
1467
1468 storm::storage::BitVector allStates(fixedTargetStates.size(), true);
1469
1470 // Extend the target states by computing all states that have probability 1 to go to a target state
1471 // under *all* schedulers.
1472 fixedTargetStates =
1473 storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, allStates, fixedTargetStates);
1474
1475 // We solve the max-case and later adjust the result if the optimization direction was to minimize.
1476 storm::storage::BitVector initialStatesBitVector = goal.relevantValues();
1477 STORM_LOG_THROW(initialStatesBitVector.getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
1478 "Computing conditional probabilities in MDPs is only supported for models with exactly one initial state.");
1479 storm::storage::sparse::state_type initialState = *initialStatesBitVector.begin();
1480
1481 // Extend the condition states by computing all states that have probability 1 to go to a condition state
1482 // under *all* schedulers.
1483 storm::storage::BitVector extendedConditionStates =
1484 storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, allStates, conditionStates);
1485
1486 STORM_LOG_DEBUG("Computing probabilities to satisfy condition.");
1487 std::chrono::high_resolution_clock::time_point conditionStart = std::chrono::high_resolution_clock::now();
1488 std::vector<ValueType> conditionProbabilities =
1489 std::move(computeUntilProbabilities(env, OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, extendedConditionStates,
1490 false, false)
1491 .values);
1492 std::chrono::high_resolution_clock::time_point conditionEnd = std::chrono::high_resolution_clock::now();
1493 STORM_LOG_DEBUG("Computed probabilities to satisfy for condition in "
1494 << std::chrono::duration_cast<std::chrono::milliseconds>(conditionEnd - conditionStart).count() << "ms.");
1495
1496 // If the conditional probability is undefined for the initial state, we return directly.
1497 if (storm::utility::isZero(conditionProbabilities[initialState])) {
1498 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, storm::utility::infinity<ValueType>()));
1499 }
1500
1501 STORM_LOG_DEBUG("Computing probabilities to reach target.");
1502 std::chrono::high_resolution_clock::time_point targetStart = std::chrono::high_resolution_clock::now();
1503 std::vector<ValueType> targetProbabilities = std::move(
1504 computeUntilProbabilities(env, OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, fixedTargetStates, false, false)
1505 .values);
1506 std::chrono::high_resolution_clock::time_point targetEnd = std::chrono::high_resolution_clock::now();
1507 STORM_LOG_DEBUG("Computed probabilities to reach target in " << std::chrono::duration_cast<std::chrono::milliseconds>(targetEnd - targetStart).count()
1508 << "ms.");
1509
1510 storm::storage::BitVector statesWithProbabilityGreater0E(transitionMatrix.getRowGroupCount(), true);
1512 for (auto const& element : conditionProbabilities) {
1513 if (storm::utility::isZero(element)) {
1514 statesWithProbabilityGreater0E.set(state, false);
1515 }
1516 ++state;
1517 }
1518
1519 // Determine those states that need to be equipped with a restart mechanism.
1520 STORM_LOG_DEBUG("Computing problematic states.");
1521 storm::storage::BitVector pureResetStates = storm::utility::graph::performProb0A(backwardTransitions, allStates, extendedConditionStates);
1523 transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, allStates, extendedConditionStates | fixedTargetStates);
1524
1525 // Otherwise, we build the transformed MDP.
1526 storm::storage::BitVector relevantStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStatesBitVector, allStates,
1527 extendedConditionStates | fixedTargetStates | pureResetStates);
1528 STORM_LOG_TRACE("Found " << relevantStates.getNumberOfSetBits() << " relevant states for conditional probability computation.");
1529 std::vector<uint_fast64_t> numberOfStatesBeforeRelevantStates = relevantStates.getNumberOfSetBitsBeforeIndices();
1530 storm::storage::sparse::state_type newGoalState = relevantStates.getNumberOfSetBits();
1531 storm::storage::sparse::state_type newStopState = newGoalState + 1;
1532 storm::storage::sparse::state_type newFailState = newStopState + 1;
1533
1534 // Build the transitions of the (relevant) states of the original model.
1535 storm::storage::SparseMatrixBuilder<ValueType> builder(0, newFailState + 1, 0, true, true);
1536 uint_fast64_t currentRow = 0;
1537 for (auto state : relevantStates) {
1538 builder.newRowGroup(currentRow);
1539 if (fixedTargetStates.get(state)) {
1540 if (!storm::utility::isZero(conditionProbabilities[state])) {
1541 builder.addNextValue(currentRow, newGoalState, conditionProbabilities[state]);
1542 }
1543 if (!storm::utility::isOne(conditionProbabilities[state])) {
1544 builder.addNextValue(currentRow, newFailState, storm::utility::one<ValueType>() - conditionProbabilities[state]);
1545 }
1546 ++currentRow;
1547 } else if (extendedConditionStates.get(state)) {
1548 if (!storm::utility::isZero(targetProbabilities[state])) {
1549 builder.addNextValue(currentRow, newGoalState, targetProbabilities[state]);
1550 }
1551 if (!storm::utility::isOne(targetProbabilities[state])) {
1552 builder.addNextValue(currentRow, newStopState, storm::utility::one<ValueType>() - targetProbabilities[state]);
1553 }
1554 ++currentRow;
1555 } else if (pureResetStates.get(state)) {
1556 builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
1557 ++currentRow;
1558 } else {
1559 for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[state]; row < transitionMatrix.getRowGroupIndices()[state + 1]; ++row) {
1560 for (auto const& successorEntry : transitionMatrix.getRow(row)) {
1561 builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[successorEntry.getColumn()], successorEntry.getValue());
1562 }
1563 ++currentRow;
1564 }
1565 if (problematicStates.get(state)) {
1566 builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
1567 ++currentRow;
1568 }
1569 }
1570 }
1571
1572 // Now build the transitions of the newly introduced states.
1573 builder.newRowGroup(currentRow);
1574 builder.addNextValue(currentRow, newGoalState, storm::utility::one<ValueType>());
1575 ++currentRow;
1576 builder.newRowGroup(currentRow);
1577 builder.addNextValue(currentRow, newStopState, storm::utility::one<ValueType>());
1578 ++currentRow;
1579 builder.newRowGroup(currentRow);
1580 builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
1581 ++currentRow;
1582
1583 std::chrono::high_resolution_clock::time_point end = std::chrono::high_resolution_clock::now();
1584 STORM_LOG_DEBUG("Computed transformed model in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
1585
1586 // Finally, build the matrix and dispatch the query as a reachability query.
1587 STORM_LOG_DEBUG("Computing conditional probabilties.");
1588 storm::storage::BitVector newGoalStates(newFailState + 1);
1589 newGoalStates.set(newGoalState);
1590 storm::storage::SparseMatrix<ValueType> newTransitionMatrix = builder.build();
1591 STORM_LOG_DEBUG("Transformed model has " << newTransitionMatrix.getRowGroupCount() << " states and " << newTransitionMatrix.getNonzeroEntryCount()
1592 << " transitions.");
1593 storm::storage::SparseMatrix<ValueType> newBackwardTransitions = newTransitionMatrix.transpose(true);
1594
1596 if (goal.minimize()) {
1597 goal.oneMinus();
1598 }
1599
1600 std::chrono::high_resolution_clock::time_point conditionalStart = std::chrono::high_resolution_clock::now();
1601 std::vector<ValueType> goalProbabilities =
1602 std::move(computeUntilProbabilities(env, std::move(goal), newTransitionMatrix, newBackwardTransitions,
1603 storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false)
1604 .values);
1605 std::chrono::high_resolution_clock::time_point conditionalEnd = std::chrono::high_resolution_clock::now();
1606 STORM_LOG_DEBUG("Computed conditional probabilities in transformed model in "
1607 << std::chrono::duration_cast<std::chrono::milliseconds>(conditionalEnd - conditionalStart).count() << "ms.");
1608
1609 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(
1610 initialState, dir == OptimizationDirection::Maximize
1611 ? goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]]
1612 : storm::utility::one<ValueType>() - goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]]));
1613 }
1614}
1615
1616template class SparseMdpPrctlHelper<double>;
1618 storm::storage::SparseMatrix<double> const& transitionMatrix,
1620 uint_fast64_t stepCount);
1622 storm::storage::SparseMatrix<double> const& transitionMatrix,
1624 uint_fast64_t stepBound);
1626 Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& transitionMatrix,
1628 storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint);
1630 Environment const& env, storm::solver::SolveGoal<double>&& goal, storm::storage::SparseMatrix<double> const& transitionMatrix,
1631 storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, bool qualitative,
1632 bool produceScheduler, ModelCheckerHint const& hint);
1633
1634#ifdef STORM_HAVE_CARL
1636template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(
1638 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepCount);
1639template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(
1641 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound);
1644 storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions,
1645 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative,
1646 bool produceScheduler, ModelCheckerHint const& hint);
1649 storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions,
1650 storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, bool qualitative, bool produceScheduler,
1651 ModelCheckerHint const& hint);
1652#endif
1653
1657 storm::models::sparse::StandardRewardModel<storm::Interval> const& rewardModel, uint_fast64_t stepCount);
1660 storm::models::sparse::StandardRewardModel<storm::Interval> const& rewardModel, uint_fast64_t stepBound);
1664 storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint);
1668 bool qualitative, bool produceScheduler, ModelCheckerHint const& hint);
1669
1670} // namespace helper
1671} // namespace modelchecker
1672} // 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.
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)
void oneMinus()
Flips the comparison type, the direction, and computes the new threshold as 1 - old threshold.
Definition SolveGoal.cpp:57
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:18
void complement()
Negates all bits 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.
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
size_t size() const
Retrieves the number of bits this bit vector can store.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
std::vector< uint_fast64_t > getNumberOfSetBitsBeforeIndices() const
Retrieves a vector that holds at position i the number of bits set before index i.
bool get(uint_fast64_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 can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
A class that holds a possibly non-square matrix in the compressed row storage format.
const_rows getRow(index_type row) const
Returns an object representing the given row.
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...
storm::storage::SparseMatrix< value_type > transpose(bool joinGroups=false, bool keepZeros=false) const
Transposes the matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
index_type getNonzeroEntryCount() const
Returns the cached number of nonzero entries in 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:29
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_DEBUG(message)
Definition logging.h:23
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_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)
SettingsType const & getModule()
Get module.
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:826
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:490
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:542
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceFilter)
Performs a forward depth-first search through the underlying graph structure to identify the states t...
Definition graph.cpp:48
storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps, boost::optional< storm::storage::BitVector > const &choiceConstraint)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under any pos...
Definition graph.cpp:848
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:615
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:988
storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound, uint_fast64_t maximalSteps)
Computes the sets of states that have probability greater 0 of satisfying phi until psi under at leas...
Definition graph.cpp:680
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:740
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:383
storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 of satisfying phi until psi under at least one po...
Definition graph.cpp:967
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:593
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:1070
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:748
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:599
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:36
bool isZero(ValueType const &a)
Definition constants.cpp:41
bool isInfinity(ValueType const &a)
Definition constants.cpp:71
LabParser.cpp.
Definition cli.cpp:18
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