From 57a6115beb8be0cdb1b09f2f318097fe06f25960 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 7 Nov 2017 11:15:33 +0100 Subject: [PATCH] new bisimulation-based abstraction-refinement model checker that uses the new abstraction-refinement framework --- src/storm/api/verification.h | 6 +- ...tractAbstractionRefinementModelChecker.cpp | 61 +++++--- ...ationAbstractionRefinementModelChecker.cpp | 142 +++++++++++++----- ...ulationAbstractionRefinementModelChecker.h | 19 ++- .../PartialBisimulationMdpModelChecker.cpp | 2 +- 5 files changed, 159 insertions(+), 71 deletions(-) diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h index ab787123a..4f7c59dbc 100644 --- a/src/storm/api/verification.h +++ b/src/storm/api/verification.h @@ -12,7 +12,7 @@ #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h" #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" -#include "storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h" +#include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" @@ -68,12 +68,12 @@ namespace storm { typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { - storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(*model->template as>()); + storm::modelchecker::BisimulationAbstractionRefinementModelChecker> modelchecker(*model->template as>()); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } } else if (model->getType() == storm::models::ModelType::Mdp) { - storm::modelchecker::PartialBisimulationMdpModelChecker> modelchecker(*model->template as>()); + storm::modelchecker::BisimulationAbstractionRefinementModelChecker> modelchecker(*model->template as>()); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); } diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp index 82461f576..8d57184d3 100644 --- a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -168,7 +168,8 @@ namespace storm { // Phase (2): solve quantitatively. if (!doSkipQuantitativeSolution) { lastBounds = computeQuantitativeResult(abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second, *lastQualitativeResults); - + STORM_LOG_ASSERT(lastBounds.first && lastBounds.second, "Expected both bounds."); + result = std::make_pair(lastBounds.first->clone(), lastBounds.second->clone()); filterInitialStates(abstractModel, result); printBoundsInformation(result); @@ -176,8 +177,7 @@ namespace storm { // Check whether the answer can be given after the quantitative solution. if (checkForResultAfterQuantitativeCheck(abstractModel, true, result.first->asQuantitativeCheckResult())) { result.second = nullptr; - } - if (checkForResultAfterQuantitativeCheck(abstractModel, false, result.second->asQuantitativeCheckResult())) { + } else if (checkForResultAfterQuantitativeCheck(abstractModel, false, result.second->asQuantitativeCheckResult())) { result.first = nullptr; } } else { @@ -193,27 +193,37 @@ namespace storm { } template - bool AbstractAbstractionRefinementModelChecker::checkForResultAfterQuantitativeCheck(storm::models::Model const& abstractModel, bool lowerBounds, QuantitativeCheckResult const& result) { - storm::logic::ComparisonType comparisonType = checkTask->getBoundComparisonType(); - ValueType threshold = checkTask->getBoundThreshold(); + bool AbstractAbstractionRefinementModelChecker::checkForResultAfterQuantitativeCheck(storm::models::Model const& abstractModel, bool lowerBounds, QuantitativeCheckResult const& quantitativeResult) { - if (lowerBounds) { - if (storm::logic::isLowerBound(comparisonType)) { - ValueType minimalLowerBound = result.getMin(); - return (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold); + bool result = false; + if (checkTask->isBoundSet()) { + storm::logic::ComparisonType comparisonType = checkTask->getBoundComparisonType(); + ValueType threshold = checkTask->getBoundThreshold(); + + if (lowerBounds) { + if (storm::logic::isLowerBound(comparisonType)) { + ValueType minimalLowerBound = quantitativeResult.getMin(); + result = (storm::logic::isStrict(comparisonType) && minimalLowerBound > threshold) || (!storm::logic::isStrict(comparisonType) && minimalLowerBound >= threshold); + } else { + ValueType maximalLowerBound = quantitativeResult.getMax(); + result = (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold); + } } else { - ValueType maximalLowerBound = result.getMax(); - return (storm::logic::isStrict(comparisonType) && maximalLowerBound >= threshold) || (!storm::logic::isStrict(comparisonType) && maximalLowerBound > threshold); + if (storm::logic::isLowerBound(comparisonType)) { + ValueType minimalUpperBound = quantitativeResult.getMin(); + result = (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold); + } else { + ValueType maximalUpperBound = quantitativeResult.getMax(); + result = (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold); + } } - } else { - if (storm::logic::isLowerBound(comparisonType)) { - ValueType minimalUpperBound = result.getMin(); - return (storm::logic::isStrict(comparisonType) && minimalUpperBound <= threshold) || (!storm::logic::isStrict(comparisonType) && minimalUpperBound < threshold); - } else { - ValueType maximalUpperBound = result.getMax(); - return (storm::logic::isStrict(comparisonType) && maximalUpperBound < threshold) || (!storm::logic::isStrict(comparisonType) && maximalUpperBound <= threshold); + + if (result) { + STORM_LOG_TRACE("Check for result after quantiative check positive."); } } + + return result; } template @@ -458,7 +468,7 @@ namespace storm { 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->prob1Max = storm::abstraction::QualitativeMdpResult(states); - states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), states); + states = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, lastQualitativeResults ? lastQualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); result->prob1Min = storm::abstraction::QualitativeMdpResult(states); states = storm::utility::graph::performProb0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); @@ -482,6 +492,13 @@ namespace storm { auto end = std::chrono::high_resolution_clock::now(); auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); + if (isRewardFormula) { + STORM_LOG_TRACE("Min: " << result->getProb1Min().getStates().getNonZeroCount() << " states with probability 1."); + STORM_LOG_TRACE("Max: " << result->getProb1Max().getStates().getNonZeroCount() << " states with probability 1."); + } else { + STORM_LOG_TRACE("Min: " << result->getProb0Min().getStates().getNonZeroCount() << " states with probability 0, " << result->getProb1Min().getStates().getNonZeroCount() << " states with probability 1."); + STORM_LOG_TRACE("Max: " << result->getProb0Max().getStates().getNonZeroCount() << " states with probability 0, " << result->getProb1Max().getStates().getNonZeroCount() << " states with probability 1."); + } STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); return result; @@ -617,6 +634,10 @@ namespace storm { } } + if (result) { + STORM_LOG_TRACE("Check for result after qualitative check positive."); + } + return result; } diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp index e3f2c28ed..d7bb3f53e 100644 --- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.cpp @@ -2,6 +2,17 @@ #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StochasticTwoPlayerGame.h" + +#include "storm/abstraction/SymbolicStateSet.h" + +#include "storm/storage/dd/BisimulationDecomposition.h" + +#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" +#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { namespace modelchecker { @@ -19,45 +30,98 @@ namespace storm { // Intentionally left empty. } -// template -// bool BisimulationAbstractionRefinementModelChecker::supportsReachabilityRewards() const { -// return true; -// } -// -// template -// std::string const& BisimulationAbstractionRefinementModelChecker::getName() const { -// return name; -// } -// -// template -// void BisimulationAbstractionRefinementModelChecker::initializeAbstractionRefinement() { -// -// } -// -// template -// std::shared_ptr::ValueType>> BisimulationAbstractionRefinementModelChecker::getAbstractModel() { -// -// } -// -// template -// std::pair, std::unique_ptr> BisimulationAbstractionRefinementModelChecker::getConstraintAndTargetStates(storm::models::Model const& abstractModel) { -// -// } -// -// template -// uint64_t BisimulationAbstractionRefinementModelChecker::getAbstractionPlayer() const { -// return 1; -// } -// -// template -// bool BisimulationAbstractionRefinementModelChecker::requiresSchedulerSynthesis() const { -// return false; -// } -// -// template -// void BisimulationAbstractionRefinementModelChecker::refineAbstractModel() { -// -// } + template + bool BisimulationAbstractionRefinementModelChecker::supportsReachabilityRewards() const { + return true; + } + + template + std::string const& BisimulationAbstractionRefinementModelChecker::getName() const { + return name; + } + + template + void BisimulationAbstractionRefinementModelChecker::initializeAbstractionRefinement() { + // Create the appropriate preservation information. + auto const& checkTask = this->getCheckTask(); + storm::dd::bisimulation::PreservationInformation preservationInformation(model, {checkTask.getFormula().asSharedPointer()}); + if (checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward) { + if (!checkTask.isRewardModelSet() || model.hasUniqueRewardModel()) { + preservationInformation.addRewardModel(model.getUniqueRewardModelName()); + } else if (checkTask.isRewardModelSet()) { + preservationInformation.addRewardModel(checkTask.getRewardModel()); + } + } + + // Create the bisimulation object. + this->bisimulation = std::make_unique>(this->model, storm::storage::BisimulationType::Strong, preservationInformation); + } + + template + std::shared_ptr::ValueType>> BisimulationAbstractionRefinementModelChecker::getAbstractModel() { + lastAbstractModel = this->bisimulation->getQuotient(); + return lastAbstractModel; + } + + template + std::pair, std::unique_ptr> BisimulationAbstractionRefinementModelChecker::getConstraintAndTargetStates(storm::models::Model const& abstractModel) { + + STORM_LOG_ASSERT(lastAbstractModel, "Expected abstract model."); + std::pair, storm::dd::Bdd> ddResult; + if (lastAbstractModel->isOfType(storm::models::ModelType::Dtmc)) { + ddResult = this->getConstraintAndTargetStates(*lastAbstractModel->template as>()); + } else if (lastAbstractModel->isOfType(storm::models::ModelType::Mdp)) { + ddResult = this->getConstraintAndTargetStates(*lastAbstractModel->template as>()); + } else { + ddResult = this->getConstraintAndTargetStates(*lastAbstractModel->template as>()); + } + + std::pair, std::unique_ptr> result; + result.first = std::make_unique>(ddResult.first); + result.second = std::make_unique>(ddResult.second); + return result; + } + + template + template + std::pair::DdType>, storm::dd::Bdd::DdType>> BisimulationAbstractionRefinementModelChecker::getConstraintAndTargetStates(QuotientModelType const& quotient) { + std::pair, storm::dd::Bdd> result; + + auto const& checkTask = this->getCheckTask(); + + SymbolicPropositionalModelChecker checker(quotient); + if (checkTask.getFormula().isUntilFormula()) { + std::unique_ptr subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula()); + result.first = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); + subresult = checker.check(checkTask.getFormula().asUntilFormula().getRightSubformula()); + result.second = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); + } else if (checkTask.getFormula().isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula().asEventuallyFormula(); + result.first = quotient.getReachableStates(); + std::unique_ptr subresult = checker.check(eventuallyFormula.getSubformula()); + result.second = subresult->asSymbolicQualitativeCheckResult().getTruthValuesVector(); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The given formula is not supported by this model checker."); + } + + return result; + } + + template + uint64_t BisimulationAbstractionRefinementModelChecker::getAbstractionPlayer() const { + return 1; + } + + template + bool BisimulationAbstractionRefinementModelChecker::requiresSchedulerSynthesis() const { + return false; + } + + template + void BisimulationAbstractionRefinementModelChecker::refineAbstractModel() { + STORM_LOG_ASSERT(bisimulation, "Bisimulation object required."); + this->bisimulation->compute(10); + } template class BisimulationAbstractionRefinementModelChecker>; template class BisimulationAbstractionRefinementModelChecker>; diff --git a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h index c46612dde..9af7c3a8b 100644 --- a/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h +++ b/src/storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h @@ -31,16 +31,19 @@ namespace storm { virtual ~BisimulationAbstractionRefinementModelChecker(); protected: -// virtual bool supportsReachabilityRewards() const override; -// virtual std::string const& getName() const override; -// virtual void initializeAbstractionRefinement() override; -// virtual std::shared_ptr> getAbstractModel() override; -// virtual std::pair, std::unique_ptr> getConstraintAndTargetStates(storm::models::Model const& abstractModel) override; -// virtual uint64_t getAbstractionPlayer() const override; -// virtual bool requiresSchedulerSynthesis() const override; -// virtual void refineAbstractModel() override; + virtual bool supportsReachabilityRewards() const override; + virtual std::string const& getName() const override; + virtual void initializeAbstractionRefinement() override; + virtual std::shared_ptr> getAbstractModel() override; + virtual std::pair, std::unique_ptr> getConstraintAndTargetStates(storm::models::Model const& abstractModel) override; + virtual uint64_t getAbstractionPlayer() const override; + virtual bool requiresSchedulerSynthesis() const override; + virtual void refineAbstractModel() override; private: + template + std::pair, storm::dd::Bdd> getConstraintAndTargetStates(QuotientModelType const& quotient); + ModelType const& model; /// The bisimulation object that maintains and refines the model. diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index cb2e0c725..26423bb87 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -122,7 +122,7 @@ namespace storm { if (!converged) { STORM_LOG_TRACE("Performing bisimulation step."); - bisimulation.compute(1); + bisimulation.compute(10); } }