Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
AbstractAbstractionRefinementModelChecker.cpp
Go to the documentation of this file.
2
31#include "storm/utility/graph.h"
33
34namespace storm::gbar {
35namespace modelchecker {
36
37template<typename ModelType>
47
48template<typename ModelType>
52
53template<typename ModelType>
55 storm::logic::Formula const& formula = checkTask.getFormula();
56 bool enableRewards = this->supportsReachabilityRewards();
59 return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
60}
61
62template<typename ModelType>
66
67template<typename ModelType>
70 this->setCheckTask(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
71 return performAbstractionRefinement(env);
72}
73
74template<typename ModelType>
77 STORM_LOG_THROW(this->supportsReachabilityRewards(), storm::exceptions::NotSupportedException,
78 "Reachability rewards are not supported by this abstraction-refinement model checker.");
79 this->setCheckTask(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
80 return performAbstractionRefinement(env);
81}
82
83template<typename ModelType>
86 this->setCheckTask(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.getFormula()));
87 return performAbstractionRefinement(env);
88}
89
90template<typename ModelType>
92 this->checkTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>>(checkTask);
93}
94
95template<typename ModelType>
100
101template<typename ModelType>
103 return reuseQualitativeResults;
104}
105
106template<typename ModelType>
108 return reuseQuantitativeResults;
109}
110
111template<typename ModelType>
112std::unique_ptr<storm::modelchecker::CheckResult> AbstractAbstractionRefinementModelChecker<ModelType>::performAbstractionRefinement(Environment const& env) {
113 STORM_LOG_THROW(checkTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException,
114 "The abstraction-refinement model checkers can only compute the result for the initial states.");
115
116 // Notify the underlying implementation that the abstraction-refinement process is being started.
117 this->initializeAbstractionRefinement();
118
119 uint64_t iterations = 0;
120 std::unique_ptr<storm::modelchecker::CheckResult> result;
121 auto start = std::chrono::high_resolution_clock::now();
122 while (!result) {
123 ++iterations;
124
125 // Obtain the abstract model.
126 auto abstractionStart = std::chrono::high_resolution_clock::now();
127 std::shared_ptr<storm::models::Model<ValueType>> abstractModel = this->getAbstractModel();
128 auto abstractionEnd = std::chrono::high_resolution_clock::now();
129 STORM_LOG_TRACE("Model in iteration " << iterations << " has " << abstractModel->getNumberOfStates() << " states and "
130 << abstractModel->getNumberOfTransitions() << " transitions (retrieved in "
131 << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
132
133 // Obtain lower and upper bounds from the abstract model.
134 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> bounds =
135 computeBounds(env, *abstractModel);
136
137 // Try to derive the final result from the obtained bounds.
138 if (bounds.first || bounds.second) {
139 result = tryToObtainResultFromBounds(*abstractModel, bounds);
140 }
141 if (!result) {
142 if (bounds.first && bounds.second) {
143 printBoundsInformation(bounds);
144 }
145
146 auto refinementStart = std::chrono::high_resolution_clock::now();
147 this->refineAbstractModel();
148 auto refinementEnd = std::chrono::high_resolution_clock::now();
149 STORM_LOG_TRACE("Refinement in iteration " << iterations << " completed in "
150 << std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count()
151 << "ms.");
152 }
153 }
154 auto end = std::chrono::high_resolution_clock::now();
155 STORM_LOG_TRACE("Completed abstraction-refinement (" << this->getName() << ") in "
156 << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
157
158 return result;
159}
160
161template<typename ModelType>
162std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
164 // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part.
165
166 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
167
168 // Preparation: determine the constraint states and the target states of the reachability objective.
169 std::pair<std::unique_ptr<storm::gbar::abstraction::StateSet>, std::unique_ptr<storm::gbar::abstraction::StateSet>> constraintAndTargetStates =
170 getConstraintAndTargetStates(abstractModel);
171
172 // Phase (1): solve qualitatively.
173 lastQualitativeResults = computeQualitativeResult(env, abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second);
174
175 // Check whether the answer can be given after the qualitative solution.
176 result.first = checkForResultAfterQualitativeCheck(abstractModel);
177 if (result.first) {
178 return result;
179 }
180
181 // Check whether we should skip the quantitative solution (for example if there are initial states for which
182 // the value is already known to be different at this point.
183 bool doSkipQuantitativeSolution = skipQuantitativeSolution(abstractModel, *lastQualitativeResults);
184 STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution.");
185
186 // Phase (2): solve quantitatively.
187 if (!doSkipQuantitativeSolution) {
188 lastBounds =
189 computeQuantitativeResult(env, abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second, *lastQualitativeResults);
190 STORM_LOG_ASSERT(lastBounds.first && lastBounds.second, "Expected both bounds.");
191
192 result = std::make_pair(lastBounds.first->clone(), lastBounds.second->clone());
193 filterInitialStates(abstractModel, result);
194
195 // Check whether the answer can be given after the quantitative solution.
196 if (checkForResultAfterQuantitativeCheck(abstractModel, true, result.first->asQuantitativeCheckResult<ValueType>())) {
197 result.second = nullptr;
198 } else if (checkForResultAfterQuantitativeCheck(abstractModel, false, result.second->asQuantitativeCheckResult<ValueType>())) {
199 result.first = nullptr;
200 }
201 }
202
203 return result;
204}
205
206template<typename ModelType>
208 storm::models::Model<ValueType> const& abstractModel, bool lowerBounds, storm::modelchecker::QuantitativeCheckResult<ValueType> const& quantitativeResult) {
209 bool result = false;
210 if (checkTask->isBoundSet()) {
211 storm::logic::ComparisonType comparisonType = checkTask->getBoundComparisonType();
212 ValueType threshold = checkTask->getBoundThreshold();
213
214 if (lowerBounds) {
215 if (storm::logic::isLowerBound(comparisonType)) {
216 ValueType minimalLowerBound = quantitativeResult.getMin();
217 result = (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) ||
218 (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold);
219 } else {
220 ValueType maximalLowerBound = quantitativeResult.getMax();
221 result = (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) ||
222 (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold);
223 }
224 } else {
225 if (storm::logic::isLowerBound(comparisonType)) {
226 ValueType minimalUpperBound = quantitativeResult.getMin();
227 result = (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) ||
228 (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold);
229 } else {
230 ValueType maximalUpperBound = quantitativeResult.getMax();
231 result = (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) ||
232 (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold);
233 }
234 }
235
236 if (result) {
237 STORM_LOG_TRACE("Found result after quantiative check.");
238 } else {
239 STORM_LOG_TRACE("Did not find result after quantiative check.");
240 }
241 }
242
243 return result;
244}
245
246template<typename ModelType>
248 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds) {
249 STORM_LOG_THROW(bounds.first->isSymbolicQuantitativeCheckResult() && bounds.second->isSymbolicQuantitativeCheckResult(),
250 storm::exceptions::NotSupportedException, "Expected symbolic bounds.");
251
252 printBoundsInformation(bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>(),
253 bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>());
254}
255
256template<typename ModelType>
260 // If there is exactly one value that we stored, we print the current bounds as an interval.
261 if (lowerBounds.getStates().getNonZeroCount() == 1 && upperBounds.getStates().getNonZeroCount() == 1) {
262 STORM_LOG_TRACE("Obtained bounds [" << lowerBounds.getValueVector().getMax() << ", " << upperBounds.getValueVector().getMax() << "] on actual result.");
263 } else {
264 storm::dd::Add<DdType, ValueType> diffs = upperBounds.getValueVector() - lowerBounds.getValueVector();
266
267 std::pair<ValueType, ValueType> bounds;
268 bounds.first = (lowerBounds.getValueVector() * maxDiffRepresentative.template toAdd<ValueType>()).getMax();
269 bounds.second = (upperBounds.getValueVector() * maxDiffRepresentative.template toAdd<ValueType>()).getMax();
270
271 STORM_LOG_TRACE("Largest interval over initial is [" << bounds.first << ", " << bounds.second << "], difference " << (bounds.second - bounds.first)
272 << ".");
273 }
274}
275
276template<typename ModelType>
278 storm::models::Model<ValueType> const& abstractModel,
279 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds) {
280 STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model.");
281
282 filterInitialStates(*abstractModel.template as<storm::models::symbolic::Model<DdType, ValueType>>(), bounds);
283}
284
285template<typename ModelType>
288 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds) {
290 bounds.first->filter(initialStateFilter);
291 bounds.second->filter(initialStateFilter);
292}
293
294template<typename ModelType>
296 storm::models::Model<ValueType> const& abstractModel, storm::gbar::abstraction::QualitativeResultMinMax const& qualitativeResults) {
297 STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model.");
298
299 return skipQuantitativeSolution(*abstractModel.template as<storm::models::symbolic::Model<DdType, ValueType>>(),
300 qualitativeResults.asSymbolicQualitativeResultMinMax<DdType>());
301}
302
303template<typename ModelType>
307 bool isRewardFormula =
308 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
309 if (isRewardFormula) {
310 if ((abstractModel.getInitialStates() && qualitativeResults.getProb1Min().getStates()) !=
311 (abstractModel.getInitialStates() && qualitativeResults.getProb1Max().getStates())) {
312 return true;
313 }
314 } else {
315 if ((abstractModel.getInitialStates() && qualitativeResults.getProb0Min().getStates()) !=
316 (abstractModel.getInitialStates() && qualitativeResults.getProb0Max().getStates())) {
317 return true;
318 } else if ((abstractModel.getInitialStates() && qualitativeResults.getProb1Min().getStates()) !=
319 (abstractModel.getInitialStates() && qualitativeResults.getProb1Max().getStates())) {
320 return true;
321 }
322 }
323 return false;
324}
325
326template<typename ModelType>
327std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
329 storm::gbar::abstraction::StateSet const& constraintStates,
330 storm::gbar::abstraction::StateSet const& targetStates,
331 storm::gbar::abstraction::QualitativeResultMinMax const& qualitativeResults) {
332 STORM_LOG_ASSERT(abstractModel.isSymbolicModel(), "Expected symbolic abstract model.");
333
335 constraintStates.asSymbolicStateSet<DdType>(), targetStates.asSymbolicStateSet<DdType>(),
336 qualitativeResults.asSymbolicQualitativeResultMinMax<DdType>());
337}
338
339template<typename ModelType>
340std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
342 Environment const& env, storm::models::symbolic::Model<DdType, ValueType> const& abstractModel,
347 storm::exceptions::NotSupportedException, "Abstract model type is not supported.");
348
349 if (abstractModel.isOfType(storm::models::ModelType::Dtmc)) {
350 return computeQuantitativeResult(env, *abstractModel.template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), constraintStates, targetStates,
351 qualitativeResults);
352 } else if (abstractModel.isOfType(storm::models::ModelType::Mdp)) {
353 return computeQuantitativeResult(env, *abstractModel.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), constraintStates, targetStates,
354 qualitativeResults);
355 } else {
357 constraintStates, targetStates, qualitativeResults);
358 }
359}
360
361template<typename ModelType>
362std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
364 Environment const& env, storm::models::symbolic::Dtmc<DdType, ValueType> const& abstractModel,
367 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
369
370 bool isRewardFormula =
371 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
372 if (isRewardFormula) {
373 maybe = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates();
374 } else {
375 maybe = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates();
376 }
377
379 if (this->getReuseQuantitativeResults() && lastBounds.first) {
380 startValues = maybe.ite(lastBounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(),
381 abstractModel.getManager().template getAddZero<ValueType>());
382 } else {
383 startValues = abstractModel.getManager().template getAddZero<ValueType>();
384 }
385
386 if (isRewardFormula) {
388 env, abstractModel, abstractModel.getTransitionMatrix(),
389 checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybe,
390 targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), startValues);
391
392 result.first = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(abstractModel.getReachableStates(), values);
393 result.second = result.first->clone();
394 } else {
396 env, abstractModel, abstractModel.getTransitionMatrix(), maybe, qualitativeResults.getProb1Min().getStates(), startValues);
397
398 result.first = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(abstractModel.getReachableStates(), values);
399 result.second = result.first->clone();
400 }
401
402 return result;
403}
404
405template<typename ModelType>
406std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
408 Environment const& env, storm::models::symbolic::Mdp<DdType, ValueType> const& abstractModel,
411 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
412 storm::dd::Bdd<DdType> maybeMin;
413 storm::dd::Bdd<DdType> maybeMax;
414
415 bool isRewardFormula =
416 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
417 if (isRewardFormula) {
418 maybeMin = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates();
419 maybeMax = qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates();
420 } else {
421 maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates();
422 maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates();
423 }
424
426 if (this->getReuseQuantitativeResults() && lastBounds.first) {
427 minStartValues = maybeMin.ite(lastBounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(),
428 abstractModel.getManager().template getAddZero<ValueType>());
429 } else {
430 minStartValues = abstractModel.getManager().template getAddZero<ValueType>();
431 }
432
433 uint64_t abstractionPlayer = this->getAbstractionPlayer();
434 if (isRewardFormula) {
436 env, abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), abstractModel,
437 abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(),
438 checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin,
439 targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), minStartValues);
440
441 if (abstractionPlayer == 0) {
442 result.second = result.first->clone();
443 } else {
445 env, storm::OptimizationDirection::Maximize, abstractModel, abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(),
446 checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin,
447 targetStates.getStates(), !qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates(),
448 maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(),
449 abstractModel.getManager().template getAddZero<ValueType>()));
450 }
451 } else {
453 env, abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), abstractModel,
454 abstractModel.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), minStartValues);
455
456 if (abstractionPlayer == 0) {
457 result.second = result.first->clone();
458 } else {
460 env, storm::OptimizationDirection::Maximize, abstractModel, abstractModel.getTransitionMatrix(), maybeMax,
461 qualitativeResults.getProb1Max().getStates(),
462 maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(),
463 abstractModel.getManager().template getAddZero<ValueType>()));
464 }
465 }
466
467 return result;
468}
469
470template<typename ModelType>
471std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
476 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
477 storm::dd::Bdd<DdType> maybeMin;
478 storm::dd::Bdd<DdType> maybeMax;
479
480 bool isRewardFormula =
481 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
482 if (!isRewardFormula) {
483 maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates();
484 maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates();
485 }
486
488 if (this->getReuseQuantitativeResults() && lastBounds.first) {
489 minStartValues = maybeMin.ite(lastBounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(),
490 abstractModel.getManager().template getAddZero<ValueType>());
491 } else {
492 minStartValues = abstractModel.getManager().template getAddZero<ValueType>();
493 }
494
495 if (isRewardFormula) {
496 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward properties are not supported for abstract stochastic games.");
497 } else {
498 result.first = computeReachabilityProbabilitiesHelper(
499 env, abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(),
500 this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), maybeMin,
501 qualitativeResults.getProb1Min().getStates(), minStartValues);
502 result.second = computeReachabilityProbabilitiesHelper(
503 env, abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Maximize : checkTask->getOptimizationDirection(),
504 this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Maximize : checkTask->getOptimizationDirection(), maybeMin,
505 qualitativeResults.getProb1Max().getStates(),
506 maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(),
507 abstractModel.getManager().template getAddZero<ValueType>()));
508 }
509
510 return result;
511}
512
513template<typename ModelType>
516 storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd<DdType> const& maybeStates,
517 storm::dd::Bdd<DdType> const& prob1States, storm::dd::Add<DdType, ValueType> const& startValues) {
518 STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << ".");
519
520 // Compute the ingredients of the equation system.
521 storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
522 storm::dd::Add<DdType, ValueType> submatrix = maybeStatesAdd * abstractModel.getTransitionMatrix();
523 storm::dd::Add<DdType, ValueType> prob1StatesAsColumn =
524 prob1States.template toAdd<ValueType>().swapVariables(abstractModel.getRowColumnMetaVariablePairs());
525 storm::dd::Add<DdType, ValueType> subvector = submatrix * prob1StatesAsColumn;
526 subvector = subvector.sumAbstract(abstractModel.getColumnVariables());
527
528 // Cut away all columns targeting non-maybe states.
529 submatrix *= maybeStatesAdd.swapVariables(abstractModel.getRowColumnMetaVariablePairs());
530
531 // Cut the starting vector to the maybe states of this query.
532 storm::dd::Add<DdType, ValueType> startVector = maybeStates.ite(startValues, abstractModel.getManager().template getAddZero<ValueType>());
533
534 // Create the solver and solve the equation system.
536 std::unique_ptr<storm::solver::SymbolicGameSolver<DdType, ValueType>> solver =
537 solverFactory.create(submatrix, maybeStates, abstractModel.getIllegalPlayer1Mask(), abstractModel.getIllegalPlayer2Mask(),
538 abstractModel.getRowVariables(), abstractModel.getColumnVariables(), abstractModel.getRowColumnMetaVariablePairs(),
539 abstractModel.getPlayer1Variables(), abstractModel.getPlayer2Variables());
540 auto values = solver->solveGame(env, player1Direction, player2Direction, startVector, subvector);
541
542 return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(abstractModel.getReachableStates(),
543 prob1States.template toAdd<ValueType>() + values);
544}
545
546template<typename ModelType>
547std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> AbstractAbstractionRefinementModelChecker<ModelType>::computeQualitativeResult(
548 Environment const& env, storm::models::Model<ValueType> const& abstractModel, storm::gbar::abstraction::StateSet const& constraintStates,
549 storm::gbar::abstraction::StateSet const& targetStates) {
550 STORM_LOG_ASSERT(abstractModel.isSymbolicModel(), "Expected symbolic abstract model.");
551
552 return computeQualitativeResult(env, *abstractModel.template as<storm::models::symbolic::Model<DdType, ValueType>>(),
553 constraintStates.asSymbolicStateSet<DdType>(), targetStates.asSymbolicStateSet<DdType>());
554}
555
556template<typename ModelType>
557std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> AbstractAbstractionRefinementModelChecker<ModelType>::computeQualitativeResult(
558 Environment const& env, storm::models::symbolic::Model<DdType, ValueType> const& abstractModel,
562 storm::exceptions::NotSupportedException, "Expected discrete-time abstract model.");
563
564 if (abstractModel.isOfType(storm::models::ModelType::Dtmc)) {
565 return computeQualitativeResult(env, *abstractModel.template as<storm::models::symbolic::Dtmc<DdType, ValueType>>(), constraintStates, targetStates);
566 } else if (abstractModel.isOfType(storm::models::ModelType::Mdp)) {
567 return computeQualitativeResult(env, *abstractModel.template as<storm::models::symbolic::Mdp<DdType, ValueType>>(), constraintStates, targetStates);
568 } else {
569 return computeQualitativeResult(env, *abstractModel.template as<storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType>>(),
570 constraintStates, targetStates);
571 }
572}
573
574template<typename ModelType>
575std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> AbstractAbstractionRefinementModelChecker<ModelType>::computeQualitativeResult(
576 Environment const& env, storm::models::symbolic::Dtmc<DdType, ValueType> const& abstractModel,
578 STORM_LOG_DEBUG("Computing qualitative solution for DTMC.");
579 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>> result =
580 std::make_unique<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>>();
581
582 auto start = std::chrono::high_resolution_clock::now();
583 bool isRewardFormula =
584 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
585 storm::dd::Bdd<DdType> transitionMatrixBdd = abstractModel.getTransitionMatrix().notZero();
586 if (isRewardFormula) {
587 auto prob1 = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
588 result->prob1Min = result->prob1Max = storm::gbar::abstraction::SymbolicQualitativeMdpResult<DdType>(prob1);
589 } else {
590 auto prob01 = storm::utility::graph::performProb01(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
591 result->prob0Min = result->prob0Max = storm::gbar::abstraction::SymbolicQualitativeMdpResult<DdType>(prob01.first);
592 result->prob1Min = result->prob1Max = storm::gbar::abstraction::SymbolicQualitativeMdpResult<DdType>(prob01.second);
593 }
594 auto end = std::chrono::high_resolution_clock::now();
595
596 auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
597 STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms.");
598
599 return std::move(result); // move() required by, e.g., clang 3.8
600}
601
602template<typename ModelType>
603std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> AbstractAbstractionRefinementModelChecker<ModelType>::computeQualitativeResult(
604 Environment const& env, storm::models::symbolic::Mdp<DdType, ValueType> const& abstractModel,
606 STORM_LOG_DEBUG("Computing qualitative solution for MDP.");
607 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>> result =
608 std::make_unique<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>>();
609
610 auto start = std::chrono::high_resolution_clock::now();
611 bool isRewardFormula =
612 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
613 storm::dd::Bdd<DdType> transitionMatrixBdd = abstractModel.getTransitionMatrix().notZero();
614 uint64_t abstractionPlayer = this->getAbstractionPlayer();
615 if (this->getReuseQualitativeResults()) {
616 if (isRewardFormula) {
617 bool computedMin = false;
618 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
620 abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
621 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates()
622 : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(),
623 targetStates.getStates()));
625 computedMin = true;
626 }
627
628 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
630 abstractModel, transitionMatrixBdd, targetStates.getStates(),
631 storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()));
633 if (!computedMin) {
634 result->prob1Min = result->prob1Max;
635 }
636 } else {
637 result->prob1Max = result->prob1Min;
638 }
639
640 } else {
641 bool computedMax = false;
642 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
643 auto states = storm::utility::graph::performProb0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
646 abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
647 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates()
648 : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(),
649 targetStates.getStates()));
651 computedMax = true;
652 }
653
654 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
656 abstractModel, transitionMatrixBdd,
657 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates()
658 : targetStates.getStates(),
659 storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()));
661
662 states = storm::utility::graph::performProb0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
664
665 if (!computedMax) {
666 result->prob0Max = result->prob0Min;
667 result->prob1Max = result->prob1Min;
668 }
669 } else {
670 result->prob0Min = result->prob0Max;
671 result->prob1Min = result->prob1Max;
672 }
673 }
674 } else {
675 if (isRewardFormula) {
676 bool computedMin = false;
677 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
679 abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
680 storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()));
682 computedMin = true;
683 }
684
685 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
687 abstractModel, transitionMatrixBdd, targetStates.getStates(),
688 storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()));
690 if (!computedMin) {
691 result->prob1Min = result->prob1Max;
692 }
693 } else {
694 result->prob1Max = result->prob1Min;
695 }
696 } else {
697 bool computedMin = false;
698 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
699 auto prob01 =
700 storm::utility::graph::performProb01Min(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
703 computedMin = true;
704 }
705
706 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
707 auto prob01 =
708 storm::utility::graph::performProb01Max(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates());
711 if (!computedMin) {
712 result->prob0Min = result->prob0Max;
713 result->prob1Min = result->prob1Max;
714 }
715 } else {
716 result->prob0Max = result->prob0Min;
717 result->prob1Max = result->prob1Min;
718 }
719 }
720 }
721 auto end = std::chrono::high_resolution_clock::now();
722
723 auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
724 if (isRewardFormula) {
725 STORM_LOG_TRACE("Min: " << result->getProb1Min().getStates().getNonZeroCount() << " states with probability 1.");
726 STORM_LOG_TRACE("Max: " << result->getProb1Max().getStates().getNonZeroCount() << " states with probability 1.");
727 } else {
728 STORM_LOG_TRACE("Min: " << result->getProb0Min().getStates().getNonZeroCount() << " states with probability 0, "
729 << result->getProb1Min().getStates().getNonZeroCount() << " states with probability 1.");
730 STORM_LOG_TRACE("Max: " << result->getProb0Max().getStates().getNonZeroCount() << " states with probability 0, "
731 << result->getProb1Max().getStates().getNonZeroCount() << " states with probability 1.");
732 }
733 STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms.");
734
735 return std::move(result); // move() required by, e.g., clang 3.8
736}
737
738template<typename ModelType>
739std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> AbstractAbstractionRefinementModelChecker<ModelType>::computeQualitativeResult(
742 STORM_LOG_DEBUG("Computing qualitative solution for S2PG.");
743 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>> result;
744
745 // Obtain the player optimization directions.
746 uint64_t abstractionPlayer = this->getAbstractionPlayer();
747
748 // Obtain direction for player 1 (model nondeterminism).
749 storm::OptimizationDirection modelNondeterminismDirection = this->getCheckTask().getOptimizationDirection();
750
751 // Convert the transition matrix to a BDD to use it in the qualitative algorithms.
752 storm::dd::Bdd<DdType> transitionMatrixBdd = abstractModel.getTransitionMatrix().toBdd();
753
754 // Remembers whether we need to synthesize schedulers.
755 bool requiresSchedulers = this->requiresSchedulerSynthesis();
756
757 auto start = std::chrono::high_resolution_clock::now();
758 if (this->getReuseQualitativeResults()) {
759 result = computeQualitativeResultReuse(abstractModel, transitionMatrixBdd, constraintStates, targetStates, abstractionPlayer,
760 modelNondeterminismDirection, requiresSchedulers);
761 } else {
762 result = std::make_unique<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>>();
763
764 result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
765 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
766 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
767 requiresSchedulers, requiresSchedulers);
768 result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
769 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
770 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
771 requiresSchedulers, requiresSchedulers);
772 result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
773 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
774 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
775 requiresSchedulers, requiresSchedulers);
776 result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
777 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
778 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
779 requiresSchedulers, requiresSchedulers);
780 }
781
782 STORM_LOG_TRACE("Qualitative precomputation completed.");
783 if (abstractionPlayer == 1) {
784 STORM_LOG_TRACE("[" << storm::OptimizationDirection::Minimize << ", " << modelNondeterminismDirection << "]: "
785 << result->prob0Min.player1States.getNonZeroCount() << " 'no', " << result->prob1Min.player1States.getNonZeroCount() << " 'yes'.");
786 STORM_LOG_TRACE("[" << storm::OptimizationDirection::Maximize << ", " << modelNondeterminismDirection << "]: "
787 << result->prob0Max.player1States.getNonZeroCount() << " 'no', " << result->prob1Max.player1States.getNonZeroCount() << " 'yes'.");
788 } else {
789 STORM_LOG_TRACE("[" << modelNondeterminismDirection << ", " << storm::OptimizationDirection::Minimize << "]: "
790 << result->prob0Min.player1States.getNonZeroCount() << " 'no', " << result->prob1Min.player1States.getNonZeroCount() << " 'yes'.");
791 STORM_LOG_TRACE("[" << modelNondeterminismDirection << ", " << storm::OptimizationDirection::Maximize << "]: "
792 << result->prob0Max.player1States.getNonZeroCount() << " 'no', " << result->prob1Max.player1States.getNonZeroCount() << " 'yes'.");
793 }
794
795 auto end = std::chrono::high_resolution_clock::now();
796
797 auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
798 STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms.");
799
800 return std::move(result); // move() required by, e.g., clang 3.8
801}
802
803template<typename ModelType>
804std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<AbstractAbstractionRefinementModelChecker<ModelType>::DdType>>
808 uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers) {
809 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>> result =
810 std::make_unique<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>>();
811
812 // Depending on the model nondeterminism direction, we choose a different order of operations.
813 if (modelNondeterminismDirection == storm::OptimizationDirection::Minimize) {
814 // (1) min/min: compute prob0 using the game functions
815 result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
816 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize,
817 requiresSchedulers, requiresSchedulers);
818
819 // (2) min/min: compute prob1 using the MDP functions
820 storm::dd::Bdd<DdType> candidates = abstractModel.getReachableStates() && !result->getProb0Min().getStates();
822 abstractModel, transitionMatrixBdd,
823 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates() : targetStates.getStates(),
824 candidates);
825
826 // (3) min/min: compute prob1 using the game functions
827 result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
828 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize,
829 requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MinMinMdp));
830
831 // (4) min/max, max/min: compute prob 0 using the game functions
832 result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
833 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
834 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
835 requiresSchedulers, requiresSchedulers);
836
837 // (5) min/max, max/min: compute prob 1 using the game functions
838 // We know that only previous prob1 states can now be prob 1 states again, because the upper bound
839 // values can only decrease over iterations.
840 result->prob1Max = storm::utility::graph::performProb1(
841 abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
842 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
843 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers,
844 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Max().getStates()
845 : boost::optional<storm::dd::Bdd<DdType>>());
846 } else {
847 // (1) max/max: compute prob0 using the game functions
848 result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
849 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize,
850 requiresSchedulers, requiresSchedulers);
851
852 // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states.
853 storm::dd::Bdd<DdType> candidates = abstractModel.getReachableStates() && !result->getProb0Max().getStates();
854 if (this->getReuseQualitativeResults() && lastQualitativeResults) {
855 candidates &= lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Max().getStates();
856 }
857 storm::dd::Bdd<DdType> prob1MaxMaxMdp =
858 storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), candidates);
859
860 // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation
861 result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
862 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize,
863 requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MaxMaxMdp));
864
865 // (4) max/min, min/max: compute prob0 using the game functions
866 result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
867 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
868 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
869 requiresSchedulers, requiresSchedulers);
870
871 // (5) max/min:, max/min compute prob1 using the game functions, use prob1 from max/max as the candidate set
872 result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(),
873 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
874 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
875 requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MaxMaxMdp));
876 }
877
878 return result;
879}
880
881template<typename ModelType>
883 storm::models::Model<ValueType> const& abstractModel) {
884 STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model.");
885
887}
888
889template<typename ModelType>
892 std::unique_ptr<storm::modelchecker::CheckResult> result;
893
894 auto const& symbolicQualitativeResultMinMax = lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>();
895
896 bool isRewardFormula =
897 checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
898 if (isRewardFormula) {
899 // In the reachability reward case, we can give an answer if all initial states of the system are infinity
900 // states in the min result.
901 if ((abstractModel.getInitialStates() && !symbolicQualitativeResultMinMax.getProb1Min().getStates()) == abstractModel.getInitialStates()) {
902 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
903 abstractModel.getReachableStates(), abstractModel.getInitialStates(),
904 abstractModel.getInitialStates().ite(abstractModel.getManager().getConstant(storm::utility::infinity<ValueType>()),
905 abstractModel.getManager().template getAddZero<ValueType>()));
906 }
907 } else {
908 // In the reachability probability case, we can give the answer if all initial states are prob1 states
909 // in the min result or if all initial states are prob0 in the max case.
910 // Furthermore, we can give the answer if there are initial states with probability > 0 in the min case
911 // and the probability bound was 0 or if there are initial states with probability < 1 in the max case
912 // and the probability bound was 1.
913 if ((abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb1Min().getStates()) == abstractModel.getInitialStates()) {
914 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
915 abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getManager().template getAddOne<ValueType>());
916 } else if ((abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb0Max().getStates()) == abstractModel.getInitialStates()) {
917 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
918 abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getManager().template getAddZero<ValueType>());
919 } else if (checkTask->isBoundSet() && checkTask->getBoundThreshold() == storm::utility::zero<ValueType>() &&
920 (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb0Min().getStates()) != abstractModel.getInitialStates()) {
921 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
922 abstractModel.getReachableStates(), abstractModel.getInitialStates(),
923 (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb0Min().getStates())
924 .ite(abstractModel.getManager().template getConstant<ValueType>(0.5), abstractModel.getManager().template getAddZero<ValueType>()));
925 } else if (checkTask->isBoundSet() && checkTask->getBoundThreshold() == storm::utility::one<ValueType>() &&
926 (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb1Max().getStates()) != abstractModel.getInitialStates()) {
927 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
928 abstractModel.getReachableStates(), abstractModel.getInitialStates(),
929 (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb1Max().getStates())
930 .ite(abstractModel.getManager().template getConstant<ValueType>(0.5), abstractModel.getManager().template getAddZero<ValueType>()) +
931 symbolicQualitativeResultMinMax.getProb1Max().getStates().template toAdd<ValueType>());
932 }
933 }
934
935 if (result) {
936 STORM_LOG_TRACE("Found result after qualitative check.");
937 } else {
938 STORM_LOG_TRACE("Did not find result after qualitative check.");
939 }
940
941 return result;
942}
943
944template<typename ModelType>
946 storm::models::Model<ValueType> const& abstractModel,
947 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds) {
948 std::unique_ptr<storm::modelchecker::CheckResult> result;
949
950 if (bounds.first == nullptr || bounds.second == nullptr) {
951 STORM_LOG_ASSERT(bounds.first || bounds.second, "Expected at least one bound.");
952
953 if (bounds.first) {
954 return std::move(bounds.first);
955 } else {
956 return std::move(bounds.second);
957 }
958 } else {
959 if (boundsAreSufficientlyClose(bounds)) {
960 STORM_LOG_TRACE("Obtained bounds are sufficiently close.");
961 result = getAverageOfBounds(bounds);
962 }
963 }
964
965 if (result) {
966 abstractModel.printModelInformationToStream(std::cout);
967 }
968
969 return result;
970}
971
972template<typename ModelType>
974 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> const& bounds) {
975 STORM_LOG_ASSERT(bounds.first->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result.");
977 bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
978 STORM_LOG_ASSERT(bounds.second->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result.");
980 bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
981
982 return lowerBounds.getValueVector().equalModuloPrecision(upperBounds.getValueVector(),
984}
985
986template<typename ModelType>
987std::unique_ptr<storm::modelchecker::CheckResult> AbstractAbstractionRefinementModelChecker<ModelType>::getAverageOfBounds(
988 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> const& bounds) {
989 STORM_LOG_ASSERT(bounds.first->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result.");
991 bounds.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
992 STORM_LOG_ASSERT(bounds.second->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result.");
994 bounds.second->asSymbolicQuantitativeCheckResult<DdType, ValueType>();
995
996 return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
997 lowerBounds.getReachableStates(), lowerBounds.getStates(),
998 (lowerBounds.getValueVector() + upperBounds.getValueVector()) /
999 lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber<ValueType>(std::string("2.0"))));
1000}
1001
1006
1007} // namespace modelchecker
1008} // namespace storm::gbar
Add< LibraryType, ValueType > swapVariables(std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
Swaps the given pairs of meta variables in the ADD.
Definition Add.cpp:292
ValueType getMax() const
Retrieves the highest function value of any encoding.
Definition Add.cpp:475
Add< LibraryType, ValueType > sumAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Sum-abstracts from the given meta variables.
Definition Add.cpp:178
Bdd< LibraryType > toBdd() const
Converts the ADD to a BDD by mapping all values unequal to zero to 1.
Definition Add.cpp:1187
bool equalModuloPrecision(Add< LibraryType, ValueType > const &other, ValueType const &precision, bool relative=true) const
Checks whether the current and the given ADD represent the same function modulo some given precision.
Definition Add.cpp:211
Bdd< LibraryType > notZero() const
Computes a BDD that represents the function in which all assignments with a function value unequal to...
Definition Add.cpp:431
Bdd< LibraryType > maxAbstractRepresentative(std::set< storm::expressions::Variable > const &metaVariables) const
Similar to maxAbstract, but does not abstract from the variables but rather picks a valuation of each...
Definition Add.cpp:205
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
Definition Bdd.cpp:513
Bdd< LibraryType > swapVariables(std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
Swaps the given pairs of meta variables in the BDD.
Definition Bdd.cpp:302
Bdd< LibraryType > ite(Bdd< LibraryType > const &thenBdd, Bdd< LibraryType > const &elseBdd) const
Performs an if-then-else with the given operands, i.e.
Definition Bdd.cpp:113
std::set< storm::expressions::Variable > const & getContainedMetaVariables() const
Retrieves the set of all meta variables contained in the DD.
Definition Dd.cpp:29
DdManager< LibraryType > & getDdManager() const
Retrieves the manager that is responsible for this DD.
Definition Dd.cpp:39
SymbolicQualitativeResultMinMax< Type > const & asSymbolicQualitativeResultMinMax() const
SymbolicStateSet< Type > const & asSymbolicStateSet() const
SymbolicQualitativeResult< Type > const & getProb0Min() const
SymbolicQualitativeResult< Type > const & getProb0Max() const
SymbolicQualitativeResult< Type > const & getProb1Max() const
SymbolicQualitativeResult< Type > const & getProb1Min() const
storm::dd::Bdd< Type > const & getStates() const
std::unique_ptr< storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax< DdType > > computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame< DdType, ValueType > const &abstractModel, storm::dd::Bdd< DdType > const &transitionMatrixBdd, storm::gbar::abstraction::SymbolicStateSet< DdType > const &constraintStates, storm::gbar::abstraction::SymbolicStateSet< DdType > const &targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const &modelNondeterminismDirection, bool requiresSchedulers)
std::unique_ptr< storm::modelchecker::CheckResult > getAverageOfBounds(std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > const &bounds)
Retrieves the average of the two bounds.
bool checkForResultAfterQuantitativeCheck(storm::models::Model< ValueType > const &abstractModel, bool lowerBounds, storm::modelchecker::QuantitativeCheckResult< ValueType > const &result)
std::unique_ptr< storm::modelchecker::CheckResult > performAbstractionRefinement(Environment const &env)
-----— Methods used to implement the abstraction refinement procedure.
std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > computeQuantitativeResult(Environment const &env, storm::models::Model< ValueType > const &abstractModel, storm::gbar::abstraction::StateSet const &constraintStates, storm::gbar::abstraction::StateSet const &targetStates, storm::gbar::abstraction::QualitativeResultMinMax const &qualitativeResults)
storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const & getCheckTask() const
std::unique_ptr< storm::gbar::abstraction::QualitativeResultMinMax > computeQualitativeResult(Environment const &env, storm::models::Model< ValueType > const &abstractModel, storm::gbar::abstraction::StateSet const &constraintStates, storm::gbar::abstraction::StateSet const &targetStates)
Solves the current check task qualitatively, i.e. computes all states with probability 0/1.
void setCheckTask(storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask)
Methods to set/get the check task that is currently handled.
void printBoundsInformation(std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > &bounds)
virtual bool supportsReachabilityRewards() const
-----— Methods that need to be overwritten/defined by implementations in subclasses.
std::unique_ptr< storm::modelchecker::CheckResult > checkForResultAfterQualitativeCheck(storm::models::Model< ValueType > const &abstractModel)
virtual std::unique_ptr< storm::modelchecker::CheckResult > computeReachabilityProbabilities(Environment const &env, storm::modelchecker::CheckTask< storm::logic::EventuallyFormula, ValueType > const &checkTask) override
virtual std::unique_ptr< storm::modelchecker::CheckResult > computeUntilProbabilities(Environment const &env, storm::modelchecker::CheckTask< storm::logic::UntilFormula, ValueType > const &checkTask) override
virtual std::unique_ptr< storm::modelchecker::CheckResult > computeReachabilityRewards(Environment const &env, storm::modelchecker::CheckTask< storm::logic::EventuallyFormula, ValueType > const &checkTask) override
bool skipQuantitativeSolution(storm::models::Model< ValueType > const &abstractModel, storm::gbar::abstraction::QualitativeResultMinMax const &qualitativeResults)
std::unique_ptr< storm::modelchecker::CheckResult > computeReachabilityProbabilitiesHelper(Environment const &env, storm::models::symbolic::StochasticTwoPlayerGame< DdType, ValueType > const &abstractModel, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::dd::Bdd< DdType > const &maybeStates, storm::dd::Bdd< DdType > const &prob1States, storm::dd::Add< DdType, ValueType > const &startValues)
std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > computeBounds(Environment const &env, storm::models::Model< ValueType > const &abstractModel)
Computes lower and upper bounds on the abstract model and returns the bounds for the initial states.
void filterInitialStates(storm::models::Model< ValueType > const &abstractModel, std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > &bounds)
std::unique_ptr< storm::modelchecker::CheckResult > tryToObtainResultFromBounds(storm::models::Model< ValueType > const &model, std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > &bounds)
Tries to obtain the results from the bounds.
bool getReuseQualitativeResults() const
Methods that retrieve which results shall be reused.
bool boundsAreSufficientlyClose(std::pair< std::unique_ptr< storm::modelchecker::CheckResult >, std::unique_ptr< storm::modelchecker::CheckResult > > const &bounds)
Checks whether the provided bounds are sufficiently close to terminate.
virtual bool canHandle(storm::modelchecker::CheckTask< storm::logic::Formula > const &checkTask) const override
Overridden methods from super class.
bool isInFragment(FragmentSpecification const &fragment) const
Definition Formula.cpp:196
FragmentSpecification & setReachabilityRewardFormulasAllowed(bool newValue)
FragmentSpecification & setRewardOperatorsAllowed(bool newValue)
SymbolicQuantitativeCheckResult< Type, ValueType > & asSymbolicQuantitativeCheckResult()
FormulaType const & getFormula() const
Retrieves the formula from this task.
Definition CheckTask.h:140
bool isOnlyInitialStatesRelevantSet() const
Retrieves whether only the initial states are relevant in the computation.
Definition CheckTask.h:204
virtual ValueType getMax() const =0
virtual ValueType getMin() const =0
storm::dd::Add< Type, ValueType > const & getValueVector() const
static storm::dd::Add< DdType, ValueType > computeUntilProbabilities(Environment const &env, storm::models::symbolic::Model< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, storm::dd::Bdd< DdType > const &phiStates, storm::dd::Bdd< DdType > const &psiStates, bool qualitative, boost::optional< storm::dd::Add< DdType, ValueType > > const &startValues=boost::none)
static storm::dd::Add< DdType, ValueType > computeReachabilityRewards(Environment const &env, storm::models::symbolic::Model< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, RewardModelType const &rewardModel, storm::dd::Bdd< DdType > const &targetStates, bool qualitative, boost::optional< storm::dd::Add< DdType, ValueType > > const &startValues=boost::none)
static std::unique_ptr< CheckResult > computeUntilProbabilities(Environment const &env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, storm::dd::Bdd< DdType > const &phiStates, storm::dd::Bdd< DdType > const &psiStates, bool qualitative, boost::optional< storm::dd::Add< DdType, ValueType > > const &startValues=boost::none)
static std::unique_ptr< CheckResult > computeReachabilityRewards(Environment const &env, OptimizationDirection dir, storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &model, storm::dd::Add< DdType, ValueType > const &transitionMatrix, RewardModelType const &rewardModel, storm::dd::Bdd< DdType > const &targetStates, boost::optional< storm::dd::Add< DdType, ValueType > > const &startValues=boost::none)
virtual bool isSymbolicModel() const
Checks whether the model is a symbolic model.
Definition ModelBase.cpp:15
virtual void printModelInformationToStream(std::ostream &out) const =0
Prints information about the model to the specified stream.
bool isOfType(storm::models::ModelType const &modelType) const
Checks whether the model is of the given type.
Definition ModelBase.cpp:19
This class represents a discrete-time Markov chain.
Definition Dtmc.h:15
This class represents a discrete-time Markov decision process.
Definition Mdp.h:15
Base class for all symbolic models.
Definition Model.h:46
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
Definition Model.cpp:92
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
Definition Model.cpp:254
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
Definition Model.cpp:177
std::set< storm::expressions::Variable > const & getColumnVariables() const
Retrieves the meta variables used to encode the columns of the transition matrix and the vector indic...
Definition Model.cpp:197
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
Definition Model.cpp:107
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
Definition Model.cpp:223
std::set< storm::expressions::Variable > const & getRowVariables() const
Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices.
Definition Model.cpp:192
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
Definition Model.cpp:102
This class represents a discrete-time stochastic two-player game.
std::set< storm::expressions::Variable > const & getPlayer1Variables() const
Retrieeves the set of meta variables used to encode the nondeterministic choices of player 1.
std::set< storm::expressions::Variable > const & getPlayer2Variables() const
Retrieeves the set of meta variables used to encode the nondeterministic choices of player 2.
storm::dd::Bdd< Type > getIllegalPlayer1Mask() const
Retrieves a BDD characterizing all illegal player 1 choice encodings in the model.
storm::dd::Bdd< Type > getIllegalPlayer2Mask() const
Retrieves a BDD characterizing all illegal player 2 choice encodings in the model.
virtual std::unique_ptr< storm::solver::SymbolicGameSolver< Type, ValueType > > create(storm::dd::Add< Type, ValueType > const &A, storm::dd::Bdd< Type > const &allRows, storm::dd::Bdd< Type > const &illegalPlayer1Mask, storm::dd::Bdd< Type > const &illegalPlayer2Mask, std::set< storm::expressions::Variable > const &rowMetaVariables, std::set< storm::expressions::Variable > const &columnMetaVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables) const
#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_THROW(cond, exception, message)
Definition macros.h:30
std::unique_ptr< storm::modelchecker::CheckResult > checkForResultAfterQuantitativeCheck(storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::OptimizationDirection const &player2Direction, std::pair< ValueType, ValueType > const &initialValueRange)
std::unique_ptr< storm::modelchecker::CheckResult > checkForResultAfterQualitativeCheck(storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd< Type > const &initialStates, storm::dd::Bdd< Type > const &prob0, storm::dd::Bdd< Type > const &prob1)
SymbolicQuantitativeGameResult< Type, ValueType > computeQuantitativeResult(Environment const &env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, SymbolicQualitativeGameResultMinMax< Type > const &qualitativeResult, storm::dd::Add< Type, ValueType > const &initialStatesAdd, storm::dd::Bdd< Type > const &maybeStates, boost::optional< SymbolicQuantitativeGameResult< Type, ValueType > > const &startInfo=boost::none)
bool isLowerBound(ComparisonType t)
bool isStrict(ComparisonType t)
FragmentSpecification reachability()
SettingsType const & getModule()
Get module.
std::pair< storm::storage::BitVector, storm::storage::BitVector > performProb01(storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi i...
Definition graph.cpp:400
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:835
ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair)
Computes the set of states that have probability 0 given the strategies of the two players.
Definition graph.cpp:1308
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:857
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:997
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:689
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
Definition graph.cpp:749
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:976
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:1079
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:757
LabParser.cpp.
Definition cli.cpp:18