From 9b972eef205f527decc9ce1cec61a537a0877cef Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 7 Nov 2017 14:22:33 +0100 Subject: [PATCH] some bug fixes in abstraction-refinement --- .../SymbolicQualitativeResultMinMax.cpp | 5 + .../SymbolicQualitativeResultMinMax.h | 4 +- ...tractAbstractionRefinementModelChecker.cpp | 115 +++++++++++++----- ...bstractAbstractionRefinementModelChecker.h | 2 + 4 files changed, 95 insertions(+), 31 deletions(-) diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp b/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp index 502ba8caa..772ee645d 100644 --- a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp +++ b/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp @@ -5,6 +5,11 @@ namespace storm { namespace abstraction { + template + bool SymbolicQualitativeResultMinMax::isSymbolic() const { + return true; + } + template QualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Min() const { return getProb0(storm::OptimizationDirection::Minimize); diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h b/src/storm/abstraction/SymbolicQualitativeResultMinMax.h index 6ddd61320..8b9be7e23 100644 --- a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h +++ b/src/storm/abstraction/SymbolicQualitativeResultMinMax.h @@ -20,7 +20,9 @@ namespace storm { class SymbolicQualitativeResultMinMax : public QualitativeResultMinMax { public: SymbolicQualitativeResultMinMax() = default; - + + virtual bool isSymbolic() const override; + QualitativeResult const& getProb0Min() const; QualitativeResult const& getProb1Min() const; QualitativeResult const& getProb0Max() const; diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index 8d57184d3..557229481 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -130,6 +130,8 @@ namespace storm { // Try to derive the final result from the obtained bounds. result = tryToObtainResultFromBounds(*abstractModel, bounds); if (!result) { + printBoundsInformation(bounds); + auto refinementStart = std::chrono::high_resolution_clock::now(); this->refineAbstractModel(); auto refinementEnd = std::chrono::high_resolution_clock::now(); @@ -172,7 +174,6 @@ namespace storm { result = std::make_pair(lastBounds.first->clone(), lastBounds.second->clone()); filterInitialStates(abstractModel, result); - printBoundsInformation(result); // Check whether the answer can be given after the quantitative solution. if (checkForResultAfterQuantitativeCheck(abstractModel, true, result.first->asQuantitativeCheckResult())) { @@ -182,16 +183,38 @@ namespace storm { } } else { // In this case, we construct the full results from the qualitative results. - auto symbolicModel = abstractModel.template as>(); - std::unique_ptr lowerBounds = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates(), symbolicModel->getInitialStates().ite(lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates().template toAdd(), symbolicModel->getManager().template getAddZero())); - std::unique_ptr upperBounds = std::make_unique>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates(), symbolicModel->getInitialStates().ite(lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates().template toAdd(), symbolicModel->getManager().template getAddZero())); - - result = std::make_pair, std::unique_ptr>(std::move(lowerBounds), std::move(upperBounds)); + result = createBoundsFromQualitativeResults(abstractModel, *lastQualitativeResults); } return result; } + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::createBoundsFromQualitativeResults(storm::models::Model const& abstractModel, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { + + STORM_LOG_THROW(qualitativeResults.isSymbolic(), storm::exceptions::NotSupportedException, "Expected symbolic bounds."); + + return createBoundsFromQualitativeResults(*abstractModel.template as>(), qualitativeResults.asSymbolicQualitativeResultMinMax()); + } + + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::createBoundsFromQualitativeResults(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { + + std::unique_ptr lowerBounds; + std::unique_ptr upperBounds; + + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + if (isRewardFormula) { + lowerBounds = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getInitialStates().ite(qualitativeResults.getProb1Min().getStates().ite(abstractModel.getManager().template getAddZero(), abstractModel.getManager().template getConstant(storm::utility::infinity())), abstractModel.getManager().template getAddZero())); + upperBounds = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getInitialStates().ite(qualitativeResults.getProb1Max().getStates().ite(abstractModel.getManager().template getAddZero(), abstractModel.getManager().template getConstant(storm::utility::infinity())), abstractModel.getManager().template getAddZero())); + } else { + lowerBounds = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getInitialStates().ite(qualitativeResults.getProb1Min().getStates().template toAdd(), abstractModel.getManager().template getAddZero())); + upperBounds = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getInitialStates().ite(qualitativeResults.getProb1Max().getStates().template toAdd(), abstractModel.getManager().template getAddZero())); + } + + return std::make_pair, std::unique_ptr>(std::move(lowerBounds), std::move(upperBounds)); + } + template bool AbstractAbstractionRefinementModelChecker::checkForResultAfterQuantitativeCheck(storm::models::Model const& abstractModel, bool lowerBounds, QuantitativeCheckResult const& quantitativeResult) { @@ -310,22 +333,33 @@ namespace storm { } } - // FIXME: reuse previous result template std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { std::pair, std::unique_ptr> result; - + storm::dd::Bdd maybe; + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { - storm::dd::Bdd maybe = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(); - storm::dd::Add values = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(abstractModel, abstractModel.getTransitionMatrix(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybe, targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); + maybe = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(); + } else { + maybe = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); + } + + storm::dd::Add startValues; + if (this->getReuseQuantitativeResults() && lastBounds.first) { + startValues = maybe.ite(lastBounds.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero()); + } else { + startValues = abstractModel.getManager().template getAddZero(); + } + + if (isRewardFormula) { + storm::dd::Add values = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(abstractModel, abstractModel.getTransitionMatrix(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybe, targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicLinearEquationSolverFactory(), startValues); result.first = std::make_unique>(abstractModel.getReachableStates(), values); result.second = result.first->clone(); } else { - storm::dd::Bdd maybe = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); - storm::dd::Add values = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(abstractModel, abstractModel.getTransitionMatrix(), maybe, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); + storm::dd::Add values = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(abstractModel, abstractModel.getTransitionMatrix(), maybe, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicLinearEquationSolverFactory(), startValues); result.first = std::make_unique>(abstractModel.getReachableStates(), values); result.second = result.first->clone(); @@ -334,44 +368,64 @@ namespace storm { return result; } - // FIXME: reuse previous result template std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { std::pair, std::unique_ptr> result; - + storm::dd::Bdd maybeMin; + storm::dd::Bdd maybeMax; + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { - storm::dd::Bdd maybeMin = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(); - result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Minimize, abstractModel, abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin, targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); - - storm::dd::Bdd maybeMax = qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates(); + maybeMin = qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(); + maybeMax = qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates(); + } else { + maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); + maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates(); + } + + storm::dd::Add minStartValues; + if (this->getReuseQuantitativeResults() && lastBounds.first) { + minStartValues = maybeMin.ite(lastBounds.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero()); + } else { + minStartValues = abstractModel.getManager().template getAddZero(); + } + + if (isRewardFormula) { + result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Minimize, abstractModel, abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin, targetStates.getStates(), !qualitativeResults.getProb1Min().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), minStartValues); result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeReachabilityRewards(storm::OptimizationDirection::Maximize, abstractModel, abstractModel.getTransitionMatrix(), abstractModel.getTransitionMatrix().notZero(), checkTask->isRewardModelSet() ? abstractModel.getRewardModel(checkTask->getRewardModel()) : abstractModel.getRewardModel(""), maybeMin, targetStates.getStates(), !qualitativeResults.getProb1Max().getStates() && abstractModel.getReachableStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero())); } else { - storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); - result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Minimize, abstractModel, abstractModel.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), abstractModel.getManager().template getAddZero()); - - storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates(); + result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Minimize, abstractModel, abstractModel.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), minStartValues); result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper::computeUntilProbabilities(storm::OptimizationDirection::Maximize, abstractModel, abstractModel.getTransitionMatrix(), maybeMax, qualitativeResults.getProb1Max().getStates(), storm::solver::GeneralSymbolicMinMaxLinearEquationSolverFactory(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero())); } return result; } - // FIXME: reuse previous result template std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { std::pair, std::unique_ptr> result; - + storm::dd::Bdd maybeMin; + storm::dd::Bdd maybeMax; + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + if (!isRewardFormula) { + maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); + maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates(); + } + + storm::dd::Add minStartValues; + if (this->getReuseQuantitativeResults() && lastBounds.first) { + minStartValues = maybeMin.ite(lastBounds.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero()); + } else { + minStartValues = abstractModel.getManager().template getAddZero(); + } + if (isRewardFormula) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward properties are not supported for abstract stochastic games."); } else { - storm::dd::Bdd maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && abstractModel.getReachableStates(); - result.first = computeReachabilityProbabilitiesHelper(abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Min().getStates(), abstractModel.getManager().template getAddZero()); - - storm::dd::Bdd maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && abstractModel.getReachableStates(); + result.first = computeReachabilityProbabilitiesHelper(abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Minimize : checkTask->getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Min().getStates(), minStartValues); result.second = computeReachabilityProbabilitiesHelper(abstractModel, this->getAbstractionPlayer() == 1 ? storm::OptimizationDirection::Maximize : checkTask->getOptimizationDirection(), this->getAbstractionPlayer() == 2 ? storm::OptimizationDirection::Maximize : checkTask->getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Max().getStates(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult().getValueVector(), abstractModel.getManager().template getAddZero())); } @@ -460,7 +514,8 @@ namespace storm { if (isRewardFormula) { auto states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); result->prob1Min = storm::abstraction::QualitativeMdpResult(states); - states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, targetStates.getStates(), states); + + states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); result->prob1Max = storm::abstraction::QualitativeMdpResult(states); } else { auto states = storm::utility::graph::performProb0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); @@ -579,7 +634,7 @@ namespace storm { // (2) max/max: compute prob1 using the MDP functions, reuse prob1 states of last iteration to constrain the candidate states. storm::dd::Bdd candidates = abstractModel.getReachableStates() && !result->getProb0Max().getStates(); - if (this->getReuseQualitativeResults()) { + if (this->getReuseQualitativeResults() && lastQualitativeResults) { candidates &= lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates(); } storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), candidates); diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h index 060687ce2..559883e4d 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h @@ -138,6 +138,8 @@ namespace storm { void printBoundsInformation(SymbolicQuantitativeCheckResult const& lowerBounds, SymbolicQuantitativeCheckResult const& upperBounds); bool checkForResultAfterQuantitativeCheck(storm::models::Model const& abstractModel, bool lowerBounds, QuantitativeCheckResult const& result); std::unique_ptr computeReachabilityProbabilitiesHelper(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd const& maybeStates, storm::dd::Bdd const& prob1States, storm::dd::Add const& startValues); + std::pair, std::unique_ptr> createBoundsFromQualitativeResults(storm::models::Model const& abstractModel, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> createBoundsFromQualitativeResults(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); /// Tries to obtain the results from the bounds. If either of the two bounds is null, the result is assumed /// to be the non-null bound. If neither is null and the bounds are sufficiently close, the average of the