diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp new file mode 100644 index 000000000..68d7631d0 --- /dev/null +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -0,0 +1,86 @@ +#include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h" +#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.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 + SparseNondeterministicStepBoundedHorizonHelper::SparseNondeterministicStepBoundedHorizonHelper(/*storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions*/) + //transitionMatrix(transitionMatrix), backwardTransitions(backwardTransitions) + { + // Intentionally left empty. + } + + template + std::vector SparseNondeterministicStepBoundedHorizonHelper::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.getRowGroupCount(), storm::utility::zero()); + storm::storage::BitVector makeZeroColumns; + + + // Determine the states that have 0 probability of reaching the target states. + storm::storage::BitVector maybeStates; + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { + maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); + } else { + if (goal.minimize()) { + maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, upperBound); + } else { + maybeStates = storm::utility::graph::performProbGreater0E(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 (!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, false, makeZeroColumns); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates); + + // Create the vector with which to multiply. + std::vector subresult(maybeStates.getNumberOfSetBits()); + + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + if (lowerBound == 0) { + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound); + } else { + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, upperBound - lowerBound + 1); + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + b = std::vector(b.size(), storm::utility::zero()); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, lowerBound - 1); + } + // Set the values of the resulting vector accordingly. + storm::utility::vector::setVectorValues(result, maybeStates, subresult); + } + if (lowerBound == 0) { + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + } + return result; + } + + + template class SparseNondeterministicStepBoundedHorizonHelper; + template class SparseNondeterministicStepBoundedHorizonHelper; + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h new file mode 100644 index 000000000..98fc49c2c --- /dev/null +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.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 SparseNondeterministicStepBoundedHorizonHelper { + public: + SparseNondeterministicStepBoundedHorizonHelper(); + 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 57262857b..831c3ac96 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -71,8 +71,9 @@ 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.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."); + STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); + STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper step bound."); std::unique_ptr leftResultPointer = this->check(env, pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(env, pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index d67de2603..709ffe605 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -16,6 +16,7 @@ #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h" @@ -83,13 +84,15 @@ namespace storm { auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeRewardBoundedValues(env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates()); 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.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound."); + STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral."); 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::SparseMdpPrctlHelper::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::SparseNondeterministicStepBoundedHorizonHelper 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()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 5282f9e60..c29035367 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -52,45 +52,7 @@ namespace storm { namespace modelchecker { namespace helper { - template - std::vector SparseMdpPrctlHelper::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.getRowGroupCount(), storm::utility::zero()); - - // Determine the states that have 0 probability of reaching the target states. - storm::storage::BitVector maybeStates; - if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { - maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); - } else { - if (goal.minimize()) { - maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); - } else { - maybeStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates, true, stepBound); - } - maybeStates &= ~psiStates; - } - - STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0."); - - 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, false); - std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates); - - // Create the vector with which to multiply. - std::vector subresult(maybeStates.getNumberOfSetBits()); - - auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); - multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound); - - // Set the values of the resulting vector accordingly. - storm::utility::vector::setVectorValues(result, maybeStates, subresult); - } - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); - - return result; - } - - + template std::map SparseMdpPrctlHelper::computeRewardBoundedValues(Environment const& env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates) { storm::utility::Stopwatch swAll(true), swBuild, swCheck; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 57cb1ad4d..64d9b03a1 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -38,8 +38,6 @@ namespace storm { template class SparseMdpPrctlHelper { 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, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding& rewardUnfolding, storm::storage::BitVector const& initialStates);