Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseMdpPrctlModelChecker.cpp
Go to the documentation of this file.
2
24#include "storm/utility/graph.h"
27
28namespace storm {
29namespace modelchecker {
30template<typename SparseMdpModelType>
32 : SparsePropositionalModelChecker<SparseMdpModelType>(model) {
33 // Intentionally left empty.
34}
35
36template<typename SparseMdpModelType>
38 bool* requiresSingleInitialState) {
39 storm::logic::Formula const& formula = checkTask.getFormula();
40 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
42 return true;
43 }
45 return true;
46 }
47 } else {
63 return true;
64 } else if (checkTask.isOnlyInitialStatesRelevantSet()) {
65 auto multiObjectiveFragment = storm::logic::multiObjective()
66 .setTimeAllowed(true)
77 auto lexObjectiveFragment = storm::logic::lexObjective()
89
90 if (formula.isInFragment(multiObjectiveFragment) || formula.isInFragment(storm::logic::quantiles()) || formula.isInFragment(lexObjectiveFragment)) {
91 if (requiresSingleInitialState) {
92 *requiresSingleInitialState = true;
93 }
94 return true;
95 }
96 }
97 }
98 return false;
99}
100
101template<typename SparseMdpModelType>
103 bool requiresSingleInitialState = false;
104 if (canHandleStatic(checkTask, &requiresSingleInitialState)) {
105 return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1;
106 } else {
107 return false;
108 }
109}
110
111template<typename SparseMdpModelType>
114 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
115 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented bounded until with intervals");
116 return nullptr;
117 } else {
118 storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
119 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
120 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
121 if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) {
122 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException,
123 "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model.");
124 STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking non-trivial bounded until formulas is not optimized w.r.t. qualitative queries");
126 if (checkTask.isBoundSet()) {
127 opInfo.bound = checkTask.getBound();
128 }
129 auto formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(checkTask.getFormula().asSharedPointer(), opInfo);
130 helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
132 env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
133 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
134 } else {
135 STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
136 STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException,
137 "Formula lower step bound must be discrete/integral.");
138 STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException,
139 "Formula needs to have discrete upper time bound.");
140 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
141 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
142 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
143 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
145 std::vector<SolutionType> numericResult =
146 helper.compute(env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
147 this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(),
148 pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint());
149 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
150 }
151 }
152}
153
154template<typename SparseMdpModelType>
157 storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
158 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
159 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
160 std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
161 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
163 env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
164 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
165}
166
167template<typename SparseMdpModelType>
170 storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
171 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
172 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
173 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
174 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
175 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
176 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
178 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
179 this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
180 checkTask.isProduceSchedulersSet(), checkTask.getHint());
181 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
182 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
183 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
184 }
185 return result;
186}
187
188template<typename SparseMdpModelType>
191 storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
192 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
193 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
194 std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
195 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
197 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
198 this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet());
199 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
200 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
201 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
202 }
203 return result;
204}
205
206template<typename SparseMdpModelType>
209 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
210 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented automata-props with intervals");
211 } else {
212 storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
213
214 storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(this->getModel().getTransitionMatrix());
216
217 auto formulaChecker = [&](storm::logic::Formula const& formula) {
218 return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
219 };
220 auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
221 std::vector<SolutionType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
222
223 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
224 if (checkTask.isProduceSchedulersSet()) {
225 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
226 std::make_unique<storm::storage::Scheduler<SolutionType>>(helper.extractScheduler(this->getModel())));
227 }
228
229 return result;
230 }
231}
232
233template<typename SparseMdpModelType>
236 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
237 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LTL with intervals");
238 } else {
239 storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
240
241 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
242 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
243
244 storm::modelchecker::helper::SparseLTLHelper<SolutionType, true> helper(this->getModel().getTransitionMatrix());
246
247 auto formulaChecker = [&](storm::logic::Formula const& formula) {
248 return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
249 };
250 std::vector<SolutionType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);
251
252 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
253 if (checkTask.isProduceSchedulersSet()) {
254 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
255 std::make_unique<storm::storage::Scheduler<SolutionType>>(helper.extractScheduler(this->getModel())));
256 }
257
258 return result;
259 }
260}
261
262template<typename SparseMdpModelType>
265 storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
266 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
267 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
268 STORM_LOG_THROW(this->getModel().getInitialStates().hasUniqueSetBit(), storm::exceptions::InvalidPropertyException,
269 "Cannot compute conditional probabilities on MDPs with more than one initial state.");
270 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException,
271 "Conditional probabilities can only be computed for the initial states of the model.");
272 STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
273 "Illegal conditional probability formula.");
274 STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
275 "Illegal conditional probability formula.");
276
277 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, conditionalFormula.getSubformula().asEventuallyFormula().getSubformula());
278 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula());
279 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
280 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
281 if constexpr (std::is_same_v<storm::Interval, ValueType>) {
282 throw exceptions::NotImplementedException() << "Conditional Probabilities are not supported with interval models";
283 } else {
285 this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(),
286 leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector());
287 }
288}
289
290template<typename SparseMdpModelType>
293 storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
294 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
295 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
296 if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) {
297 if constexpr (std::is_same_v<storm::Interval, ValueType>) {
298 throw exceptions::NotImplementedException() << "Multi-reward bounded is not supported with interval models";
299 } else {
300 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException,
301 "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model.");
302 STORM_LOG_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException,
303 "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given.");
304 STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries");
306 if (checkTask.isBoundSet()) {
307 opInfo.bound = checkTask.getBound();
308 }
309 auto formula = std::make_shared<storm::logic::RewardOperatorFormula>(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo);
310 helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
312 env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
313 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
314 }
315 } else {
316 STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
317 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
319 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
320 rewardPathFormula.getNonStrictBound<uint64_t>());
321 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
322 }
323}
324
325template<>
326std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>::computeDiscountedCumulativeRewards(
328 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Discounted properties are not implemented for interval models.");
329}
330
331template<typename SparseMdpModelType>
334 storm::logic::DiscountedCumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
335 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
336 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
337 STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
338 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
340 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
341 rewardPathFormula.getNonStrictBound<uint64_t>(), rewardPathFormula.getDiscountFactor<ValueType>());
342 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
343}
344
345template<typename SparseMdpModelType>
348 storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
349 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
350 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
351 STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
353 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
354 checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""),
355 rewardPathFormula.getBound<uint64_t>());
356 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
357}
358
359template<typename SparseMdpModelType>
362 storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
363 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
364 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
365 std::unique_ptr<CheckResult> subResultPointer = this->check(env, eventuallyFormula.getSubformula());
366 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
367 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
369 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
370 this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
371 checkTask.isProduceSchedulersSet(), checkTask.getHint());
372 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
373 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
374 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
375 }
376 return result;
377}
378
379template<typename SparseMdpModelType>
382 storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
383 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
384 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
385 std::unique_ptr<CheckResult> subResultPointer = this->check(env, eventuallyFormula.getSubformula());
386 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
388 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
389 this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(),
390 checkTask.getHint());
391 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
392 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
393 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
394 }
395 return result;
396}
397
398template<typename SparseMdpModelType>
401 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
402 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
403 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
405 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
406 this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint());
407 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
408 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
409 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
410 }
411 return result;
412}
413
414template<>
415std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>::computeDiscountedTotalRewards(
417 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Discounted properties are not implemented for interval models.");
418}
419
420template<typename SparseMdpModelType>
423 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
424 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
425 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
426 storm::logic::DiscountedTotalRewardFormula const& rewardPathFormula = checkTask.getFormula();
427 auto discountFactor = rewardPathFormula.getDiscountFactor<ValueType>();
429 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
430 this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), discountFactor,
431 checkTask.getHint());
432 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
433 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
434 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
435 }
436 return result;
437}
438
439template<typename SparseMdpModelType>
442 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
443 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LRA probabilities with intervals");
444 } else {
445 storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
446 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
447 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
448 std::unique_ptr<CheckResult> subResultPointer = this->check(env, stateFormula);
449 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
450
453 auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector());
454
455 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(values)));
456 if (checkTask.isProduceSchedulersSet()) {
457 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
459 }
460 return result;
461 }
462}
463
464template<typename SparseMdpModelType>
467 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
468 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lra with intervals");
469 } else {
470 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
471 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
472 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
475 auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
476 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(values)));
477 if (checkTask.isProduceSchedulersSet()) {
478 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
480 }
481 return result;
482 }
483}
484
485template<typename SparseMdpModelType>
488 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
489 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented multi-objective with intervals");
490 } else {
491 return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula(), checkTask.isProduceSchedulersSet());
492 }
493}
494
495template<class SparseMdpModelType>
498 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
499 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lexicographic model checking with intervals");
500 } else {
501 auto formulaChecker = [&](storm::logic::Formula const& formula) {
502 return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
503 };
504 auto ret = lexicographic::check(env, this->getModel(), checkTask, formulaChecker);
505 std::unique_ptr<CheckResult> result(new LexicographicCheckResult<SolutionType>(ret.values, *this->getModel().getInitialStates().begin()));
506 return result;
507 }
508}
509
510template<typename SparseMdpModelType>
513 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
514 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented quantile formulas with intervals");
515 } else {
516 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException,
517 "Computing quantiles is only supported for the initial states of a model.");
518 STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException,
519 "Quantiles not supported on models with multiple initial states.");
520 uint64_t initialState = *this->getModel().getInitialStates().begin();
521
522 helper::rewardbounded::QuantileHelper<SparseMdpModelType> qHelper(this->getModel(), checkTask.getFormula());
523 auto res = qHelper.computeQuantile(env);
524
525 if (res.size() == 1 && res.front().size() == 1) {
526 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(initialState, std::move(res.front().front())));
527 } else {
528 return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<SolutionType>(initialState, std::move(res)));
529 }
530 }
531}
532
536} // namespace modelchecker
537} // namespace storm
Formula const & getRightSubformula() const
Formula const & getLeftSubformula() const
ValueType getNonStrictLowerBound(unsigned i=0) const
TimeBoundReference const & getTimeBoundReference(unsigned i=0) const
ValueType getNonStrictUpperBound(unsigned i=0) const
bool hasIntegerUpperBound(unsigned i=0) const
bool hasIntegerLowerBound(unsigned i=0) const
Formula const & getConditionFormula() const
Formula const & getSubformula() const
TimeBoundReference const & getTimeBoundReference() const
storm::expressions::Expression const & getDiscountFactor() const
storm::expressions::Expression const & getDiscountFactor() const
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:341
bool isInFragment(FragmentSpecification const &fragment) const
Definition Formula.cpp:204
virtual bool isEventuallyFormula() const
Definition Formula.cpp:88
FragmentSpecification & setStepBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setRewardAccumulationAllowed(bool newValue)
FragmentSpecification & setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue)
FragmentSpecification & setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setTimeOperatorsAllowed(bool newValue)
FragmentSpecification & setTimeBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setTotalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setDiscountedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setConditionalProbabilityFormulasAllowed(bool newValue)
FragmentSpecification & setRewardBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setLongRunAverageRewardFormulasAllowed(bool newValue)
FragmentSpecification & setLongRunAverageProbabilitiesAllowed(bool newValue)
FragmentSpecification & setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setHOAPathFormulasAllowed(bool newValue)
FragmentSpecification & setReachbilityTimeFormulasAllowed(bool newValue)
FragmentSpecification & setDiscountedTotalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setTimeAllowed(bool newValue)
FragmentSpecification & setStepBoundedCumulativeRewardFormulasAllowed(bool newValue)
const ap_to_formula_map & getAPMapping() const
std::shared_ptr< storm::automata::DeterministicAutomaton > readAutomaton() const
storm::expressions::Expression const & getBound() const
Formula const & getSubformula() const
ExplicitQualitativeCheckResult & asExplicitQualitativeCheckResult()
bool isBoundSet() const
Retrieves whether there is a bound with which the values for the states will be compared.
Definition CheckTask.h:219
bool isOptimizationDirectionSet() const
Retrieves whether an optimization direction was set.
Definition CheckTask.h:147
bool isRewardModelSet() const
Retrieves whether a reward model was set.
Definition CheckTask.h:190
bool isQualitativeSet() const
Retrieves whether the computation only needs to be performed qualitatively, because the values will o...
Definition CheckTask.h:257
std::string const & getRewardModel() const
Retrieves the reward model over which to perform the checking (if set).
Definition CheckTask.h:197
FormulaType const & getFormula() const
Retrieves the formula from this task.
Definition CheckTask.h:140
ModelCheckerHint const & getHint() const
Retrieves a hint that might contain information that speeds up the modelchecking process (if supporte...
Definition CheckTask.h:293
bool isProduceSchedulersSet() const
Retrieves whether scheduler(s) are to be produced (if supported).
Definition CheckTask.h:279
storm::logic::Bound const & getBound() const
Retrieves the bound (if set).
Definition CheckTask.h:242
storm::OptimizationDirection const & getOptimizationDirection() const
Retrieves the optimization direction (if set).
Definition CheckTask.h:154
bool isOnlyInitialStatesRelevantSet() const
Retrieves whether only the initial states are relevant in the computation.
Definition CheckTask.h:204
virtual std::unique_ptr< CheckResult > computeLongRunAverageProbabilities(Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeCumulativeRewards(Environment const &env, CheckTask< storm::logic::CumulativeRewardFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeLongRunAverageRewards(Environment const &env, CheckTask< storm::logic::LongRunAverageRewardFormula, SolutionType > const &checkTask) override
static bool canHandleStatic(CheckTask< storm::logic::Formula, SolutionType > const &checkTask, bool *requiresSingleInitialState=nullptr)
Returns false, if this task can certainly not be handled by this model checker (independent of the co...
virtual std::unique_ptr< CheckResult > checkMultiObjectiveFormula(Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeReachabilityTimes(Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeDiscountedCumulativeRewards(Environment const &env, CheckTask< storm::logic::DiscountedCumulativeRewardFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeLTLProbabilities(Environment const &env, CheckTask< storm::logic::PathFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeGloballyProbabilities(Environment const &env, CheckTask< storm::logic::GloballyFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeUntilProbabilities(Environment const &env, CheckTask< storm::logic::UntilFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > checkQuantileFormula(Environment const &env, CheckTask< storm::logic::QuantileFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > checkLexObjectiveFormula(Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask) override
virtual bool canHandle(CheckTask< storm::logic::Formula, SolutionType > const &checkTask) const override
Determines whether the model checker can handle the given verification task.
virtual std::unique_ptr< CheckResult > computeReachabilityRewards(Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeHOAPathProbabilities(Environment const &env, CheckTask< storm::logic::HOAPathFormula, SolutionType > const &checkTask) override
typename std::conditional< std::is_same_v< ValueType, storm::Interval >, double, ValueType >::type SolutionType
virtual std::unique_ptr< CheckResult > computeInstantaneousRewards(Environment const &env, CheckTask< storm::logic::InstantaneousRewardFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeConditionalProbabilities(Environment const &env, CheckTask< storm::logic::ConditionalFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeNextProbabilities(Environment const &env, CheckTask< storm::logic::NextFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeDiscountedTotalRewards(Environment const &env, CheckTask< storm::logic::DiscountedTotalRewardFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeTotalRewards(Environment const &env, CheckTask< storm::logic::TotalRewardFormula, SolutionType > const &checkTask) override
virtual std::unique_ptr< CheckResult > computeBoundedUntilProbabilities(Environment const &env, CheckTask< storm::logic::BoundedUntilFormula, SolutionType > const &checkTask) override
std::vector< ValueType > computeLongRunAverageRewards(Environment const &env, storm::models::sparse::StandardRewardModel< ValueType > const &rewardModel)
Computes the long run average rewards, i.e., the average reward collected per time unit.
std::vector< ValueType > computeLongRunAverageProbabilities(Environment const &env, storm::storage::BitVector const &psiStates)
Computes the long run average probabilities, i.e., the fraction of the time we are in a psiState.
Helper class for LTL model checking.
std::vector< ValueType > computeLTLProbabilities(Environment const &env, storm::logic::PathFormula const &formula, CheckFormulaCallback const &formulaChecker)
Computes the LTL probabilities.
storm::storage::Scheduler< ValueType > extractScheduler(storm::models::sparse::Model< ValueType > const &model)
static std::map< std::string, storm::storage::BitVector > computeApSets(std::map< std::string, std::shared_ptr< storm::logic::Formula const > > const &extracted, CheckFormulaCallback const &formulaChecker)
Computes the states that are satisfying the AP.
std::vector< ValueType > computeDAProductProbabilities(Environment const &env, storm::automata::DeterministicAutomaton const &da, std::map< std::string, storm::storage::BitVector > &apSatSets)
Computes the (maximizing) probabilities for the constructed DA product.
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeReachabilityTimes(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 &targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const &hint=ModelCheckerHint())
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 > computeDiscountedCumulativeRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, RewardModelType const &rewardModel, uint_fast64_t stepBound, ValueType discountFactor)
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())
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeDiscountedTotalRewards(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, ValueType discountFactor, ModelCheckerHint const &hint=ModelCheckerHint())
static MDPSparseModelCheckingHelperReturnType< SolutionType > computeReachabilityRewards(Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, RewardModelType const &rewardModel, storm::storage::BitVector const &targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const &hint=ModelCheckerHint())
Helper class for model checking queries that depend on the long run behavior of the (nondeterministic...
std::vector< ValueType > compute(Environment const &env, storm::solver::SolveGoal< ValueType > &&goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const &hint=ModelCheckerHint())
std::vector< std::vector< ValueType > > computeQuantile(Environment const &env)
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
FragmentSpecification prctlstar()
FragmentSpecification propositional()
FragmentSpecification lexObjective()
FragmentSpecification multiObjective()
FragmentSpecification reachability()
FragmentSpecification quantiles()
void setInformationFromCheckTaskNondeterministic(HelperType &helper, storm::modelchecker::CheckTask< FormulaType, typename ModelType::ValueType > const &checkTask, ModelType const &model)
Forwards relevant information stored in the given CheckTask to the given helper.
helper::MDPSparseModelCheckingHelperReturnType< ValueType > check(Environment const &, SparseModelType const &model, CheckTask< storm::logic::MultiObjectiveFormula, ValueType > const &checkTask, CheckFormulaCallback const &formulaChecker)
check a lexicographic LTL-formula
std::unique_ptr< CheckResult > performMultiObjectiveModelChecking(Environment const &env, SparseModelType const &model, storm::logic::MultiObjectiveFormula const &formula, bool produceScheduler)
std::unique_ptr< CheckResult > computeConditionalProbabilities(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 &targetStates, storm::storage::BitVector const &conditionStates)
FilteredRewardModel< RewardModelType > createFilteredRewardModel(RewardModelType const &baseRewardModel, storm::logic::RewardAccumulation const &acc, bool isDiscreteTimeModel)
LabParser.cpp.
boost::optional< Bound > bound