From 843e6a9b6b82601c879fcd5bef7314cb54bc09ca Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 20 Aug 2020 23:15:49 -0700 Subject: [PATCH] step bounded properties for dtmcs in a new helper, and now with support for (extra) lower bounds --- ...eDeterministicStepBoundedHorizonHelper.cpp | 94 +++++++++++++++++++ ...rseDeterministicStepBoundedHorizonHelper.h | 25 +++++ .../prctl/SparseDtmcPrctlModelChecker.cpp | 8 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 39 +------- .../prctl/helper/SparseDtmcPrctlHelper.h | 2 - 5 files changed, 125 insertions(+), 43 deletions(-) create mode 100644 src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp create mode 100644 src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp new file mode 100644 index 000000000..311f0a943 --- /dev/null +++ b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp @@ -0,0 +1,94 @@ +#include "storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h" + +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/utility/macros.h" +#include "storm/utility/vector.h" +#include "storm/utility/graph.h" + +#include "storm/storage/expressions/Expression.h" +#include "storm/solver/Multiplier.h" +#include "storm/utility/SignalHandler.h" + +#include "storm/environment/solver/MinMaxSolverEnvironment.h" + + +namespace storm { + namespace modelchecker { + namespace helper { + + template + SparseDeterministicStepBoundedHorizonHelper::SparseDeterministicStepBoundedHorizonHelper() + { + // Intentionally left empty. + } + + template + std::vector SparseDeterministicStepBoundedHorizonHelper::compute(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const& hint) + { + std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); + + // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis. + storm::storage::BitVector maybeStates; + storm::storage::BitVector makeZeroColumns; + + + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + } else { + maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, upperBound); + if (lowerBound == 0) { + maybeStates &= ~psiStates; + } else { + makeZeroColumns = psiStates; + } + } + + STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0."); + if (lowerBound == 0) { + storm::utility::vector::setVectorValues(result, psiStates, + storm::utility::one()); + } + + if (!maybeStates.empty()) { + // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true, makeZeroColumns); + + // Create the vector of one-step probabilities to go to target states. + std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, psiStates); + + // Create the vector with which to multiply. + std::vector subresult(maybeStates.getNumberOfSetBits()); + + // Perform the matrix vector multiplication + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + if (lowerBound == 0) { + multiplier->repeatedMultiply(env, subresult, &b, upperBound); + } else { + multiplier->repeatedMultiply(env, subresult, &b, upperBound - lowerBound + 1); + submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); + multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + b = std::vector(b.size(), storm::utility::zero()); + multiplier->repeatedMultiply(env, subresult, &b, lowerBound - 1); + } + + + // Set the values of the resulting vector accordingly. + storm::utility::vector::setVectorValues(result, maybeStates, subresult); + } + + return result; + } + + + template class SparseDeterministicStepBoundedHorizonHelper; + template class SparseDeterministicStepBoundedHorizonHelper; + template class SparseDeterministicStepBoundedHorizonHelper; + } + } +}// +// Created by Sebastian Junges on 8/20/20. +// + diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h new file mode 100644 index 000000000..c1f1a5529 --- /dev/null +++ b/src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h @@ -0,0 +1,25 @@ +#pragma once + + +#include "storm/modelchecker/hints/ModelCheckerHint.h" +#include "storm/modelchecker/prctl/helper/SolutionType.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/solver.h" +#include "storm/solver/SolveGoal.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + template + class SparseDeterministicStepBoundedHorizonHelper { + public: + SparseDeterministicStepBoundedHorizonHelper(); + std::vector compute(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const& hint = ModelCheckerHint()); + private: + }; + + + } + } +} diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index a34431013..57262857b 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -1,4 +1,5 @@ #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h" #include #include @@ -70,15 +71,16 @@ namespace storm { auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeRewardBoundedValues(env, this->getModel(), formula); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } else { - STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper time bound, and no lower bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete lower time bound."); STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeStepBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), checkTask.getHint()); + storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper helper; + std::vector numericResult = helper.compute(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound(), checkTask.getHint()); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); - return result; + return result; } } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 97983ee54..683099542 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -43,44 +43,7 @@ namespace storm { namespace modelchecker { namespace helper { - template - std::vector SparseDtmcPrctlHelper::computeStepBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, ModelCheckerHint const& hint) { - std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); - - // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis. - storm::storage::BitVector maybeStates; - - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { - maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); - } else { - maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, stepBound); - maybeStates &= ~psiStates; - } - - STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0."); - - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); - - if (!maybeStates.empty()) { - // We can eliminate the rows and columns from the original transition probability matrix that have probability 0. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); - - // Create the vector of one-step probabilities to go to target states. - std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, psiStates); - - // Create the vector with which to multiply. - std::vector subresult(maybeStates.getNumberOfSetBits()); - - // Perform the matrix vector multiplication - auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); - multiplier->repeatedMultiply(env, subresult, &b, stepBound); - - // Set the values of the resulting vector accordingly. - storm::utility::vector::setVectorValues(result, maybeStates, subresult); - } - - return result; - } + template<> std::map SparseDtmcPrctlHelper::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula) { diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index f892f3a7d..17fb161de 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -28,8 +28,6 @@ namespace storm { class SparseDtmcPrctlHelper { public: - static std::vector computeStepBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, ModelCheckerHint const& hint = ModelCheckerHint()); - static std::map computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc const& model, std::shared_ptr rewardBoundedFormula); static std::vector computeNextProbabilities(Environment const& env, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates);