35namespace modelchecker {
37template<
typename ModelType>
39 :
storm::modelchecker::AbstractModelChecker<ModelType>(), checkTask(nullptr) {
48template<
typename ModelType>
53template<
typename ModelType>
56 bool enableRewards = this->supportsReachabilityRewards();
62template<
typename ModelType>
67template<
typename ModelType>
70 this->setCheckTask(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.
getFormula()));
71 return performAbstractionRefinement(env);
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);
83template<
typename ModelType>
86 this->setCheckTask(checkTask.template substituteFormula<storm::logic::Formula>(checkTask.
getFormula()));
87 return performAbstractionRefinement(env);
90template<
typename ModelType>
92 this->checkTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>>(checkTask);
95template<
typename ModelType>
101template<
typename ModelType>
103 return reuseQualitativeResults;
106template<
typename ModelType>
108 return reuseQuantitativeResults;
111template<
typename ModelType>
113 STORM_LOG_THROW(checkTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException,
114 "The abstraction-refinement model checkers can only compute the result for the initial states.");
117 this->initializeAbstractionRefinement();
119 uint64_t iterations = 0;
120 std::unique_ptr<storm::modelchecker::CheckResult> result;
121 auto start = std::chrono::high_resolution_clock::now();
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).");
134 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> bounds =
135 computeBounds(env, *abstractModel);
138 if (bounds.first || bounds.second) {
139 result = tryToObtainResultFromBounds(*abstractModel, bounds);
142 if (bounds.first && bounds.second) {
143 printBoundsInformation(bounds);
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()
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.");
161template<
typename ModelType>
162std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
166 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
169 std::pair<std::unique_ptr<storm::gbar::abstraction::StateSet>, std::unique_ptr<storm::gbar::abstraction::StateSet>> constraintAndTargetStates =
170 getConstraintAndTargetStates(abstractModel);
173 lastQualitativeResults = computeQualitativeResult(env, abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second);
183 bool doSkipQuantitativeSolution = skipQuantitativeSolution(abstractModel, *lastQualitativeResults);
184 STORM_LOG_TRACE(
"" << (doSkipQuantitativeSolution ?
"Skipping" :
"Not skipping") <<
" quantitative solution.");
187 if (!doSkipQuantitativeSolution) {
189 computeQuantitativeResult(env, abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second, *lastQualitativeResults);
190 STORM_LOG_ASSERT(lastBounds.first && lastBounds.second,
"Expected both bounds.");
192 result = std::make_pair(lastBounds.first->clone(), lastBounds.second->clone());
193 filterInitialStates(abstractModel, result);
197 result.second =
nullptr;
199 result.first =
nullptr;
206template<
typename ModelType>
210 if (checkTask->isBoundSet()) {
212 ValueType threshold = checkTask->getBoundThreshold();
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.");
252 printBoundsInformation(bounds.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>(),
253 bounds.second->asSymbolicQuantitativeCheckResult<DdType,
ValueType>());
256template<
typename ModelType>
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();
271 STORM_LOG_TRACE(
"Largest interval over initial is [" << bounds.first <<
", " << bounds.second <<
"], difference " << (bounds.second - bounds.first)
276template<
typename ModelType>
279 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds) {
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);
294template<
typename ModelType>
303template<
typename ModelType>
307 bool isRewardFormula =
309 if (isRewardFormula) {
326template<
typename ModelType>
327std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
339template<
typename ModelType>
340std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
347 storm::exceptions::NotSupportedException,
"Abstract model type is not supported.");
357 constraintStates, targetStates, qualitativeResults);
361template<
typename ModelType>
362std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
367 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
370 bool isRewardFormula =
372 if (isRewardFormula) {
379 if (this->getReuseQuantitativeResults() && lastBounds.first) {
380 startValues = maybe.
ite(lastBounds.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>().getValueVector(),
381 abstractModel.
getManager().template getAddZero<ValueType>());
383 startValues = abstractModel.
getManager().template getAddZero<ValueType>();
386 if (isRewardFormula) {
392 result.first = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(abstractModel.
getReachableStates(), values);
393 result.second = result.first->clone();
398 result.first = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(abstractModel.
getReachableStates(), values);
399 result.second = result.first->clone();
405template<
typename ModelType>
406std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>
411 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> result;
415 bool isRewardFormula =
417 if (isRewardFormula) {
426 if (this->getReuseQuantitativeResults() && lastBounds.first) {
427 minStartValues = maybeMin.
ite(lastBounds.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>().getValueVector(),
428 abstractModel.
getManager().template getAddZero<ValueType>());
430 minStartValues = abstractModel.
getManager().template getAddZero<ValueType>();
433 uint64_t abstractionPlayer = this->getAbstractionPlayer();
434 if (isRewardFormula) {
436 env, abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), abstractModel,
441 if (abstractionPlayer == 0) {
442 result.second = result.first->clone();
448 maybeMax.
ite(result.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>().getValueVector(),
449 abstractModel.
getManager().template getAddZero<ValueType>()));
453 env, abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), abstractModel,
456 if (abstractionPlayer == 0) {
457 result.second = result.first->clone();
460 env, storm::OptimizationDirection::Maximize, abstractModel, abstractModel.
getTransitionMatrix(), maybeMax,
462 maybeMax.
ite(result.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>().getValueVector(),
463 abstractModel.
getManager().template getAddZero<ValueType>()));
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;
480 bool isRewardFormula =
482 if (!isRewardFormula) {
488 if (this->getReuseQuantitativeResults() && lastBounds.first) {
489 minStartValues = maybeMin.
ite(lastBounds.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>().getValueVector(),
490 abstractModel.
getManager().template getAddZero<ValueType>());
492 minStartValues = abstractModel.
getManager().template getAddZero<ValueType>();
495 if (isRewardFormula) {
496 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Reward properties are not supported for abstract stochastic games.");
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,
506 maybeMax.
ite(result.first->asSymbolicQuantitativeCheckResult<DdType,
ValueType>().getValueVector(),
507 abstractModel.
getManager().template getAddZero<ValueType>()));
513template<
typename ModelType>
518 STORM_LOG_TRACE(
"Performing quantative solution step. Player 1: " << player1Direction <<
", player 2: " << player2Direction <<
".");
536 std::unique_ptr<storm::solver::SymbolicGameSolver<DdType, ValueType>> solver =
540 auto values = solver->solveGame(env, player1Direction, player2Direction, startVector, subvector);
542 return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(abstractModel.
getReachableStates(),
543 prob1States.template toAdd<ValueType>() + values);
546template<
typename ModelType>
556template<
typename ModelType>
562 storm::exceptions::NotSupportedException,
"Expected discrete-time abstract model.");
570 constraintStates, targetStates);
574template<
typename ModelType>
579 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>> result =
580 std::make_unique<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>>();
582 auto start = std::chrono::high_resolution_clock::now();
583 bool isRewardFormula =
586 if (isRewardFormula) {
594 auto end = std::chrono::high_resolution_clock::now();
596 auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
597 STORM_LOG_DEBUG(
"Computed qualitative solution in " << timeInMilliseconds <<
"ms.");
599 return std::move(result);
602template<
typename ModelType>
607 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>> result =
608 std::make_unique<storm::gbar::abstraction::SymbolicQualitativeMdpResultMinMax<DdType>>();
610 auto start = std::chrono::high_resolution_clock::now();
611 bool isRewardFormula =
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()
628 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
630 abstractModel, transitionMatrixBdd, targetStates.
getStates(),
634 result->prob1Min = result->prob1Max;
637 result->prob1Max = result->prob1Min;
641 bool computedMax =
false;
642 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
646 abstractModel, transitionMatrixBdd, constraintStates.
getStates(), targetStates.
getStates(),
647 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates()
654 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
656 abstractModel, transitionMatrixBdd,
657 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates()
666 result->prob0Max = result->prob0Min;
667 result->prob1Max = result->prob1Min;
670 result->prob0Min = result->prob0Max;
671 result->prob1Min = result->prob1Max;
675 if (isRewardFormula) {
676 bool computedMin =
false;
677 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
679 abstractModel, transitionMatrixBdd, constraintStates.
getStates(), targetStates.
getStates(),
685 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
687 abstractModel, transitionMatrixBdd, targetStates.
getStates(),
691 result->prob1Min = result->prob1Max;
694 result->prob1Max = result->prob1Min;
697 bool computedMin =
false;
698 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Minimize) {
706 if (abstractionPlayer == 1 || checkTask->getOptimizationDirection() == storm::OptimizationDirection::Maximize) {
712 result->prob0Min = result->prob0Max;
713 result->prob1Min = result->prob1Max;
716 result->prob0Max = result->prob0Min;
717 result->prob1Max = result->prob1Min;
721 auto end = std::chrono::high_resolution_clock::now();
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.");
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.");
733 STORM_LOG_DEBUG(
"Computed qualitative solution in " << timeInMilliseconds <<
"ms.");
735 return std::move(result);
738template<
typename ModelType>
743 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>> result;
746 uint64_t abstractionPlayer = this->getAbstractionPlayer();
755 bool requiresSchedulers = this->requiresSchedulerSynthesis();
757 auto start = std::chrono::high_resolution_clock::now();
758 if (this->getReuseQualitativeResults()) {
759 result = computeQualitativeResultReuse(abstractModel, transitionMatrixBdd, constraintStates, targetStates, abstractionPlayer,
760 modelNondeterminismDirection, requiresSchedulers);
762 result = std::make_unique<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>>();
765 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
766 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
767 requiresSchedulers, requiresSchedulers);
769 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
770 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
771 requiresSchedulers, requiresSchedulers);
773 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
774 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
775 requiresSchedulers, requiresSchedulers);
777 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
778 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
779 requiresSchedulers, requiresSchedulers);
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'.");
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'.");
795 auto end = std::chrono::high_resolution_clock::now();
797 auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
798 STORM_LOG_DEBUG(
"Computed qualitative solution in " << timeInMilliseconds <<
"ms.");
800 return std::move(result);
803template<
typename ModelType>
804std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<AbstractAbstractionRefinementModelChecker<ModelType>::DdType>>
809 std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>> result =
810 std::make_unique<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>>();
813 if (modelNondeterminismDirection == storm::OptimizationDirection::Minimize) {
816 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize,
817 requiresSchedulers, requiresSchedulers);
822 abstractModel, transitionMatrixBdd,
823 lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Min().getStates() : targetStates.
getStates(),
828 storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize,
829 requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MinMinMdp));
833 abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
834 abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection,
835 requiresSchedulers, requiresSchedulers);
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>>());
849 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize,
850 requiresSchedulers, requiresSchedulers);
854 if (this->getReuseQualitativeResults() && lastQualitativeResults) {
855 candidates &= lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>().getProb1Max().getStates();
862 storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize,
863 requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MaxMaxMdp));
867 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
868 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
869 requiresSchedulers, requiresSchedulers);
873 abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
874 abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection,
875 requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MaxMaxMdp));
881template<
typename ModelType>
889template<
typename ModelType>
892 std::unique_ptr<storm::modelchecker::CheckResult> result;
894 auto const& symbolicQualitativeResultMinMax = lastQualitativeResults->asSymbolicQualitativeResultMinMax<DdType>();
896 bool isRewardFormula =
898 if (isRewardFormula) {
902 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
905 abstractModel.
getManager().template getAddZero<ValueType>()));
914 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
917 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
919 }
else if (checkTask->isBoundSet() && checkTask->getBoundThreshold() == storm::utility::zero<ValueType>() &&
921 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
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>() &&
927 result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
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>());
944template<
typename ModelType>
947 std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds) {
948 std::unique_ptr<storm::modelchecker::CheckResult> result;
950 if (bounds.first ==
nullptr || bounds.second ==
nullptr) {
951 STORM_LOG_ASSERT(bounds.first || bounds.second,
"Expected at least one bound.");
954 return std::move(bounds.first);
956 return std::move(bounds.second);
959 if (boundsAreSufficientlyClose(bounds)) {
961 result = getAverageOfBounds(bounds);
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.");
978 STORM_LOG_ASSERT(bounds.second->isSymbolicQuantitativeCheckResult(),
"Expected symbolic quantitative check result.");
986template<
typename ModelType>
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.");
992 STORM_LOG_ASSERT(bounds.second->isSymbolicQuantitativeCheckResult(),
"Expected symbolic quantitative check result.");
996 return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(
35namespace modelchecker {
…}
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.
ValueType getMax() const
Retrieves the highest function value of any encoding.
Add< LibraryType, ValueType > sumAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Sum-abstracts from the given meta variables.
Bdd< LibraryType > toBdd() const
Converts the ADD to a BDD by mapping all values unequal to zero to 1.
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.
Bdd< LibraryType > notZero() const
Computes a BDD that represents the function in which all assignments with a function value unequal to...
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...
virtual uint_fast64_t getNonZeroCount() const override
Retrieves the number of encodings that are mapped to a non-zero value.
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.
Bdd< LibraryType > ite(Bdd< LibraryType > const &thenBdd, Bdd< LibraryType > const &elseBdd) const
Performs an if-then-else with the given operands, i.e.
std::set< storm::expressions::Variable > const & getContainedMetaVariables() const
Retrieves the set of all meta variables contained in the DD.
DdManager< LibraryType > & getDdManager() const
Retrieves the manager that is responsible for this DD.
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.
virtual ~AbstractAbstractionRefinementModelChecker()
ModelType::ValueType ValueType
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)
bool getReuseQuantitativeResults() const
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.
AbstractAbstractionRefinementModelChecker()
Constructs a model checker for the given model.
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.
FragmentSpecification & setReachabilityRewardFormulasAllowed(bool newValue)
FragmentSpecification & setRewardOperatorsAllowed(bool newValue)
SymbolicQuantitativeCheckResult< Type, ValueType > & asSymbolicQuantitativeCheckResult()
FormulaType const & getFormula() const
Retrieves the formula from this task.
bool isOnlyInitialStatesRelevantSet() const
Retrieves whether only the initial states are relevant in the computation.
virtual ValueType getMax() const =0
virtual ValueType getMin() const =0
storm::dd::Add< Type, ValueType > const & getValueVector() const
storm::dd::Bdd< Type > const & getStates() const
storm::dd::Bdd< Type > const & getReachableStates() 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.
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.
This class represents a discrete-time Markov chain.
This class represents a discrete-time Markov decision process.
Base class for all symbolic models.
storm::dd::DdManager< Type > & getManager() const
Retrieves the manager responsible for the DDs that represent this model.
RewardModelType const & getRewardModel(std::string const &rewardModelName) const
Retrieves the reward model with the given name, if one exists.
storm::dd::Add< Type, ValueType > const & getTransitionMatrix() const
Retrieves the matrix representing the transitions of the model.
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...
storm::dd::Bdd< Type > const & getInitialStates() const
Retrieves the initial states of the model.
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & getRowColumnMetaVariablePairs() const
Retrieves the pairs of row and column meta variables.
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.
storm::dd::Bdd< Type > const & getReachableStates() const
Retrieves the reachable states of the model.
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)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
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...
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)
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.
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...
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...
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...
storm::storage::BitVector performProb0A(storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
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...
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...
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)
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...