diff --git a/src/storm/abstraction/QualitativeGameResultMinMax.h b/src/storm/abstraction/QualitativeGameResultMinMax.h index 39d139767..c40338185 100644 --- a/src/storm/abstraction/QualitativeGameResultMinMax.h +++ b/src/storm/abstraction/QualitativeGameResultMinMax.h @@ -2,14 +2,14 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/QualitativeResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" #include "storm/abstraction/QualitativeGameResult.h" namespace storm { namespace abstraction { template - struct QualitativeGameResultMinMax : public QualitativeResultMinMax { + class QualitativeGameResultMinMax : public SymbolicQualitativeResultMinMax { public: QualitativeGameResultMinMax() = default; diff --git a/src/storm/abstraction/QualitativeMdpResultMinMax.h b/src/storm/abstraction/QualitativeMdpResultMinMax.h index 3c1979afc..9f2a3c130 100644 --- a/src/storm/abstraction/QualitativeMdpResultMinMax.h +++ b/src/storm/abstraction/QualitativeMdpResultMinMax.h @@ -2,14 +2,14 @@ #include "storm/storage/dd/DdType.h" -#include "storm/abstraction/QualitativeResultMinMax.h" +#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" #include "storm/abstraction/QualitativeMdpResult.h" namespace storm { namespace abstraction { template - struct QualitativeMdpResultMinMax : public QualitativeResultMinMax { + class QualitativeMdpResultMinMax : public SymbolicQualitativeResultMinMax { public: QualitativeMdpResultMinMax() = default; diff --git a/src/storm/abstraction/QualitativeResult.h b/src/storm/abstraction/QualitativeResult.h index 49f4b29ad..8d2873541 100644 --- a/src/storm/abstraction/QualitativeResult.h +++ b/src/storm/abstraction/QualitativeResult.h @@ -11,7 +11,8 @@ namespace storm { namespace abstraction { template - struct QualitativeResult { + class QualitativeResult { + public: virtual storm::dd::Bdd const& getStates() const = 0; }; diff --git a/src/storm/abstraction/QualitativeResultMinMax.cpp b/src/storm/abstraction/QualitativeResultMinMax.cpp index 4bda4dc50..95465172c 100644 --- a/src/storm/abstraction/QualitativeResultMinMax.cpp +++ b/src/storm/abstraction/QualitativeResultMinMax.cpp @@ -1,32 +1,28 @@ #include "storm/abstraction/QualitativeResultMinMax.h" -#include "storm/abstraction/QualitativeResult.h" +#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" namespace storm { namespace abstraction { - template - QualitativeResult const& QualitativeResultMinMax::getProb0Min() const { - return getProb0(storm::OptimizationDirection::Minimize); - } - - template - QualitativeResult const& QualitativeResultMinMax::getProb1Min() const { - return getProb1(storm::OptimizationDirection::Minimize); + bool QualitativeResultMinMax::isSymbolic() const { + return false; } template - QualitativeResult const& QualitativeResultMinMax::getProb0Max() const { - return getProb0(storm::OptimizationDirection::Maximize); + SymbolicQualitativeResultMinMax const& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax() const { + return static_cast const&>(*this); } template - QualitativeResult const& QualitativeResultMinMax::getProb1Max() const { - return getProb1(storm::OptimizationDirection::Maximize); + SymbolicQualitativeResultMinMax& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax() { + return static_cast&>(*this); } - template struct QualitativeResultMinMax; - template struct QualitativeResultMinMax; + template SymbolicQualitativeResultMinMax const& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax() const; + template SymbolicQualitativeResultMinMax& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax(); + template SymbolicQualitativeResultMinMax const& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax() const; + template SymbolicQualitativeResultMinMax& QualitativeResultMinMax::asSymbolicQualitativeResultMinMax(); } } diff --git a/src/storm/abstraction/QualitativeResultMinMax.h b/src/storm/abstraction/QualitativeResultMinMax.h index 5375f5880..e748d4023 100644 --- a/src/storm/abstraction/QualitativeResultMinMax.h +++ b/src/storm/abstraction/QualitativeResultMinMax.h @@ -1,31 +1,23 @@ #pragma once -#include "storm/solver/OptimizationDirection.h" - #include "storm/storage/dd/DdType.h" namespace storm { - namespace dd { - template - class Bdd; - } - namespace abstraction { + template - struct QualitativeResult; + class SymbolicQualitativeResultMinMax; - template - struct QualitativeResultMinMax { + class QualitativeResultMinMax { public: - QualitativeResultMinMax() = default; - - QualitativeResult const& getProb0Min() const; - QualitativeResult const& getProb1Min() const; - QualitativeResult const& getProb0Max() const; - QualitativeResult const& getProb1Max() const; + virtual bool isSymbolic() const; - virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; - virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; + template + SymbolicQualitativeResultMinMax const& asSymbolicQualitativeResultMinMax() const; + + template + SymbolicQualitativeResultMinMax& asSymbolicQualitativeResultMinMax(); }; + } } diff --git a/src/storm/abstraction/QuantitativeGameResultMinMax.h b/src/storm/abstraction/QuantitativeGameResultMinMax.h index 3b13b6927..c88c014f3 100644 --- a/src/storm/abstraction/QuantitativeGameResultMinMax.h +++ b/src/storm/abstraction/QuantitativeGameResultMinMax.h @@ -6,7 +6,8 @@ namespace storm { namespace abstraction { template - struct QuantitativeGameResultMinMax { + class QuantitativeGameResultMinMax { + public: QuantitativeGameResultMinMax() = default; QuantitativeGameResultMinMax(QuantitativeGameResult const& min, QuantitativeGameResult const& max) : min(min), max(max) { diff --git a/src/storm/abstraction/StateSet.cpp b/src/storm/abstraction/StateSet.cpp new file mode 100644 index 000000000..5c20ef7e0 --- /dev/null +++ b/src/storm/abstraction/StateSet.cpp @@ -0,0 +1,28 @@ +#include "storm/abstraction/StateSet.h" +#include "storm/abstraction/SymbolicStateSet.h" + +namespace storm { + namespace abstraction { + + bool StateSet::isSymbolic() const { + return false; + } + + template + SymbolicStateSet const& StateSet::asSymbolicStateSet() const { + return static_cast const&>(*this); + } + + template + SymbolicStateSet& StateSet::asSymbolicStateSet() { + return static_cast&>(*this); + } + + template SymbolicStateSet const& StateSet::asSymbolicStateSet() const; + template SymbolicStateSet& StateSet::asSymbolicStateSet(); + + template SymbolicStateSet const& StateSet::asSymbolicStateSet() const; + template SymbolicStateSet& StateSet::asSymbolicStateSet(); + + } +} diff --git a/src/storm/abstraction/StateSet.h b/src/storm/abstraction/StateSet.h new file mode 100644 index 000000000..2a4e0642d --- /dev/null +++ b/src/storm/abstraction/StateSet.h @@ -0,0 +1,23 @@ +#pragma once + +#include "storm/storage/dd/DdType.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicStateSet; + + class StateSet { + public: + virtual bool isSymbolic() const; + + template + SymbolicStateSet const& asSymbolicStateSet() const; + + template + SymbolicStateSet& asSymbolicStateSet(); + }; + + } +} diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp b/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp new file mode 100644 index 000000000..502ba8caa --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeResultMinMax.cpp @@ -0,0 +1,32 @@ +#include "storm/abstraction/SymbolicQualitativeResultMinMax.h" + +#include "storm/abstraction/QualitativeResult.h" + +namespace storm { + namespace abstraction { + + template + QualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Min() const { + return getProb0(storm::OptimizationDirection::Minimize); + } + + template + QualitativeResult const& SymbolicQualitativeResultMinMax::getProb1Min() const { + return getProb1(storm::OptimizationDirection::Minimize); + } + + template + QualitativeResult const& SymbolicQualitativeResultMinMax::getProb0Max() const { + return getProb0(storm::OptimizationDirection::Maximize); + } + + template + QualitativeResult const& SymbolicQualitativeResultMinMax::getProb1Max() const { + return getProb1(storm::OptimizationDirection::Maximize); + } + + template class SymbolicQualitativeResultMinMax; + template class SymbolicQualitativeResultMinMax; + + } +} diff --git a/src/storm/abstraction/SymbolicQualitativeResultMinMax.h b/src/storm/abstraction/SymbolicQualitativeResultMinMax.h new file mode 100644 index 000000000..6ddd61320 --- /dev/null +++ b/src/storm/abstraction/SymbolicQualitativeResultMinMax.h @@ -0,0 +1,33 @@ +#pragma once + +#include "storm/solver/OptimizationDirection.h" + +#include "storm/storage/dd/DdType.h" + +#include "storm/abstraction/QualitativeResultMinMax.h" + +namespace storm { + namespace dd { + template + class Bdd; + } + + namespace abstraction { + template + class QualitativeResult; + + template + class SymbolicQualitativeResultMinMax : public QualitativeResultMinMax { + public: + SymbolicQualitativeResultMinMax() = default; + + QualitativeResult const& getProb0Min() const; + QualitativeResult const& getProb1Min() const; + QualitativeResult const& getProb0Max() const; + QualitativeResult const& getProb1Max() const; + + virtual QualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0; + virtual QualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0; + }; + } +} diff --git a/src/storm/abstraction/SymbolicStateSet.cpp b/src/storm/abstraction/SymbolicStateSet.cpp new file mode 100644 index 000000000..e2a57847a --- /dev/null +++ b/src/storm/abstraction/SymbolicStateSet.cpp @@ -0,0 +1,25 @@ +#include "storm/abstraction/SymbolicStateSet.h" + +namespace storm { + namespace abstraction { + + template + SymbolicStateSet::SymbolicStateSet(storm::dd::Bdd const& states) : states(states) { + // Intentionally left empty. + } + + template + bool SymbolicStateSet::isSymbolic() const { + return true; + } + + template + storm::dd::Bdd const& SymbolicStateSet::getStates() const { + return states; + } + + template class SymbolicStateSet; + template class SymbolicStateSet; + + } +} diff --git a/src/storm/abstraction/SymbolicStateSet.h b/src/storm/abstraction/SymbolicStateSet.h new file mode 100644 index 000000000..880758d30 --- /dev/null +++ b/src/storm/abstraction/SymbolicStateSet.h @@ -0,0 +1,25 @@ +#pragma once + +#include "storm/abstraction/StateSet.h" + +#include "storm/storage/dd/DdType.h" +#include "storm/storage/dd/Bdd.h" + +namespace storm { + namespace abstraction { + + template + class SymbolicStateSet : public StateSet { + public: + SymbolicStateSet(storm::dd::Bdd const& states); + + virtual bool isSymbolic() const override; + + storm::dd::Bdd const& getStates() const; + + private: + storm::dd::Bdd states; + }; + + } +} diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp new file mode 100644 index 000000000..e37e00cd9 --- /dev/null +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.cpp @@ -0,0 +1,444 @@ +#include "storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h" + +#include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/Add.h" +#include "storm/storage/dd/Bdd.h" + +#include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" + +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StochasticTwoPlayerGame.h" + +#include "storm/modelchecker/CheckTask.h" +#include "storm/modelchecker/results/CheckResult.h" +#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" + +#include "storm/abstraction/StateSet.h" +#include "storm/abstraction/SymbolicStateSet.h" +#include "storm/abstraction/QualitativeResultMinMax.h" +#include "storm/abstraction/QualitativeMdpResult.h" +#include "storm/abstraction/QualitativeMdpResultMinMax.h" +#include "storm/abstraction/QualitativeGameResultMinMax.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/AbstractionSettings.h" + +#include "storm/utility/graph.h" + +#include "storm/utility/constants.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace modelchecker { + + template + AbstractAbstractionRefinementModelChecker::AbstractAbstractionRefinementModelChecker() : AbstractModelChecker(), checkTask(nullptr) { + storm::settings::modules::AbstractionSettings::ReuseMode reuseMode = storm::settings::getModule().getReuseMode(); + reuseQualitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Qualitative; + reuseQuantitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Quantitative; + } + + template + AbstractAbstractionRefinementModelChecker::~AbstractAbstractionRefinementModelChecker() { + // Intentionally left empty. + } + + template + bool AbstractAbstractionRefinementModelChecker::canHandle(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); + bool enableRewards = this->supportsReachabilityRewards(); + storm::logic::FragmentSpecification fragment = storm::logic::reachability().setRewardOperatorsAllowed(enableRewards).setReachabilityRewardFormulasAllowed(enableRewards); + return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet(); + } + + template + bool AbstractAbstractionRefinementModelChecker::supportsReachabilityRewards() const { + return false; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { + this->setCheckTask(checkTask.template substituteFormula(checkTask.getFormula())); + return performAbstractionRefinement(); + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { + STORM_LOG_THROW(this->supportsReachabilityRewards(), storm::exceptions::NotSupportedException, "Reachability rewards are not supported by this abstraction-refinement model checker."); + this->setCheckTask(checkTask.template substituteFormula(checkTask.getFormula())); + return performAbstractionRefinement(); + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + this->setCheckTask(checkTask.template substituteFormula(checkTask.getFormula())); + return performAbstractionRefinement(); + } + + template + void AbstractAbstractionRefinementModelChecker::setCheckTask(CheckTask const& checkTask) { + this->checkTask = std::make_unique>(checkTask); + } + + template + CheckTask::ValueType> const& AbstractAbstractionRefinementModelChecker::getCheckTask() const { + return *checkTask; + } + + template + bool AbstractAbstractionRefinementModelChecker::getReuseQualitativeResults() const { + return reuseQualitativeResults; + } + + template + bool AbstractAbstractionRefinementModelChecker::getReuseQuantitativeResults() const { + return reuseQuantitativeResults; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::performAbstractionRefinement() { + STORM_LOG_THROW(checkTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The abstraction-refinement model checkers can only compute the result for the initial states."); + + // Notify the underlying implementation that the abstraction-refinement process is being started. + this->initializeAbstractionRefinement(); + + uint64_t iterations = 0; + std::unique_ptr result; + auto start = std::chrono::high_resolution_clock::now(); + while (!result) { + ++iterations; + + // Obtain the abstract model. + auto abstractionStart = std::chrono::high_resolution_clock::now(); + std::shared_ptr> abstractModel = this->getAbstractModel(); + auto abstractionEnd = std::chrono::high_resolution_clock::now(); + 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); + + // Try to derive the final result from the obtained bounds. + std::unique_ptr finalResult = tryToObtainResultFromBounds(abstractModel, bounds); + if (finalResult) { + result = std::move(finalResult); + } else { + auto refinementStart = std::chrono::high_resolution_clock::now(); + this->refineAbstractModel(); + auto refinementEnd = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Refinement in iteration " << iterations << " completed in " << std::chrono::duration_cast(refinementEnd - refinementStart).count() << "ms."); + } + } + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Completed abstraction-refinement (" << this->getName() << ") in " << std::chrono::duration_cast(end - start).count() << "ms."); + + return result; + } + + template + std::pair, std::unique_ptr> AbstractAbstractionRefinementModelChecker::computeBounds(storm::models::Model const& abstractModel) { + // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part. + + std::pair, std::unique_ptr> result; + + // Preparation: determine the constraint states and the target states of the reachability objective. + std::pair, std::unique_ptr> constraintAndTargetStates = getConstraintAndTargetStates(abstractModel); + + // Phase (1): solve qualitatively. + qualitativeResults = computeQualitativeResult(abstractModel, *constraintAndTargetStates.first, *constraintAndTargetStates.second); + + // Check whether the answer can be given after the qualitative solution. + result.first = checkForResultAfterQualitativeCheck(abstractModel); + if (result.first) { + return result; + } + + // Check whether we should skip the quantitative solution (for example if there are initial states for which + // the value is already known to be different at this point. + bool doSkipQuantitativeSolution = skipQuantitativeSolution(abstractModel, qualitativeResults, checkTask); + STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution."); + + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(storm::models::Model const& abstractModel, storm::abstraction::StateSet const& constraintStates, storm::abstraction::StateSet const& targetStates) { + STORM_LOG_ASSERT(abstractModel.isSymbolicModel(), "Expected symbolic abstract model."); + + return computeQualitativeResult(*abstractModel.template as>(), constraintStates.asSymbolicStateSet(), targetStates.asSymbolicStateSet()); + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { + STORM_LOG_THROW(abstractModel.isOfType(storm::models::ModelType::Dtmc) || abstractModel.isOfType(storm::models::ModelType::Mdp) || abstractModel.isOfType(storm::models::ModelType::S2pg), storm::exceptions::NotSupportedException, "Expected discrete-time abstract model."); + + if (abstractModel.isOfType(storm::models::ModelType::Dtmc)) { + return computeQualitativeResult(*abstractModel.template as>(), constraintStates, targetStates); + } else if (abstractModel.isOfType(storm::models::ModelType::Mdp)) { + return computeQualitativeResult(*abstractModel.template as>(), constraintStates, targetStates); + } else { + return computeQualitativeResult(*abstractModel.template as>(), constraintStates, targetStates); + } + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { + STORM_LOG_DEBUG("Computing qualitative solution for DTMC."); + std::unique_ptr> result = std::make_unique>(); + + auto start = std::chrono::high_resolution_clock::now(); + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + storm::dd::Bdd transitionMatrixBdd = abstractModel.getTransitionMatrix().notZero(); + if (isRewardFormula) { + auto prob1 = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); + result->prob1Min = result->prob1Max = storm::abstraction::QualitativeMdpResult(prob1); + } else { + auto prob01 = storm::utility::graph::performProb01(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); + result->prob0Min = result->prob0Max = storm::abstraction::QualitativeMdpResult(prob01.first); + result->prob1Min = result->prob1Max = storm::abstraction::QualitativeMdpResult(prob01.second); + } + auto end = std::chrono::high_resolution_clock::now(); + + auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); + STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); + + return result; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { + STORM_LOG_DEBUG("Computing qualitative solution for MDP."); + std::unique_ptr> result = std::make_unique>(); + + auto start = std::chrono::high_resolution_clock::now(); + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + storm::dd::Bdd transitionMatrixBdd = abstractModel.getTransitionMatrix().notZero(); + if (this->getReuseQualitativeResults()) { + if (isRewardFormula) { + auto states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), qualitativeResults ? qualitativeResults->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); + result->prob1Max = storm::abstraction::QualitativeMdpResult(states); + } else { + auto states = storm::utility::graph::performProb0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); + result->prob0Max = storm::abstraction::QualitativeMdpResult(states); + states = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), qualitativeResults ? qualitativeResults->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, qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), states); + result->prob1Min = storm::abstraction::QualitativeMdpResult(states); + + states = storm::utility::graph::performProb0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); + result->prob0Min = storm::abstraction::QualitativeMdpResult(states); + } + } else { + if (isRewardFormula) { + auto prob1 = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::utility::graph::performProbGreater0E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); + result->prob1Min = storm::abstraction::QualitativeMdpResult(prob1); + prob1 = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, targetStates.getStates(), storm::utility::graph::performProbGreater0A(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates())); + result->prob1Max = storm::abstraction::QualitativeMdpResult(prob1); + } else { + auto prob01 = storm::utility::graph::performProb01Min(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); + result->prob0Min = storm::abstraction::QualitativeMdpResult(prob01.first); + result->prob1Min = storm::abstraction::QualitativeMdpResult(prob01.second); + prob01 = storm::utility::graph::performProb01Max(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates()); + result->prob0Max = storm::abstraction::QualitativeMdpResult(prob01.first); + result->prob1Max = storm::abstraction::QualitativeMdpResult(prob01.second); + } + } + auto end = std::chrono::high_resolution_clock::now(); + + auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); + STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); + + return result; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates) { + STORM_LOG_DEBUG("Computing qualitative solution for S2PG."); + std::unique_ptr> result; + + // Obtain the player optimization directions. + uint64_t abstractionPlayer = this->getAbstractionPlayer(); + + // Obtain direction for player 1 (model nondeterminism). + storm::OptimizationDirection modelNondeterminismDirection = this->getCheckTask().getOptimizationDirection(); + + // Convert the transition matrix to a BDD to use it in the qualitative algorithms. + storm::dd::Bdd transitionMatrixBdd = abstractModel.getTransitionMatrix().toBdd(); + + // Remembers whether we need to synthesize schedulers. + bool requiresSchedulers = this->requiresSchedulerSynthesis(); + + auto start = std::chrono::high_resolution_clock::now(); + if (this->getReuseQualitativeResults()) { + result = computeQualitativeResultReuse(abstractModel, transitionMatrixBdd, constraintStates, targetStates, abstractionPlayer, modelNondeterminismDirection, requiresSchedulers); + } else { + result = std::make_unique>(); + + result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); + result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); + result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); + result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); + } + + STORM_LOG_TRACE("Qualitative precomputation completed."); + if (abstractionPlayer == 1) { + STORM_LOG_TRACE("[" << storm::OptimizationDirection::Minimize << ", " << modelNondeterminismDirection << "]: " << result->prob0Min.player1States.getNonZeroCount() << " 'no', " << result->prob1Min.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_TRACE("[" << storm::OptimizationDirection::Maximize << ", " << modelNondeterminismDirection << "]: " << result->prob0Max.player1States.getNonZeroCount() << " 'no', " << result->prob1Max.player1States.getNonZeroCount() << " 'yes'."); + } else { + STORM_LOG_TRACE("[" << modelNondeterminismDirection << ", " << storm::OptimizationDirection::Minimize << "]: " << result->prob0Min.player1States.getNonZeroCount() << " 'no', " << result->prob1Min.player1States.getNonZeroCount() << " 'yes'."); + STORM_LOG_TRACE("[" << modelNondeterminismDirection << ", " << storm::OptimizationDirection::Maximize << "]: " << result->prob0Max.player1States.getNonZeroCount() << " 'no', " << result->prob1Max.player1States.getNonZeroCount() << " 'yes'."); + } + + auto end = std::chrono::high_resolution_clock::now(); + + auto timeInMilliseconds = std::chrono::duration_cast(end - start).count(); + STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms."); + + return result; + } + + template + std::unique_ptr::DdType>> AbstractAbstractionRefinementModelChecker::computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::dd::Bdd const& transitionMatrixBdd, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers) { + std::unique_ptr> result = std::make_unique>(); + + // Depending on the model nondeterminism direction, we choose a different order of operations. + if (modelNondeterminismDirection == storm::OptimizationDirection::Minimize) { + // (1) min/min: compute prob0 using the game functions + result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, requiresSchedulers, requiresSchedulers); + + // (2) min/min: compute prob1 using the MDP functions + storm::dd::Bdd candidates = abstractModel.getReachableStates() && !result->getProb0Min().getStates(); + storm::dd::Bdd prob1MinMinMdp = storm::utility::graph::performProb1A(abstractModel, transitionMatrixBdd, qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Min().getStates() : targetStates.getStates(), candidates); + + // (3) min/min: compute prob1 using the game functions + result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MinMinMdp)); + + // (4) min/max, max/min: compute prob 0 using the game functions + result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); + + // (5) min/max, max/min: compute prob 1 using the game functions + // We know that only previous prob1 states can now be prob 1 states again, because the upper bound + // values can only decrease over iterations. + result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Maximize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers, qualitativeResults ? qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates() : boost::optional>()); + } else { + // (1) max/max: compute prob0 using the game functions + result->prob0Max = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, requiresSchedulers, requiresSchedulers); + + // (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()) { + candidates &= qualitativeResults->asSymbolicQualitativeResultMinMax().getProb1Max().getStates(); + } + storm::dd::Bdd prob1MaxMaxMdp = storm::utility::graph::performProb1E(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), candidates); + + // (3) max/max: compute prob1 using the game functions, reuse prob1 states from the MDP precomputation + result->prob1Max = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MaxMaxMdp)); + + // (4) max/min, min/max: compute prob0 using the game functions + result->prob0Min = storm::utility::graph::performProb0(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers); + + // (5) max/min:, max/min compute prob1 using the game functions, use prob1 from max/max as the candidate set + result->prob1Min = storm::utility::graph::performProb1(abstractModel, transitionMatrixBdd, constraintStates.getStates(), targetStates.getStates(), abstractionPlayer == 1 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, abstractionPlayer == 2 ? storm::OptimizationDirection::Minimize : modelNondeterminismDirection, requiresSchedulers, requiresSchedulers, boost::make_optional(prob1MaxMaxMdp)); + } + + return result; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::checkForResultAfterQualitativeCheck(storm::models::Model const& abstractModel) { + STORM_LOG_THROW(abstractModel.isSymbolicModel(), storm::exceptions::NotSupportedException, "Expected symbolic model."); + + return checkForResultAfterQualitativeCheck(*abstractModel.template as>()); + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::checkForResultAfterQualitativeCheck(storm::models::symbolic::Model const& abstractModel) { + std::unique_ptr result; + + auto const& symbolicQualitativeResultMinMax = qualitativeResults->asSymbolicQualitativeResultMinMax(); + + bool isRewardFormula = checkTask->getFormula().isEventuallyFormula() && checkTask->getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; + if (isRewardFormula) { + // In the reachability reward case, we can give an answer if all initial states of the system are infinity + // states in the min result. + if ((abstractModel.getInitialStates() && !symbolicQualitativeResultMinMax.getProb1Min().getStates()) == abstractModel.getInitialStates()) { + result = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getInitialStates().ite(abstractModel.getManager().getConstant(storm::utility::infinity()), abstractModel.getManager().template getAddZero())); + } + } else { + // In the reachability probability case, we can give the answer if all initial states are prob1 states + // in the min result or if all initial states are prob0 in the max case. + // Furthermore, we can give the answer if there are initial states with probability > 0 in the min case + // and the probability bound was 0 or if there are initial states with probability < 1 in the max case + // and the probability bound was 1. + if ((abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb1Min().getStates()) == abstractModel.getInitialStates()) { + result = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getManager().template getAddOne()); + } else if ((abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb0Max().getStates()) == abstractModel.getInitialStates()) { + result = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), abstractModel.getManager().template getAddZero()); + } else if (checkTask->isBoundSet() && checkTask->getBoundThreshold() == storm::utility::zero() && (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb0Min().getStates()) != abstractModel.getInitialStates()) { + result = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb0Min().getStates()).ite(abstractModel.getManager().template getConstant(0.5), abstractModel.getManager().template getAddZero())); + } else if (checkTask->isBoundSet() && checkTask->getBoundThreshold() == storm::utility::one() && (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb1Max().getStates()) != abstractModel.getInitialStates()) { + result = std::make_unique>(abstractModel.getReachableStates(), abstractModel.getInitialStates(), (abstractModel.getInitialStates() && symbolicQualitativeResultMinMax.getProb1Max().getStates()).ite(abstractModel.getManager().template getConstant(0.5), abstractModel.getManager().template getAddZero()) + symbolicQualitativeResultMinMax.getProb1Max().getStates().template toAdd()); + } + } + + return result; + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::tryToObtainResultFromBounds(std::shared_ptr> const& abstractModel, std::pair, std::unique_ptr>& bounds) { + std::unique_ptr result; + + if (bounds.first == nullptr || bounds.second == nullptr) { + STORM_LOG_ASSERT(bounds.first || bounds.second, "Expected at least one bound."); + + if (bounds.first) { + return std::move(bounds.first); + } else { + return std::move(bounds.second); + } + } else { + if (boundsAreSufficientlyClose(bounds)) { + result = getAverageOfBounds(bounds); + } + } + + if (result) { + abstractModel->printModelInformationToStream(std::cout); + } + + return result; + } + + template + bool AbstractAbstractionRefinementModelChecker::boundsAreSufficientlyClose(std::pair, std::unique_ptr> const& bounds) { + STORM_LOG_ASSERT(bounds.first->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); + STORM_LOG_ASSERT(bounds.second->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); + + return lowerBounds.getValueVector().equalModuloPrecision(upperBounds.getValueVector(), storm::settings::getModule().getPrecision(), false); + } + + template + std::unique_ptr AbstractAbstractionRefinementModelChecker::getAverageOfBounds(std::pair, std::unique_ptr> const& bounds) { + STORM_LOG_ASSERT(bounds.first->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& lowerBounds = bounds.first->asSymbolicQuantitativeCheckResult(); + STORM_LOG_ASSERT(bounds.second->isSymbolicQuantitativeCheckResult(), "Expected symbolic quantitative check result."); + storm::modelchecker::SymbolicQuantitativeCheckResult const& upperBounds = bounds.second->asSymbolicQuantitativeCheckResult(); + + return std::make_unique>(lowerBounds.getReachableStates(), lowerBounds.getStates(), (lowerBounds.getValueVector() + upperBounds.getValueVector()) / lowerBounds.getValueVector().getDdManager().getConstant(storm::utility::convertNumber(std::string("2.0")))); + } + + template class AbstractAbstractionRefinementModelChecker>; + template class AbstractAbstractionRefinementModelChecker>; + template class AbstractAbstractionRefinementModelChecker>; + template class AbstractAbstractionRefinementModelChecker>; + + } +} + diff --git a/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h new file mode 100644 index 000000000..6b2f3a41c --- /dev/null +++ b/src/storm/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h @@ -0,0 +1,153 @@ +#pragma once + +#include "storm/modelchecker/AbstractModelChecker.h" +#include "storm/storage/dd/DdType.h" + +namespace storm { + namespace dd { + template + class Bdd; + } + + namespace models { + template + class Model; + + namespace symbolic { + template + class Model; + + template + class Dtmc; + + template + class Mdp; + + template + class StochasticTwoPlayerGame; + } + } + + namespace abstraction { + class QualitativeResultMinMax; + + template + class SymbolicQualitativeResultMinMax; + + template + class QualitativeMdpResultMinMax; + + template + class QualitativeGameResultMinMax; + + class StateSet; + + template + class SymbolicStateSet; + } + + namespace modelchecker { + template + class SymbolicMdpPrctlModelChecker; + + template + class QuantitativeCheckResult; + + template + class AbstractAbstractionRefinementModelChecker : public AbstractModelChecker { + public: + typedef typename ModelType::ValueType ValueType; + static const storm::dd::DdType DdType = ModelType::DdType; + + /*! + * Constructs a model checker for the given model. + */ + explicit AbstractAbstractionRefinementModelChecker(); + + ~AbstractAbstractionRefinementModelChecker(); + + /// Overridden methods from super class. + virtual bool canHandle(CheckTask const& checkTask) const override; + virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + + protected: + /// -------- Methods that need to be overwritten/defined by implementations in subclasses. + + /// Determines whether the model checker can handle reachability rewards or only reachability probabilities. + virtual bool supportsReachabilityRewards() const; + + /// Retrieves the name of the underlying method. + virtual std::string const& getName() const = 0; + + /// Called before the abstraction refinement loop to give the implementation a time to set up auxiliary data. + virtual void initializeAbstractionRefinement() = 0; + + /// Retrieves the abstract model. + virtual std::shared_ptr> getAbstractModel() = 0; + + /// Retrieves the state sets corresponding to the constraint and target states. + virtual std::pair, std::unique_ptr> getConstraintAndTargetStates(storm::models::Model const& abstractModel) = 0; + + /// Retrieves the index of the abstraction player. Must be in {0} for DTMCs, {1} for MDPs and in {1, 2} for games. + virtual uint64_t getAbstractionPlayer() const = 0; + + /// Retrieves whether schedulers need to be computed. + virtual bool requiresSchedulerSynthesis() const = 0; + + /// Refines the abstract model so that the next iteration obtains bounds that are at least as precise as + /// current ones. + virtual void refineAbstractModel() = 0; + + /// -------- Methods used to implement the abstraction refinement procedure. + + /// 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); + + /// 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); + std::unique_ptr computeQualitativeResult(storm::models::symbolic::Model const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); + std::unique_ptr computeQualitativeResult(storm::models::symbolic::Dtmc const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); + std::unique_ptr computeQualitativeResult(storm::models::symbolic::Mdp const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); + std::unique_ptr computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates); + std::unique_ptr> computeQualitativeResultReuse(storm::models::symbolic::StochasticTwoPlayerGame const& abstractModel, storm::dd::Bdd const& transitionMatrixBdd, storm::abstraction::SymbolicStateSet const& constraintStates, storm::abstraction::SymbolicStateSet const& targetStates, uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers); + std::unique_ptr checkForResultAfterQualitativeCheck(storm::models::Model const& abstractModel); + std::unique_ptr checkForResultAfterQualitativeCheck(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); + /// 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 + /// bounds are sufficiently close. + std::unique_ptr getAverageOfBounds(std::pair, std::unique_ptr> const& bounds); + + /// Methods to set/get the check task that is currently handled. + void setCheckTask(CheckTask const& checkTask); + CheckTask const& getCheckTask() const; + + /// Methods that retrieve which results shall be reused. + bool getReuseQualitativeResults() const; + bool getReuseQuantitativeResults() const; + + private: + /// The check task that is currently handled. + std::unique_ptr const> checkTask; + + /// A flag indicating whether to reuse the qualitative results. + bool reuseQualitativeResults; + + /// A flag indicating whether to reuse the quantitative results. + bool reuseQuantitativeResults; + + /// The last qualitative results. + std::unique_ptr qualitativeResults; + }; + } +} diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp index 3a2686398..4175a2ced 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp @@ -65,7 +65,6 @@ namespace storm { template std::unique_ptr PartialBisimulationMdpModelChecker::computeValuesAbstractionRefinement(CheckTask const& checkTask) { - STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states."); // Create the appropriate preservation information. @@ -307,7 +306,7 @@ namespace storm { } template - std::unique_ptr PartialBisimulationMdpModelChecker::checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { + std::unique_ptr PartialBisimulationMdpModelChecker::checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { std::unique_ptr result; bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; @@ -338,7 +337,7 @@ namespace storm { } template - bool PartialBisimulationMdpModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { + bool PartialBisimulationMdpModelChecker::skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask) { bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward; if (isRewardFormula) { @@ -356,7 +355,7 @@ namespace storm { } template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { std::pair, std::unique_ptr> result; @@ -405,7 +404,7 @@ namespace storm { } template - std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults) { + std::pair, std::unique_ptr> PartialBisimulationMdpModelChecker::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults) { std::pair, std::unique_ptr> result; diff --git a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h index 0916bb930..eb129c711 100644 --- a/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h +++ b/src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h @@ -33,13 +33,13 @@ namespace storm { namespace abstraction { template - struct QualitativeResultMinMax; + class SymbolicQualitativeResultMinMax; template - struct QualitativeMdpResultMinMax; + class QualitativeMdpResultMinMax; template - struct QualitativeGameResultMinMax; + class QualitativeGameResultMinMax; } namespace modelchecker { @@ -77,12 +77,12 @@ namespace storm { // Methods related to the qualitative solution. storm::abstraction::QualitativeMdpResultMinMax computeQualitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates); storm::abstraction::QualitativeGameResultMinMax computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::OptimizationDirection optimizationDirectionInModel); - std::unique_ptr checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); - bool skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::QualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); + std::unique_ptr checkForResult(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); + bool skipQuantitativeSolution(storm::models::symbolic::Model const& quotient, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults, CheckTask const& checkTask); // Methods related to the quantitative solution. - std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); - std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::QualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::Mdp const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); + std::pair, std::unique_ptr> computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame const& quotient, CheckTask const& checkTask, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& targetStates, storm::abstraction::SymbolicQualitativeResultMinMax const& qualitativeResults); // Retrieves the constraint and target states of the quotient wrt. to the formula in the check task. template diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 39be2fbaa..ea7746bb9 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -29,7 +29,7 @@ namespace storm { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states."); - std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); + std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix.notZero(), phiStates, psiStates); storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining)."); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index ffc602aaa..28c3f57db 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -23,7 +23,7 @@ namespace storm { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states."); - std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); + std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix.notZero(), phiStates, psiStates); storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining)."); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 889734d45..c12ca39e5 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -376,11 +376,10 @@ namespace storm { } template - std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { + std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) { std::pair, storm::dd::Bdd> result; - storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); - result.first = performProbGreater0(model, transitionMatrixBdd, phiStates, psiStates); - result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); + result.first = performProbGreater0(model, transitionMatrix, phiStates, psiStates); + result.second = !performProbGreater0(model, transitionMatrix, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates(); result.first = !result.first && model.getReachableStates(); return result; } @@ -1539,7 +1538,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template storm::dd::Bdd computeSchedulerProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1579,7 +1578,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template storm::dd::Bdd computeSchedulerProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1619,7 +1618,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template storm::dd::Bdd computeSchedulerProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); @@ -1655,7 +1654,7 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template storm::dd::Bdd computeSchedulerProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 79cefffc2..0f9b3c66e 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -237,7 +237,7 @@ namespace storm { * @return A pair of BDDs that represent all states with probability 0 and 1, respectively. */ template - std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes a scheduler for the given states that chooses an action that stays completely in the very same set.