From 92beab426f71562fa6a3c55e1c2d3a98e8d071c6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 28 Feb 2017 16:50:07 +0100 Subject: [PATCH] created a modelCheckerHint class that allows to store all kinds of hints that a model checker might make use of --- src/storm/modelchecker/CheckTask.h | 45 ++++------- .../hints/ExplicitModelCheckerHint.cpp | 81 +++++++++++++++++++ .../hints/ExplicitModelCheckerHint.h | 48 +++++++++++ .../modelchecker/hints/ModelCheckerHint.cpp | 34 ++++++++ .../modelchecker/hints/ModelCheckerHint.h | 36 +++++++++ .../SparseDtmcInstantiationModelChecker.cpp | 17 ++-- .../SparseDtmcInstantiationModelChecker.h | 6 +- .../SparseMdpInstantiationModelChecker.cpp | 18 +++-- .../SparseMdpInstantiationModelChecker.h | 4 - .../prctl/SparseDtmcPrctlModelChecker.cpp | 4 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 4 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 21 ++--- .../prctl/helper/SparseDtmcPrctlHelper.h | 9 ++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 41 ++++++---- .../prctl/helper/SparseMdpPrctlHelper.h | 9 ++- .../ExplicitQuantitativeCheckResult.cpp | 6 ++ .../results/ExplicitQuantitativeCheckResult.h | 1 + src/storm/storage/TotalScheduler.cpp | 5 ++ src/storm/storage/TotalScheduler.h | 8 ++ 19 files changed, 304 insertions(+), 93 deletions(-) create mode 100644 src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp create mode 100644 src/storm/modelchecker/hints/ExplicitModelCheckerHint.h create mode 100644 src/storm/modelchecker/hints/ModelCheckerHint.cpp create mode 100644 src/storm/modelchecker/hints/ModelCheckerHint.h diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 435a25e45..3caba461c 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -2,12 +2,14 @@ #define STORM_MODELCHECKER_CHECKTASK_H_ #include +#include #include "storm/logic/Formulas.h" #include "storm/utility/constants.h" #include "storm/solver/OptimizationDirection.h" #include "storm/logic/ComparisonType.h" +#include "storm/modelchecker/hints/ModelCheckerHint.h" namespace storm { namespace logic { @@ -32,7 +34,7 @@ namespace storm { /*! * Creates a task object with the default options for the given formula. */ - CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) { + CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula), hint(new ModelCheckerHint()) { this->onlyInitialStatesRelevant = onlyInitialStatesRelevant; this->produceSchedulers = false; this->qualitative = false; @@ -80,7 +82,7 @@ namespace storm { */ template CheckTask substituteFormula(NewFormulaType const& newFormula) const { - return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint); + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); } /*! @@ -191,34 +193,23 @@ namespace storm { } /*! - * sets a vector that may serve as a hint for the (quantitative) model-checking result + * sets a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ - void setResultHint(std::vector const& hint){ - this->resultHint = hint; + void setHint(ModelCheckerHint const& hint) { + this->hint = std::make_shared(hint); } - - /*! - * sets a vector that may serve as a hint for the (quantitative) model-checking result - */ - void setResultHint(std::vector&& hint){ - this->resultHint = hint; - } - - /*! - * Retrieves whether there is a vector that may serve as a hint for the (quantitative) model-checking result - */ - bool isResultHintSet() const { - return static_cast(resultHint); + void setHint(ModelCheckerHint&& hint){ + this->hint = std::make_shared(hint); } /*! - * Retrieves the vector that may serve as a hint for the (quantitative) model-checking result + * Retrieves a hint that might contain information that speeds up the modelchecking process (if supported by the model checker) */ - std::vector const& getResultVectorHint() const { - return resultHint.get(); + ModelCheckerHint const& getHint() const { + return *hint; } - boost::optional> const& getOptionalResultVectorHint() const{ - return resultHint; + ModelCheckerHint& getHint() { + return *hint; } private: @@ -236,7 +227,7 @@ namespace storm { * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve * a value will be produced if this flag is set. */ - CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers, boost::optional> const& resultHint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), resultHint(resultHint) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers, std::shared_ptr const& hint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), hint(hint) { // Intentionally left empty. } @@ -262,10 +253,8 @@ namespace storm { // if this flag is set. bool produceSchedulers; - // If supported by the model checker and the model formalism, this vector serves as initial guess for the - // solution. - boost::optional> resultHint; - // boost::optional schedulerHint; //TODO: will need two schedulers for games + // A hint that might contain information that speeds up the modelchecking process (if supported by the model checker) + std::shared_ptr hint; }; } diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp new file mode 100644 index 000000000..67d233fcd --- /dev/null +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp @@ -0,0 +1,81 @@ +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/adapters/CarlAdapter.h" +namespace storm { + namespace modelchecker { + + template + ExplicitModelCheckerHint::ExplicitModelCheckerHint(boost::optional> const& resultHint, boost::optional const& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint) { + // Intentionally left empty + } + + template + ExplicitModelCheckerHint::ExplicitModelCheckerHint(boost::optional>&& resultHint, boost::optional&& schedulerHint) : resultHint(resultHint), schedulerHint(schedulerHint) { + // Intentionally left empty + } + + template + bool ExplicitModelCheckerHint::isEmpty() const { + return !resultHint.is_initialized() && !schedulerHint.is_initialized(); + } + + template + bool ExplicitModelCheckerHint::isExplicitModelCheckerHint() const { + return true; + } + + template + bool ExplicitModelCheckerHint::hasResultHint() const { + return resultHint.is_initialized(); + } + + template + std::vector const& ExplicitModelCheckerHint::getResultHint() const { + return *resultHint; + } + + template + std::vector& ExplicitModelCheckerHint::getResultHint() { + return *resultHint; + } + + template + void ExplicitModelCheckerHint::setResultHint(boost::optional> const& resultHint) { + this->resultHint = resultHint; + } + + template + void ExplicitModelCheckerHint::setResultHint(boost::optional>&& resultHint) { + this->resultHint = resultHint; + } + + template + bool ExplicitModelCheckerHint::hasSchedulerHint() const { + return schedulerHint.is_initialized(); + } + + template + storm::storage::TotalScheduler const& ExplicitModelCheckerHint::getSchedulerHint() const { + return *schedulerHint; + } + + template + storm::storage::TotalScheduler& ExplicitModelCheckerHint::getSchedulerHint() { + return *schedulerHint; + } + + template + void ExplicitModelCheckerHint::setSchedulerHint(boost::optional const& schedulerHint) { + this->schedulerHint = schedulerHint; + } + + template + void ExplicitModelCheckerHint::setSchedulerHint(boost::optional&& schedulerHint) { + this->schedulerHint = schedulerHint; + } + + template class ExplicitModelCheckerHint; + template class ExplicitModelCheckerHint; + template class ExplicitModelCheckerHint; + + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h new file mode 100644 index 000000000..533c551f8 --- /dev/null +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.h @@ -0,0 +1,48 @@ +#ifndef STORM_MODELCHECKER_HINTS_EXPLICITMODELCHECKERHINT_H +#define STORM_MODELCHECKER_HINTS_EXPLICITMODELCHECKERHINT_H + +#include +#include + +#include "storm/modelchecker/hints/ModelCheckerHint.h" +#include "storm/storage/TotalScheduler.h" + +namespace storm { + namespace modelchecker { + + template + class ExplicitModelCheckerHint : public ModelCheckerHint { + public: + + ExplicitModelCheckerHint(ExplicitModelCheckerHint const& other) = default; + ExplicitModelCheckerHint(ExplicitModelCheckerHint&& other) = default; + ExplicitModelCheckerHint(boost::optional> const& resultHint = boost::none, boost::optional const& schedulerHint = boost::none); + ExplicitModelCheckerHint(boost::optional>&& resultHint, boost::optional&& schedulerHint = boost::none); + + // Returns true iff this hint does not contain any information + virtual bool isEmpty() const override; + + // Returns true iff this is an explicit model checker hint + virtual bool isExplicitModelCheckerHint() const override; + + bool hasResultHint() const; + std::vector const& getResultHint() const; + std::vector& getResultHint(); + void setResultHint(boost::optional> const& resultHint); + void setResultHint(boost::optional>&& resultHint); + + bool hasSchedulerHint() const; + storm::storage::TotalScheduler const& getSchedulerHint() const; + storm::storage::TotalScheduler& getSchedulerHint(); + void setSchedulerHint(boost::optional const& schedulerHint); + void setSchedulerHint(boost::optional&& schedulerHint); + + private: + boost::optional> resultHint; + boost::optional schedulerHint; + }; + + } +} + +#endif /* STORM_MODELCHECKER_HINTS_EXPLICITMODELCHECKERHINT_H */ diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.cpp b/src/storm/modelchecker/hints/ModelCheckerHint.cpp new file mode 100644 index 000000000..31f016857 --- /dev/null +++ b/src/storm/modelchecker/hints/ModelCheckerHint.cpp @@ -0,0 +1,34 @@ +#include "storm/modelchecker/hints/ModelCheckerHint.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/adapters/CarlAdapter.h" + +namespace storm { + namespace modelchecker { + + bool ModelCheckerHint::isEmpty() const { + return true; + } + + bool ModelCheckerHint::isExplicitModelCheckerHint() const { + return false; + } + + template + ExplicitModelCheckerHint const& ModelCheckerHint::asExplicitModelCheckerHint() const { + return dynamic_cast const&>(*this); + } + + template + ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint() { + return dynamic_cast&>(*this); + } + + template ExplicitModelCheckerHint const& ModelCheckerHint::asExplicitModelCheckerHint() const; + template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); + template ExplicitModelCheckerHint const& ModelCheckerHint::asExplicitModelCheckerHint() const; + template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); + template ExplicitModelCheckerHint const& ModelCheckerHint::asExplicitModelCheckerHint() const; + template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); + + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.h b/src/storm/modelchecker/hints/ModelCheckerHint.h new file mode 100644 index 000000000..4c3842c53 --- /dev/null +++ b/src/storm/modelchecker/hints/ModelCheckerHint.h @@ -0,0 +1,36 @@ +#ifndef STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H +#define STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H + +namespace storm { + namespace modelchecker { + + template + class ExplicitModelCheckerHint; + + + /* + * This class contains information that might accelerate the solving process + */ + class ModelCheckerHint { + public: + + ModelCheckerHint() = default; + + // Returns true iff this hint does not contain any information + virtual bool isEmpty() const; + + // Returns true iff this is an explicit model checker hint + virtual bool isExplicitModelCheckerHint() const; + + template + ExplicitModelCheckerHint& asExplicitModelCheckerHint(); + + template + ExplicitModelCheckerHint const& asExplicitModelCheckerHint() const; + + }; + + } +} + +#endif /* STORM_MODELCHECKER_HINTS_MODELCHECKERHINT_H */ diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp index e457919cb..4cd5a37d4 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" @@ -22,7 +23,7 @@ namespace storm { // Check if there are some optimizations implemented for the specified property if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) { - return checkWithResultHint(modelChecker); + return checkWithHint(modelChecker); } else { return modelChecker.check(*this->currentCheckTask); } @@ -30,18 +31,12 @@ namespace storm { template - std::unique_ptr SparseDtmcInstantiationModelChecker::checkWithResultHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelchecker) { - - // Insert the hint if it exists - if(resultOfLastCheck) { - this->currentCheckTask->setResultHint(std::move(*resultOfLastCheck)); - } - + std::unique_ptr SparseDtmcInstantiationModelChecker::checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelchecker) { // Check the formula and store the result as a hint for the next call. - // For qualitative properties, we still want a quantitative result hint. Hence we perform the subformula + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { std::unique_ptr result = modelchecker.check(*this->currentCheckTask); - resultOfLastCheck = result->template asExplicitQuantitativeCheckResult().getValueVector(); + this->currentCheckTask->setHint(ExplicitModelCheckerHint(result->template asExplicitQuantitativeCheckResult().getValueVector())); return result; } else { std::unique_ptr quantitativeResult; @@ -54,7 +49,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with result hint is only implemented for probability or reward operator formulas"); } std::unique_ptr qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - resultOfLastCheck = std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()); + this->currentCheckTask->setHint(ExplicitModelCheckerHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()))); return qualitativeResult; } } diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h index 2a88f39b3..4253ea65e 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h @@ -26,13 +26,9 @@ namespace storm { protected: // Considers the result of the last check as a hint for the current check - std::unique_ptr checkWithResultHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); - + std::unique_ptr checkWithHint(storm::modelchecker::SparseDtmcPrctlModelChecker>& modelChecker); storm::utility::ModelInstantiator> modelInstantiator; - - // Stores the result of the last check in order to use it as a hint for the next check. (If this is supported by the property) - boost::optional> resultOfLastCheck; }; } } diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp index 6dbaea1dd..acffc0360 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp @@ -2,6 +2,7 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" @@ -33,16 +34,15 @@ namespace storm { template std::unique_ptr SparseMdpInstantiationModelChecker::checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker>& modelchecker) { - // Insert the hint if it exists - if(resultOfLastCheck) { - this->currentCheckTask->setResultHint(std::move(*resultOfLastCheck)); - } + this->currentCheckTask->setProduceSchedulers(true); // Check the formula and store the result as a hint for the next call. - // For qualitative properties, we still want a quantitative result hint. Hence we perform the subformula + // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { std::unique_ptr result = modelchecker.check(*this->currentCheckTask); - resultOfLastCheck = result->template asExplicitQuantitativeCheckResult().getValueVector(); + storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); + this->currentCheckTask->setHint(ExplicitModelCheckerHint(result->template asExplicitQuantitativeCheckResult().getValueVector(), + dynamic_cast(scheduler))); return result; } else { std::unique_ptr quantitativeResult; @@ -52,10 +52,12 @@ namespace storm { } else if (this->currentCheckTask->getFormula().isRewardOperatorFormula()) { quantitativeResult = modelchecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with result hint is only implemented for probability or reward operator formulas"); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Checking with hint is only implemented for probability or reward operator formulas"); } std::unique_ptr qualitativeResult = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); - resultOfLastCheck = std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()); + storm::storage::Scheduler& scheduler = qualitativeResult->template asExplicitQuantitativeCheckResult().getScheduler(); + this->currentCheckTask->setHint(ExplicitModelCheckerHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector()), + std::move(dynamic_cast(scheduler)))); return qualitativeResult; } } diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h index 72e5120ba..ad3b97e67 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h @@ -29,10 +29,6 @@ namespace storm { std::unique_ptr checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker>& modelChecker); storm::utility::ModelInstantiator> modelInstantiator; - - - // Stores the result of the last check in order to use it as a hint for the next check. (If this is supported by the property) - boost::optional> resultOfLastCheck; }; } } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 5bbf6cf23..b94f22c92 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -69,7 +69,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getOptionalResultVectorHint()); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -103,7 +103,7 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getOptionalResultVectorHint()); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index d29c222f2..c8878d74c 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -86,7 +86,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getOptionalResultVectorHint()); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); @@ -144,7 +144,7 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory, checkTask.getOptionalResultVectorHint()); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index dc921aa68..7fff11150 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -9,6 +9,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -49,7 +50,7 @@ namespace storm { template - std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint) { + std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { // 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. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); @@ -84,8 +85,8 @@ namespace storm { // This is the initial guess for the iterative solvers. It should be safe as for all // 'maybe' states we know that the probability is strictly larger than 0. std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::convertNumber(0.5)); - if(resultHint){ - storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get()); + if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { + storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint().getResultHint()); } // Prepare the right-hand side of the equation system. For entry i this corresponds to @@ -161,12 +162,12 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint) { - return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory, resultHint); + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { + return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(numberOfRows, transitionMatrix, maybeStates); }, targetStates, qualitative, linearEquationSolverFactory, hint); } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const& maybeStates) { @@ -174,11 +175,11 @@ namespace storm { storm::utility::vector::selectVectorValues(result, maybeStates, totalStateRewardVector); return result; }, - targetStates, qualitative, linearEquationSolverFactory, resultHint); + targetStates, qualitative, linearEquationSolverFactory, hint); } template - std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates); @@ -209,8 +210,8 @@ namespace storm { // Initialize the x vector with the hint (if available) or with 1 for each element. // This is the initial guess for the iterative solvers. std::vector x(submatrix.getColumnCount(), storm::utility::one()); - if(resultHint){ - storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get()); + if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { + storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint().getResultHint()); } // Prepare the right-hand side of the equation system. diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index e6e2c59c4..2dfaac693 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -6,6 +6,7 @@ #include #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/BitVector.h" @@ -25,7 +26,7 @@ namespace storm { static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -34,9 +35,9 @@ namespace storm { static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -49,7 +50,7 @@ namespace storm { static std::vector computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); private: - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); struct BaierTransformedModel { BaierTransformedModel() : noTargetStates(false) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index fb9a562cf..1296676f2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1,6 +1,7 @@ #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -73,7 +74,7 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only."); // We need to identify the states which have to be taken out of the matrix, i.e. @@ -122,8 +123,8 @@ namespace storm { // Prepare the solution vector for the maybestates. Apply the hint, if given and applicable std::vector x(submatrix.getRowGroupCount()); - if(resultHint && (goal.minimize() || (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) { - storm::utility::vector::selectVectorValues(x, maybeStates, *resultHint); + if(!hint.isEmpty() && (goal.minimize() || (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) { + storm::utility::vector::selectVectorValues(x, maybeStates, hint.template asExplicitModelCheckerHint().getResultHint()); } MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeUntilProbabilitiesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(x)); @@ -180,9 +181,9 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { storm::solver::SolveGoal goal(dir); - return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, resultHint)); + return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, hint)); } template @@ -249,14 +250,14 @@ namespace storm { template template - std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); return computeReachabilityRewardsHelper(dir, transitionMatrix, backwardTransitions, [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); }, - targetStates, qualitative, minMaxLinearEquationSolverFactory, resultHint); + targetStates, qualitative, minMaxLinearEquationSolverFactory, hint); } #ifdef STORM_HAVE_CARL @@ -284,7 +285,7 @@ namespace storm { #endif template - std::vector SparseMdpPrctlHelper::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); @@ -337,14 +338,24 @@ namespace storm { } } - // Create vector for results for maybe states. If applicable, consider the given hint - std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::zero()); - if(resultHint && (dir == OptimizationDirection::Maximize || (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) { - storm::utility::vector::selectVectorValues(x, maybeStates, *resultHint); + // Create vector for results for maybe states and a solver object. + std::vector x; + std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); + + // If applicable, consider the given hint(s) + if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint() && + (hint.template asExplicitModelCheckerHint().hasSchedulerHint() || + dir == OptimizationDirection::Maximize || + (maybeStates & storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates)).empty())) { + x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); + } else { + x = std::vector(maybeStates.getNumberOfSetBits(), storm::utility::zero()); + } + if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint()) { + solver->setSchedulerHint(hint.template asExplicitModelCheckerHint().getSchedulerHint().getSchedulerForSubsystem(maybeStates)); } // Solve the corresponding system of equations. - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); solver->solveEquations(dir, x, b); // Set values of resulting vector according to result. @@ -658,13 +669,13 @@ namespace storm { template class SparseMdpPrctlHelper; template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint); + template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); #ifdef STORM_HAVE_CARL template class SparseMdpPrctlHelper; template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint); + template std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); #endif } } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index c352e6c0e..7210cd6c8 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -3,6 +3,7 @@ #include +#include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/MaximalEndComponent.h" #include "MDPModelCheckingHelperReturnType.h" @@ -36,11 +37,11 @@ namespace storm { static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static MDPSparseModelCheckingHelperReturnType computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, std::vector&& x = std::vector()); - static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false); @@ -51,7 +52,7 @@ namespace storm { static std::vector computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template - static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); #ifdef STORM_HAVE_CARL static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& intervalRewardModel, bool lowerBoundOfIntervals, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -62,7 +63,7 @@ namespace storm { static std::unique_ptr computeConditionalProbabilities(OptimizationDirection dir, storm::storage::sparse::state_type initialState, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: - static std::vector computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional> const& resultHint = boost::none); + static std::vector computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::function(uint_fast64_t, storm::storage::SparseMatrix const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 9e487550c..c2f84b652 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -175,6 +175,12 @@ namespace storm { return *scheduler.get(); } + template + storm::storage::Scheduler& ExplicitQuantitativeCheckResult::getScheduler() { + STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); + return *scheduler.get(); + } + template void print(std::ostream& out, ValueType const& value) { if (value == storm::utility::infinity()) { diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h index 9af78dbe8..bd0a2387f 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -64,6 +64,7 @@ namespace storm { bool hasScheduler() const; void setScheduler(std::unique_ptr&& scheduler); storm::storage::Scheduler const& getScheduler() const; + storm::storage::Scheduler& getScheduler(); private: // The values of the quantitative check result. diff --git a/src/storm/storage/TotalScheduler.cpp b/src/storm/storage/TotalScheduler.cpp index 57d641fa8..65904222d 100644 --- a/src/storm/storage/TotalScheduler.cpp +++ b/src/storm/storage/TotalScheduler.cpp @@ -1,6 +1,7 @@ #include "storm/storage/TotalScheduler.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/Hash.h" +#include "storm/utility/vector.h" namespace storm { namespace storage { @@ -43,6 +44,10 @@ namespace storm { return choices; } + TotalScheduler TotalScheduler::getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const { + return TotalScheduler(storm::utility::vector::filterVector(choices, subsystem)); + } + std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler) { out << "total scheduler (defined on " << scheduler.choices.size() << " states) [ "; for (uint_fast64_t state = 0; state < scheduler.choices.size() - 1; ++state) { diff --git a/src/storm/storage/TotalScheduler.h b/src/storm/storage/TotalScheduler.h index 67bd64b25..d70017b91 100644 --- a/src/storm/storage/TotalScheduler.h +++ b/src/storm/storage/TotalScheduler.h @@ -5,6 +5,7 @@ #include #include "storm/storage/Scheduler.h" +#include "storm/storage/BitVector.h" namespace storm { namespace storage { @@ -49,6 +50,13 @@ namespace storm { std::vector const& getChoices() const; + /*! + * Constructs the scheduler for the subsystem indicated by the given BitVector + * + * @param subsystem A BitVector whose i-th entry is true iff state i is part of the subsystem + */ + TotalScheduler getSchedulerForSubsystem(storm::storage::BitVector const& subsystem) const; + friend std::ostream& operator<<(std::ostream& out, TotalScheduler const& scheduler); friend struct std::hash;