From 183eea7a892ec1bb9cf9f0e8ed023e69af2d0733 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 2 Nov 2017 16:35:44 +0100 Subject: [PATCH] more work on abstraction refinement framework --- ...tractAbstractionRefinementModelChecker.cpp | 61 ++++++++++++++++--- ...bstractAbstractionRefinementModelChecker.h | 13 +++- 2 files changed, 64 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index e37e00cd9..123a772cc 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -119,13 +119,11 @@ namespace storm { STORM_LOG_TRACE("Model in iteration " << iterations << " has " << abstractModel->getNumberOfStates() << " states and " << abstractModel->getNumberOfTransitions() << " transitions (retrieved in " << std::chrono::duration_cast(abstractionEnd - abstractionStart).count() << "ms)."); // Obtain lower and upper bounds from the abstract model. - std::pair, std::unique_ptr> bounds = computeBounds(*abstractModel); + computeBounds(*abstractModel); // Try to derive the final result from the obtained bounds. - std::unique_ptr finalResult = tryToObtainResultFromBounds(abstractModel, bounds); - if (finalResult) { - result = std::move(finalResult); - } else { + result = tryToObtainResultFromBounds(abstractModel, this->bounds); + if (!result) { auto refinementStart = std::chrono::high_resolution_clock::now(); this->refineAbstractModel(); auto refinementEnd = std::chrono::high_resolution_clock::now(); @@ -161,6 +159,55 @@ namespace storm { bool doSkipQuantitativeSolution = skipQuantitativeSolution(abstractModel, qualitativeResults, checkTask); STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution."); + // Phase (2): solve quantitatively. + if (!doSkipQuantitativeSolution) { + result = computeQuantitativeResult(abstractModel, checkTask, constraintTargetStates.first, constraintTargetStates.second, qualitativeResults); + +// storm::modelchecker::SymbolicQualitativeCheckResult initialStateFilter(quotient.getReachableStates(), quotient.getInitialStates()); +// result.first->filter(initialStateFilter); +// result.second->filter(initialStateFilter); +// printBoundsInformation(result); +// +// // Check whether the answer can be given after the quantitative solution. +// if (checkForResult(abstractModel, true, result.first->asQuantitativeCheckResult(), checkTask)) { +// result.second = nullptr; +// } +// if (checkForResult(abstractModel, false, result.second->asQuantitativeCheckResult(), checkTask)) { +// result.first = nullptr; +// } + } else { + // In this case, we construct the full results from the qualitative results. + + } + + // + fullResults = result; + + return result; + } + + template + bool AbstractAbstractionRefinementModelChecker::skipQuantitativeSolution(storm::models::Model const& abstractModel) { + STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model."); + + return skipQuantitativeSolution(*abstractModel.template as>()); + } + + template + bool AbstractAbstractionRefinementModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& abstractModel) { + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + if (isRewardFormula) { + if ((abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates())) { + return true; + } + } else { + if ((abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb0Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb0Max().getStates())) { + return true; + } else if ((abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates()) != (abstractModel.getInitialStates() && qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates())) { + return true; + } + } + return false; } template @@ -390,7 +437,7 @@ namespace storm { } template - std::unique_ptr AbstractAbstractionRefinementModelChecker::tryToObtainResultFromBounds(std::shared_ptr> const& abstractModel, std::pair, std::unique_ptr>& bounds) { + std::unique_ptr AbstractAbstractionRefinementModelChecker::tryToObtainResultFromBounds(storm::models::Model const& abstractModel, std::pair, std::unique_ptr>& bounds) { std::unique_ptr result; if (bounds.first == nullptr || bounds.second == nullptr) { @@ -408,7 +455,7 @@ namespace storm { } if (result) { - abstractModel->printModelInformationToStream(std::cout); + abstractModel.printModelInformationToStream(std::cout); } return result; diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h index 6b2f3a41c..9d9f3a7ef 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h @@ -105,8 +105,8 @@ namespace storm { /// Performs the actual abstraction refinement loop. std::unique_ptr performAbstractionRefinement(); - /// Computes lower and upper bounds on the - std::pair, std::unique_ptr> computeBounds(storm::models::Model const& abstractModel); + /// Computes lower and upper bounds on the abstract model and stores them in a member. + void computeBounds(storm::models::Model const& abstractModel); /// Solves the current check task qualitatively, i.e. computes all states with probability 0/1. std::unique_ptr computeQualitativeResult(storm::models::Model const& abstractModel, storm::abstraction::StateSet const& constraintStates, storm::abstraction::StateSet const& targetStates); @@ -118,10 +118,14 @@ namespace storm { std::unique_ptr checkForResultAfterQualitativeCheck(storm::models::Model const& abstractModel); std::unique_ptr checkForResultAfterQualitativeCheck(storm::models::symbolic::Model const& abstractModel); + // Methods related to the quantitative solution. + bool skipQuantitativeSolution(storm::models::Model const& abstractModel); + bool skipQuantitativeSolution(storm::models::symbolic::Model const& abstractModel); + /// 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 /// bounds is returned. - std::unique_ptr tryToObtainResultFromBounds(std::shared_ptr> const& model, std::pair, std::unique_ptr>& bounds); + std::unique_ptr tryToObtainResultFromBounds(storm::models::Model const& model, std::pair, std::unique_ptr>& bounds); /// Checks whether the provided bounds are sufficiently close to terminate. bool boundsAreSufficientlyClose(std::pair, std::unique_ptr> const& bounds); /// Retrieves the average of the two bounds. This should only be used to derive the overall result when the @@ -148,6 +152,9 @@ namespace storm { /// The last qualitative results. std::unique_ptr qualitativeResults; + + /// The last full result that was obtained. + std::pair, std::unique_ptr> bounds; }; } }