From 6a5f64c9fd30f3d8584ef6175e19f11a3a8d54dd Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 13 Mar 2016 18:24:26 +0100 Subject: [PATCH] resultHint for dtmc model checker Former-commit-id: 52a3cc37de6d482c3a3971031cb88a68080acd43 --- src/modelchecker/CheckTask.h | 40 ++++++++++++++++--- .../prctl/SparseDtmcPrctlModelChecker.cpp | 6 +-- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 29 +++++++++----- .../prctl/helper/SparseDtmcPrctlHelper.h | 10 +++-- 4 files changed, 62 insertions(+), 23 deletions(-) diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index 63b9561c0..73e96cb9b 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -80,7 +80,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); + return CheckTask(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint); } /*! @@ -183,6 +183,37 @@ namespace storm { return produceSchedulers; } + /*! + * sets a vector that may serve as a hint for the (quantitative) model-checking result + */ + void setResultHint(std::vector const& hint){ + this->resultHint = 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); + } + + /*! + * Retrieves the vector that may serve as a hint for the (quantitative) model-checking result + */ + std::vector const& getResultVectorHint() const { + return resultHint.get(); + } + boost::optional> const& getOptionalResultVectorHint() const{ + return resultHint; + } + private: /*! * Creates a task object with the given options. @@ -198,7 +229,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) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) { + 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) { // Intentionally left empty. } @@ -226,9 +257,8 @@ namespace storm { // If supported by the model checker and the model formalism, this vector serves as initial guess for the // solution. - boost::optional> resultVectorHint; - // If supported by the model checker, this - // boost::optional schedulerHint; + boost::optional> resultHint; + // boost::optional schedulerHint; //TODO: will need two schedulers for games }; } diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index d110f067d..15ac70e91 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -68,7 +68,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); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getOptionalResultVectorHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -102,7 +102,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); + 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()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -147,4 +147,4 @@ namespace storm { template class SparseDtmcPrctlModelChecker>; } -} \ No newline at end of file +} diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 9e1b6ef14..b71d15197 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -48,7 +48,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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint) { // 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); @@ -79,10 +79,14 @@ namespace storm { // system. That is, we go from x = A*x + b to (I-A)x = b. submatrix.convertToEquationSystem(); - // Initialize the x vector with 0.5 for each element. 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. + + // Initialize the x vector with the hint (if available) or with 0.5 for each element. + // 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(), ValueType(0.5)); + if(resultHint){ + storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get()); + } // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. @@ -156,23 +160,23 @@ 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - 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); + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> 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); } 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint) { return computeReachabilityRewards(transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result(numberOfRows); storm::utility::vector::selectVectorValues(result, maybeStates, totalStateRewardVector); return result; }, - targetStates, qualitative, linearEquationSolverFactory); + targetStates, qualitative, linearEquationSolverFactory, resultHint); } 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint) { // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); @@ -201,9 +205,12 @@ namespace storm { // system. That is, we go from x = A*x + b to (I-A)x = b. submatrix.convertToEquationSystem(); - // Initialize the x vector with 1 for each element. This is the initial guess for - // the iterative solvers. + // 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()); + } // Prepare the right-hand side of the equation system. std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 637c30cb5..8ec0cfc8a 100644 --- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -3,6 +3,8 @@ #include +#include + #include "src/models/sparse/StandardRewardModel.h" #include "src/storage/SparseMatrix.h" @@ -23,7 +25,7 @@ namespace storm { static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::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::utility::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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none); static std::vector computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -31,9 +33,9 @@ namespace storm { static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::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::utility::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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none); static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -42,7 +44,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::utility::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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + 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::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none); struct BaierTransformedModel { storm::storage::BitVector beforeStates;