Storm 1.10.0.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 {
61 return true;
62 } else if (checkTask.isOnlyInitialStatesRelevantSet()) {
63 auto multiObjectiveFragment = storm::logic::multiObjective()
64 .setTimeAllowed(true)
75 auto lexObjectiveFragment = storm::logic::lexObjective()
87
88 if (formula.isInFragment(multiObjectiveFragment) || formula.isInFragment(storm::logic::quantiles()) || formula.isInFragment(lexObjectiveFragment)) {
89 if (requiresSingleInitialState) {
90 *requiresSingleInitialState = true;
91 }
92 return true;
93 }
94 }
95 }
96 return false;
97}
98
99template<typename SparseMdpModelType>
101 bool requiresSingleInitialState = false;
102 if (canHandleStatic(checkTask, &requiresSingleInitialState)) {
103 return !requiresSingleInitialState || this->getModel().getInitialStates().getNumberOfSetBits() == 1;
104 } else {
105 return false;
106 }
107}
108
109template<typename SparseMdpModelType>
112 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
113 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented bounded until with intervals");
114 return nullptr;
115 } else {
116 storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
117 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
118 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
119 if (pathFormula.isMultiDimensional() || pathFormula.getTimeBoundReference().isRewardBound()) {
120 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException,
121 "Checking non-trivial bounded until probabilities can only be computed for the initial states of the model.");
122 STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking non-trivial bounded until formulas is not optimized w.r.t. qualitative queries");
124 if (checkTask.isBoundSet()) {
125 opInfo.bound = checkTask.getBound();
126 }
127 auto formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(checkTask.getFormula().asSharedPointer(), opInfo);
128 helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
130 env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
131 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
132 } else {
133 STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
134 STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException,
135 "Formula lower step bound must be discrete/integral.");
136 STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException,
137 "Formula needs to have discrete upper time bound.");
138 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
139 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
140 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
141 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
143 std::vector<SolutionType> numericResult =
144 helper.compute(env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
145 this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(),
146 pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint());
147 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
148 }
149 }
150}
151
152template<typename SparseMdpModelType>
155 storm::logic::NextFormula const& pathFormula = checkTask.getFormula();
156 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
157 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
158 std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
159 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
161 env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
162 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
163}
164
165template<typename SparseMdpModelType>
168 storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
169 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
170 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
171 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
172 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
173 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
174 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
176 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
177 this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
178 checkTask.isProduceSchedulersSet(), checkTask.getHint());
179 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
180 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
181 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
182 }
183 return result;
184}
185
186template<typename SparseMdpModelType>
189 storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
190 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
191 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
192 std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
193 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
195 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
196 this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet());
197 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
198 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
199 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
200 }
201 return result;
202}
203
204template<typename SparseMdpModelType>
207 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
208 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented automata-props with intervals");
209 } else {
210 storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
211
212 storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(this->getModel().getTransitionMatrix());
214
215 auto formulaChecker = [&](storm::logic::Formula const& formula) {
216 return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
217 };
218 auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
219 std::vector<SolutionType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
220
221 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
222 if (checkTask.isProduceSchedulersSet()) {
223 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
224 std::make_unique<storm::storage::Scheduler<SolutionType>>(helper.extractScheduler(this->getModel())));
225 }
226
227 return result;
228 }
229}
230
231template<typename SparseMdpModelType>
234 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
235 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LTL with intervals");
236 } else {
237 storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
238
239 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
240 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
241
242 storm::modelchecker::helper::SparseLTLHelper<SolutionType, true> helper(this->getModel().getTransitionMatrix());
244
245 auto formulaChecker = [&](storm::logic::Formula const& formula) {
246 return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
247 };
248 std::vector<SolutionType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);
249
250 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
251 if (checkTask.isProduceSchedulersSet()) {
252 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
253 std::make_unique<storm::storage::Scheduler<SolutionType>>(helper.extractScheduler(this->getModel())));
254 }
255
256 return result;
257 }
258}
259
260template<typename SparseMdpModelType>
263 storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
264 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
265 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
266 STORM_LOG_THROW(this->getModel().getInitialStates().hasUniqueSetBit(), storm::exceptions::InvalidPropertyException,
267 "Cannot compute conditional probabilities on MDPs with more than one initial state.");
268 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException,
269 "Conditional probabilities can only be computed for the initial states of the model.");
270 STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
271 "Illegal conditional probability formula.");
272 STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
273 "Illegal conditional probability formula.");
274
275 std::unique_ptr<CheckResult> leftResultPointer = this->check(env, conditionalFormula.getSubformula().asEventuallyFormula().getSubformula());
276 std::unique_ptr<CheckResult> rightResultPointer = this->check(env, conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula());
277 ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
278 ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
279 if constexpr (std::is_same_v<storm::Interval, ValueType>) {
280 throw exceptions::NotImplementedException() << "Conditional Probabilities are not supported with interval models";
281 } else {
283 this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(),
284 leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector());
285 }
286}
287
288template<typename SparseMdpModelType>
291 storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
292 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
293 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
294 if (rewardPathFormula.isMultiDimensional() || rewardPathFormula.getTimeBoundReference().isRewardBound()) {
295 if constexpr (std::is_same_v<storm::Interval, ValueType>) {
296 throw exceptions::NotImplementedException() << "Multi-reward bounded is not supported with interval models";
297 } else {
298 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException,
299 "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model.");
300 STORM_LOG_THROW(!checkTask.getFormula().hasRewardAccumulation(), storm::exceptions::InvalidOperationException,
301 "Checking reward bounded cumulative reward formulas is not supported if reward accumulations are given.");
302 STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries");
304 if (checkTask.isBoundSet()) {
305 opInfo.bound = checkTask.getBound();
306 }
307 auto formula = std::make_shared<storm::logic::RewardOperatorFormula>(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo);
308 helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
310 env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
311 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
312 }
313 } else {
314 STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
315 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
317 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), rewardModel.get(),
318 rewardPathFormula.getNonStrictBound<uint64_t>());
319 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
320 }
321}
322
323template<typename SparseMdpModelType>
326 storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();
327 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
328 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
329 STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
331 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
332 checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""),
333 rewardPathFormula.getBound<uint64_t>());
334 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
335}
336
337template<typename SparseMdpModelType>
340 storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
341 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
342 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
343 std::unique_ptr<CheckResult> subResultPointer = this->check(env, eventuallyFormula.getSubformula());
344 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
345 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
347 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
348 this->getModel().getBackwardTransitions(), rewardModel.get(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
349 checkTask.isProduceSchedulersSet(), checkTask.getHint());
350 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
351 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
352 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
353 }
354 return result;
355}
356
357template<typename SparseMdpModelType>
360 storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
361 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
362 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
363 std::unique_ptr<CheckResult> subResultPointer = this->check(env, eventuallyFormula.getSubformula());
364 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
366 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
367 this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(),
368 checkTask.getHint());
369 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
370 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
371 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
372 }
373 return result;
374}
375
376template<typename SparseMdpModelType>
379 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
380 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
381 auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);
383 env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
384 this->getModel().getBackwardTransitions(), rewardModel.get(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint());
385 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
386 if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
387 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
388 }
389 return result;
390}
391
392template<typename SparseMdpModelType>
395 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
396 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented LRA probabilities with intervals");
397 } else {
398 storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
399 STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException,
400 "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
401 std::unique_ptr<CheckResult> subResultPointer = this->check(env, stateFormula);
402 ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
403
406 auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector());
407
408 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(values)));
409 if (checkTask.isProduceSchedulersSet()) {
410 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
412 }
413 return result;
414 }
415}
416
417template<typename SparseMdpModelType>
420 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
421 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lra with intervals");
422 } else {
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);
428 auto values = helper.computeLongRunAverageRewards(env, rewardModel.get());
429 std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(values)));
430 if (checkTask.isProduceSchedulersSet()) {
431 result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(
433 }
434 return result;
435 }
436}
437
438template<typename SparseMdpModelType>
441 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
442 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented multi-objective with intervals");
443 } else {
444 return multiobjective::performMultiObjectiveModelChecking(env, this->getModel(), checkTask.getFormula());
445 }
446}
447
448template<class SparseMdpModelType>
451 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
452 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented lexicographic model checking with intervals");
453 } else {
454 auto formulaChecker = [&](storm::logic::Formula const& formula) {
455 return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
456 };
457 auto ret = lexicographic::check(env, this->getModel(), checkTask, formulaChecker);
458 std::unique_ptr<CheckResult> result(new LexicographicCheckResult<SolutionType>(ret.values, *this->getModel().getInitialStates().begin()));
459 return result;
460 }
461}
462
463template<typename SparseMdpModelType>
466 if constexpr (std::is_same_v<ValueType, storm::Interval>) {
467 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We have not yet implemented quantile formulas with intervals");
468 } else {
469 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException,
470 "Computing quantiles is only supported for the initial states of a model.");
471 STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException,
472 "Quantiles not supported on models with multiple initial states.");
473 uint64_t initialState = *this->getModel().getInitialStates().begin();
474
475 helper::rewardbounded::QuantileHelper<SparseMdpModelType> qHelper(this->getModel(), checkTask.getFormula());
476 auto res = qHelper.computeQuantile(env);
477
478 if (res.size() == 1 && res.front().size() == 1) {
479 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(initialState, std::move(res.front().front())));
480 } else {
481 return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<SolutionType>(initialState, std::move(res)));
482 }
483 }
484}
485
489} // namespace modelchecker
490} // 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
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:333
bool isInFragment(FragmentSpecification const &fragment) const
Definition Formula.cpp:196
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 & 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 & 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 > 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 > 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 > 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 > 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)
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.
Definition cli.cpp:18
boost::optional< Bound > bound