From 7f56c82523ead89e64794e23617d52afef9ed6d1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Sep 2017 14:44:48 +0200 Subject: [PATCH] moved to providing solve goals in sparse model checkers and helpers --- .../MILPMinimalLabelSetGenerator.h | 2 + src/storm/modelchecker/CheckTask.h | 8 + .../csl/SparseCtmcCslModelChecker.cpp | 16 +- .../csl/helper/HybridCtmcCslHelper.cpp | 4 +- .../csl/helper/SparseCtmcCslHelper.cpp | 96 +++++----- .../csl/helper/SparseCtmcCslHelper.h | 27 +-- .../prctl/SparseDtmcPrctlModelChecker.cpp | 20 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 22 +-- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 4 +- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 61 ++++--- .../prctl/helper/SparseDtmcPrctlHelper.h | 28 +-- .../prctl/helper/SparseMdpPrctlHelper.cpp | 136 +++++++------- .../prctl/helper/SparseMdpPrctlHelper.h | 27 ++- src/storm/solver/AbstractEquationSolver.cpp | 20 ++ src/storm/solver/AbstractEquationSolver.h | 23 +++ .../IterativeMinMaxLinearEquationSolver.cpp | 40 +++- .../IterativeMinMaxLinearEquationSolver.h | 2 +- .../solver/NativeLinearEquationSolver.cpp | 6 +- src/storm/solver/SolveGoal.cpp | 126 ++++++++++--- src/storm/solver/SolveGoal.h | 172 ++++++++---------- src/storm/solver/SolverGuarantee.h | 4 + src/storm/solver/TerminationCondition.cpp | 8 +- src/storm/solver/TerminationCondition.h | 7 +- 23 files changed, 493 insertions(+), 366 deletions(-) diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index dff7a2808..a7d132e89 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -16,6 +16,8 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" + #include "storm/counterexamples/PrismHighLevelCounterexample.h" #include "storm/utility/graph.h" diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 828f85215..cc0de06c0 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -228,10 +228,18 @@ namespace storm { ModelCheckerHint const& getHint() const { return *hint; } + ModelCheckerHint& getHint() { return *hint; } + /*! + * Conversion operator that strips the type of the formula. + */ + operator CheckTask() const { + return this->substituteFormula(this->getFormula()); + } + private: /*! * Creates a task object with the given options. diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index facfd3da2..5443c27ee 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -72,7 +72,7 @@ namespace storm { upperBound = storm::utility::infinity(); } - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -92,7 +92,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::SparseCtmcCslHelper::computeUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeUntilProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -100,7 +100,7 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeInstantaneousRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -108,7 +108,7 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeCumulativeRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -118,7 +118,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -129,14 +129,14 @@ namespace storm { ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(probabilityMatrix, checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), &this->getModel().getExitRateVector(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal(this->getModel(), checkTask), probabilityMatrix, checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), &this->getModel().getExitRateVector(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -146,7 +146,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index cb046cfb1..59e5b2ea2 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -301,7 +301,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal(), explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } @@ -318,7 +318,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); std::vector explicitExitRateVector = exitRateVector.toVector(odd); - std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal(), explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index b59c13897..430b16224 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -28,13 +28,13 @@ namespace storm { namespace modelchecker { namespace helper { template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { uint_fast64_t numberOfStates = rateMatrix.getRowCount(); // If the time bounds are [0, inf], we rather call untimed reachability. if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { - return computeUntilProbabilities(rateMatrix, backwardTransitions, exitRates, phiStates, psiStates, qualitative, linearEquationSolverFactory); + return computeUntilProbabilities(std::move(goal), rateMatrix, backwardTransitions, exitRates, phiStates, psiStates, qualitative, linearEquationSolverFactory); } // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0 @@ -89,7 +89,7 @@ namespace storm { // Start by computing the (unbounded) reachability probabilities of reaching psi states while // staying in phi states. - result = computeUntilProbabilities(rateMatrix, backwardTransitions, exitRates, phiStates, psiStates, qualitative, linearEquationSolverFactory); + result = computeUntilProbabilities(storm::solver::SolveGoal(), rateMatrix, backwardTransitions, exitRates, phiStates, psiStates, qualitative, linearEquationSolverFactory); // Determine the set of states that must be considered further. storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates; @@ -195,13 +195,13 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector const&, bool, double, double, storm::solver::LinearEquationSolverFactory const&) { + std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, storm::storage::BitVector const&, storm::storage::BitVector const&, std::vector const&, bool, double, double, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); } template - std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseDtmcPrctlHelper::computeUntilProbabilities(computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); + std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseDtmcPrctlHelper::computeUntilProbabilities(std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector), backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolverFactory); } template @@ -210,7 +210,7 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -236,12 +236,12 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory const&) { + std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing instantaneous rewards is unsupported for this value type."); } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -272,12 +272,12 @@ namespace storm { } template ::SupportsExponential, int>::type> - std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory const&) { + std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const&, std::vector const&, RewardModelType const&, double, storm::solver::LinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing cumulative rewards is unsupported for this value type."); } template - std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -293,11 +293,11 @@ namespace storm { } } - return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); + return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(std::move(goal), probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); } template - std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -324,11 +324,11 @@ namespace storm { totalRewardVector = rewardModel.getStateActionRewardVector(); } - return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); + return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(std::move(goal), probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative, linearEquationSolverFactory); } template - std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); @@ -344,7 +344,7 @@ namespace storm { ValueType zero = storm::utility::zero(); ValueType one = storm::utility::one(); - return computeLongRunAverages(probabilityMatrix, + return computeLongRunAverages(std::move(goal), probabilityMatrix, [&zero, &one, &psiStates] (storm::storage::sparse::state_type const& state) -> ValueType { if (psiStates.get(state)) { return one; @@ -356,16 +356,16 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector), exitRateVector, linearEquationSolverFactory); + return computeLongRunAverageRewards(std::move(goal), probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector), exitRateVector, linearEquationSolverFactory); } template - std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return computeLongRunAverages(probabilityMatrix, + std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return computeLongRunAverages(std::move(goal), probabilityMatrix, [&stateRewardVector] (storm::storage::sparse::state_type const& state) -> ValueType { return stateRewardVector[state]; }, @@ -374,7 +374,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeLongRunAverages(storm::storage::SparseMatrix const& probabilityMatrix, std::function const& valueGetter, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory){ + std::vector SparseCtmcCslHelper::computeLongRunAverages(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::function const& valueGetter, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory){ uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); // Start by decomposing the CTMC into its BSCCs. @@ -723,58 +723,58 @@ namespace storm { } - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector const& exitRates); template std::vector SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const* addVector, double timeBound, double uniformizationRate, std::vector values, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); #ifdef STORM_HAVE_CARL - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); template storm::storage::SparseMatrix SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index 78787b748..cdfc5ca17 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -4,6 +4,7 @@ #include "storm/storage/BitVector.h" #include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/SolveGoal.h" #include "storm/utility/NumberTraits.h" @@ -15,43 +16,43 @@ namespace storm { class SparseCtmcCslHelper { public: template ::SupportsExponential, int>::type = 0> - static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeBoundedUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeUntilProbabilities(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeUntilProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template static std::vector computeNextProbabilities(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template ::SupportsExponential, int>::type = 0> - static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template - static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityTimes(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! * Computes the matrix representing the transitions of the uniformized CTMC. @@ -104,7 +105,7 @@ namespace storm { private: template - static std::vector computeLongRunAverages(storm::storage::SparseMatrix const& probabilityMatrix, std::function const& valueGetter, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverages(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::function const& valueGetter, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } } diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 9fde067e9..d05c86e1f 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -48,7 +48,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::computeBoundedUntilProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *linearEquationSolverFactory, checkTask.getHint()); std::unique_ptr result = std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); return result; } @@ -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.getHint()); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory, checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -78,7 +78,7 @@ namespace storm { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeGloballyProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -86,7 +86,7 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeCumulativeRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -94,7 +94,7 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeInstantaneousRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); 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.getHint()); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal(this->getModel(), checkTask), 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))); } @@ -112,13 +112,13 @@ namespace storm { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), nullptr, *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), nullptr, *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -134,7 +134,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -149,7 +149,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeConditionalRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); 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 6b9026ff0..256ddb2b7 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -16,7 +16,7 @@ #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" -#include "storm/solver/LpSolver.h" +#include "storm/solver/SolveGoal.h" #include "storm/settings/modules/GeneralSettings.h" @@ -64,7 +64,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::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeBoundedUntilProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -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.getHint()); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), 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)); @@ -100,7 +100,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(pathFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeGloballyProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret))); } @@ -117,7 +117,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(checkTask.getOptimizationDirection(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + return storm::modelchecker::helper::SparseMdpPrctlHelper::computeConditionalProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); } template @@ -125,7 +125,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeCumulativeRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -134,7 +134,7 @@ namespace storm { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeInstantaneousRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -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(); - auto ret = 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(), checkTask.isProduceSchedulersSet(), *minMaxLinearEquationSolverFactory, checkTask.getHint()); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.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)); @@ -158,19 +158,17 @@ 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(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { 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::vector result = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getUniqueRewardModel(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMdpPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getUniqueRewardModel(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - - template std::unique_ptr SparseMdpPrctlModelChecker::checkMultiObjectiveFormula(CheckTask const& checkTask) { return multiobjective::performMultiObjectiveModelChecking(this->getModel(), checkTask.getFormula()); diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 2a7e8672e..f4cca554f 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -265,7 +265,7 @@ namespace storm { storm::dd::Odd odd = model.getReachableStates().createOdd(); storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, targetStates.toVector(odd), linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal(), explicitProbabilityMatrix, targetStates.toVector(odd), linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } @@ -275,7 +275,7 @@ namespace storm { storm::dd::Odd odd = model.getReachableStates().createOdd(); storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal(), explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 305986555..6107e3acb 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -29,7 +29,7 @@ namespace storm { namespace modelchecker { namespace helper { template - std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint) { + std::vector SparseDtmcPrctlHelper::computeBoundedUntilProbabilities(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, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, 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. @@ -56,7 +56,8 @@ namespace storm { std::vector subresult(maybeStates.getNumberOfSetBits()); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + goal.restrictRelevantValues(maybeStates); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(std::move(goal), linearEquationSolverFactory, std::move(submatrix)); solver->repeatedMultiply(subresult, &b, stepBound); // Set the values of the resulting vector accordingly. @@ -68,7 +69,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, ModelCheckerHint const& hint) { + std::vector SparseDtmcPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal&& goal, 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) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); @@ -92,7 +93,6 @@ namespace storm { } } } else { - // Get all states that have probability 0 and 1 of satisfying the until-formula. std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); @@ -142,7 +142,8 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); // Now solve the created system of linear equations. - std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + goal.restrictRelevantValues(maybeStates); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(std::move(goal), linearEquationSolverFactory, std::move(submatrix)); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->solveEquations(x, b); @@ -154,8 +155,9 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - std::vector result = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative, linearEquationSolverFactory); + std::vector SparseDtmcPrctlHelper::computeGloballyProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + goal.oneMinus(); + std::vector result = computeUntilProbabilities(std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative, linearEquationSolverFactory); for (auto& entry : result) { entry = storm::utility::one() - entry; } @@ -175,7 +177,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Initialize result to the null vector. std::vector result(transitionMatrix.getRowCount()); @@ -183,14 +185,14 @@ namespace storm { std::vector totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(std::move(goal), linearEquationSolverFactory, transitionMatrix); solver->repeatedMultiply(result, &totalRewardVector, stepBound); return result; } template - std::vector SparseDtmcPrctlHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -198,21 +200,21 @@ namespace storm { std::vector result = rewardModel.getStateRewardVector(); // Perform the matrix vector multiplication as often as required by the formula bound. - std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(std::move(goal), linearEquationSolverFactory, transitionMatrix); solver->repeatedMultiply(result, nullptr, stepCount); return result; } 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, 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); + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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(std::move(goal), 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, ModelCheckerHint const& hint) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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, + return computeReachabilityRewards(std::move(goal), transitionMatrix, backwardTransitions, [&] (uint_fast64_t numberOfRows, storm::storage::SparseMatrix const&, storm::storage::BitVector const& maybeStates) { std::vector result(numberOfRows); storm::utility::vector::selectVectorValues(result, maybeStates, totalStateRewardVector); @@ -235,7 +237,7 @@ namespace storm { } 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, ModelCheckerHint const& hint) { + std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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) { std::vector result(transitionMatrix.getRowCount(), storm::utility::zero()); @@ -297,8 +299,9 @@ namespace storm { } STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver."); - // Create the solvers and provide - std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + // Create the solver. + goal.restrictRelevantValues(maybeStates); + std::unique_ptr> solver = storm::solver::configureLinearEquationSolver(std::move(goal), linearEquationSolverFactory, std::move(submatrix)); solver->setLowerBound(storm::utility::zero()); if (upperRewardBounds) { solver->setUpperBounds(std::move(upperRewardBounds.get())); @@ -315,18 +318,18 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, linearEquationSolverFactory); + std::vector SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageProbabilities(std::move(goal), transitionMatrix, psiStates, nullptr, linearEquationSolverFactory); } template - std::vector SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseCtmcCslHelper::computeLongRunAverageRewards(transitionMatrix, rewardModel, nullptr, linearEquationSolverFactory); + std::vector SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageRewards(std::move(goal), transitionMatrix, rewardModel, nullptr, linearEquationSolverFactory); } template - std::vector SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { - return SparseCtmcCslHelper::computeLongRunAverageRewards(transitionMatrix, stateRewards, nullptr, linearEquationSolverFactory); + std::vector SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageRewards(std::move(goal), transitionMatrix, stateRewards, nullptr, linearEquationSolverFactory); } template @@ -335,7 +338,7 @@ namespace storm { BaierTransformedModel result; // Start by computing all 'before' states, i.e. the states for which the conditional probability is defined. - std::vector probabilitiesToReachConditionStates = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory); + std::vector probabilitiesToReachConditionStates = computeUntilProbabilities(storm::solver::SolveGoal(), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), conditionStates, false, linearEquationSolverFactory); result.beforeStates = storm::storage::BitVector(targetStates.size(), true); uint_fast64_t state = 0; @@ -450,7 +453,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseDtmcPrctlHelper::computeConditionalProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Prepare result vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); @@ -467,7 +470,7 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - std::vector conditionalProbabilities = computeUntilProbabilities(newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + std::vector conditionalProbabilities = computeUntilProbabilities(std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), storm::storage::BitVector(newTransitionMatrix.getRowCount(), true), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalProbabilities); } @@ -477,7 +480,7 @@ namespace storm { } template - std::vector SparseDtmcPrctlHelper::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) { + std::vector SparseDtmcPrctlHelper::computeConditionalRewards(storm::solver::SolveGoal&& goal, 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) { // Prepare result vector. std::vector result(transitionMatrix.getRowCount(), storm::utility::infinity()); @@ -493,7 +496,7 @@ namespace storm { // Now compute reachability probabilities in the transformed model. storm::storage::SparseMatrix const& newTransitionMatrix = transformedModel.transitionMatrix.get(); - std::vector conditionalRewards = computeReachabilityRewards(newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); + std::vector conditionalRewards = computeReachabilityRewards(std::move(goal), newTransitionMatrix, newTransitionMatrix.transpose(), transformedModel.stateRewards.get(), transformedModel.targetStates.get(), qualitative, linearEquationSolverFactory); storm::utility::vector::setVectorValues(result, transformedModel.beforeStates, conditionalRewards); } } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 12f545d00..46cd0f05a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -12,6 +12,7 @@ #include "storm/storage/BitVector.h" #include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/SolveGoal.h" namespace storm { namespace modelchecker { @@ -22,35 +23,34 @@ namespace storm { template > class SparseDtmcPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeBoundedUntilProbabilities(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, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); 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, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeUntilProbabilities(storm::solver::SolveGoal&& goal, 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); + static std::vector computeGloballyProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeCumulativeRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeInstantaneousRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeInstantaneousRewards(storm::solver::SolveGoal&& goal, 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, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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); + static std::vector computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeConditionalProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - 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); + static std::vector computeConditionalRewards(storm::solver::SolveGoal&& goal, 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, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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 0b1aaf6f2..85713333a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -38,7 +38,7 @@ namespace storm { namespace helper { template - std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { + std::vector SparseMdpPrctlHelper::computeBoundedUntilProbabilities(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, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // Determine the states that have 0 probability of reaching the target states. @@ -46,7 +46,7 @@ namespace storm { if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { maybeStates = hint.template asExplicitModelCheckerHint().getMaybeStates(); } else { - if (dir == OptimizationDirection::Minimize) { + 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); @@ -63,8 +63,9 @@ namespace storm { // Create the vector with which to multiply. std::vector subresult(maybeStates.getNumberOfSetBits()); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(submatrix)); - solver->repeatedMultiply(dir, subresult, &b, stepBound); + goal.restrictRelevantValues(maybeStates); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); + solver->repeatedMultiply(subresult, &b, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); @@ -315,10 +316,13 @@ namespace storm { }; template - MaybeStateResult computeValuesForMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, SparseMdpHintType& hint) { + MaybeStateResult computeValuesForMaybeStates(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix&& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, SparseMdpHintType& hint) { + + // Initialize the solution vector. + std::vector x = hint.hasValueHint() ? std::move(hint.getValueHint()) : std::vector(submatrix.getRowGroupCount(), hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero()); // Set up the solver. - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); solver->setRequirementsChecked(); if (hint.hasLowerResultBound()) { solver->setLowerBound(hint.getLowerResultBound()); @@ -334,9 +338,6 @@ namespace storm { } solver->setTrackScheduler(produceScheduler); - // Initialize the solution vector. - std::vector x = hint.hasValueHint() ? std::move(hint.getValueHint()) : std::vector(submatrix.getRowGroupCount(), hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero()); - // Solve the corresponding system of equations. solver->solveEquations(x, b); @@ -390,7 +391,7 @@ namespace storm { } template - QualitativeStateSetsUntilProbabilities computeQualitativeStateSetsUntilProbabilities(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) { + QualitativeStateSetsUntilProbabilities computeQualitativeStateSetsUntilProbabilities(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) { QualitativeStateSetsUntilProbabilities result; // Get all states that have probability 0 and 1 of satisfying the until-formula. @@ -411,7 +412,7 @@ namespace storm { } template - QualitativeStateSetsUntilProbabilities getQualitativeStateSetsUntilProbabilities(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, ModelCheckerHint const& hint) { + QualitativeStateSetsUntilProbabilities getQualitativeStateSetsUntilProbabilities(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, ModelCheckerHint const& hint) { if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { return getQualitativeStateSetsUntilProbabilitiesFromHint(hint); } else { @@ -430,7 +431,7 @@ namespace storm { } template - void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for // the states with probability 1 or 0 (depending on whether we maximize or minimize). @@ -676,7 +677,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, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilities(storm::solver::SolveGoal&& 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."); // Prepare resulting vector. @@ -723,7 +724,8 @@ namespace storm { } // Now compute the results for the maybe states. - MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); + goal.restrictRelevantValues(qualitativeStateSets.maybeStates); + MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(std::move(goal), std::move(submatrix), b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); // If we eliminated end components, we need to extract the result differently. if (ecInformation && ecInformation.get().eliminatedEndComponents) { @@ -752,13 +754,7 @@ 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, ModelCheckerHint const& hint) { - storm::solver::SolveGoal goal(dir); - return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, produceScheduler, minMaxLinearEquationSolverFactory, hint)); - } - - template - std::vector SparseMdpPrctlHelper::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) { + std::vector SparseMdpPrctlHelper::computeGloballyProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique) { if (useMecBasedTechnique) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, psiStates); storm::storage::BitVector statesInPsiMecs(transitionMatrix.getRowGroupCount()); @@ -768,9 +764,10 @@ namespace storm { } } - return std::move(computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).values); + return std::move(computeUntilProbabilities(std::move(goal), transitionMatrix, backwardTransitions, psiStates, statesInPsiMecs, qualitative, false, minMaxLinearEquationSolverFactory).values); } else { - std::vector result = computeUntilProbabilities(dir == OptimizationDirection::Minimize ? OptimizationDirection::Maximize : OptimizationDirection::Minimize, transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values; + goal.oneMinus(); + std::vector result = computeUntilProbabilities(std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), ~psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values; for (auto& element : result) { element = storm::utility::one() - element; } @@ -780,7 +777,7 @@ namespace storm { template template - std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Only compute the result if the model has a state-based reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -788,15 +785,15 @@ namespace storm { // Initialize result to state rewards of the this->getModel(). std::vector result(rewardModel.getStateRewardVector()); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->repeatedMultiply(dir, result, nullptr, stepCount); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, transitionMatrix); + solver->repeatedMultiply(result, nullptr, stepCount); return result; } template template - std::vector SparseMdpPrctlHelper::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // 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."); @@ -807,30 +804,18 @@ namespace storm { // Initialize result to the zero vector. std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); - solver->repeatedMultiply(dir, result, &totalRewardVector, stepBound); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, transitionMatrix); + solver->repeatedMultiply(result, &totalRewardVector, stepBound); return result; } template template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, 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(storm::solver::SolveGoal(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, produceScheduler, minMaxLinearEquationSolverFactory, hint); - } - - template - template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, 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(goal, transitionMatrix, backwardTransitions, + return computeReachabilityRewardsHelper(std::move(goal), transitionMatrix, backwardTransitions, [&rewardModel] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { return rewardModel.getTotalRewardVector(rowCount, transitionMatrix, maybeStates); }, @@ -839,10 +824,10 @@ namespace storm { #ifdef STORM_HAVE_CARL template - std::vector SparseMdpPrctlHelper::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) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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) { // Only compute the result if the reward model is not empty. STORM_LOG_THROW(!intervalRewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - return computeReachabilityRewardsHelper(storm::solver::SolveGoal(dir), transitionMatrix, backwardTransitions, \ + return computeReachabilityRewardsHelper(std::move(goal), transitionMatrix, backwardTransitions, \ [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result; result.reserve(rowCount); @@ -856,7 +841,7 @@ namespace storm { } template<> - std::vector SparseMdpPrctlHelper::computeReachabilityRewards(OptimizationDirection, storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, storm::models::sparse::StandardRewardModel const&, bool, storm::storage::BitVector const&, bool, storm::solver::MinMaxLinearEquationSolverFactory const&) { + std::vector SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&&, storm::storage::SparseMatrix const&, storm::storage::SparseMatrix const&, storm::models::sparse::StandardRewardModel const&, bool, storm::storage::BitVector const&, bool, storm::solver::MinMaxLinearEquationSolverFactory const&) { STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Computing reachability rewards is unsupported for this data type."); } #endif @@ -875,7 +860,7 @@ namespace storm { } template - QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates) { + QualitativeStateSetsReachabilityRewards computeQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates) { QualitativeStateSetsReachabilityRewards result; storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); if (goal.minimize()) { @@ -892,7 +877,7 @@ namespace storm { } template - QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint) { + QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, ModelCheckerHint const& hint) { if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().getComputeOnlyMaybeStates()) { return getQualitativeStateSetsReachabilityRewardsFromHint(hint, targetStates); } else { @@ -901,7 +886,7 @@ namespace storm { } template - void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& targetStates) { + void extendScheduler(storm::storage::Scheduler& scheduler, storm::solver::SolveGoal const& goal, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& targetStates) { // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for // the states with reward infinity. Moreover, we have to set some arbitrary choice for the remaining states // to obtain a fully defined scheduler. @@ -1027,7 +1012,7 @@ namespace storm { } template - MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewardsHelper(storm::solver::SolveGoal&& goal, 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint) { // Prepare resulting vector. std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -1091,7 +1076,8 @@ namespace storm { } // Now compute the results for the maybe states. - MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); + goal.restrictRelevantValues(qualitativeStateSets.maybeStates); + MaybeStateResult resultForMaybeStates = computeValuesForMaybeStates(std::move(goal), std::move(submatrix), b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation); // If we eliminated end components, we need to extract the result differently. if (ecInformation && ecInformation.get().eliminatedEndComponents) { @@ -1119,7 +1105,7 @@ namespace storm { } template - std::vector SparseMdpPrctlHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // If there are no goal states, we avoid the computation and directly return zero. if (psiStates.empty()) { @@ -1136,12 +1122,12 @@ namespace storm { std::vector stateRewards(psiStates.size(), storm::utility::zero()); storm::utility::vector::setVectorValues(stateRewards, psiStates, storm::utility::one()); storm::models::sparse::StandardRewardModel rewardModel(std::move(stateRewards)); - return computeLongRunAverageRewards(dir, transitionMatrix, backwardTransitions, rewardModel, minMaxLinearEquationSolverFactory); + return computeLongRunAverageRewards(std::move(goal), transitionMatrix, backwardTransitions, rewardModel, minMaxLinearEquationSolverFactory); } template template - std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint64_t numberOfStates = transitionMatrix.getRowGroupCount(); @@ -1160,7 +1146,7 @@ namespace storm { for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; - lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(dir, transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory); + lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(goal.direction(), transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory); // Gather information for later use. for (auto const& stateChoicesPair : mec) { @@ -1270,9 +1256,10 @@ namespace storm { STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::vector sspResult(numberOfSspStates); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(std::move(sspMatrix)); + goal.restrictRelevantValues(statesNotContainedInAnyMec); + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, sspMatrix); solver->setRequirementsChecked(); - solver->solveEquations(dir, sspResult, b); + solver->solveEquations(sspResult, b); // Prepare result vector. std::vector result(numberOfStates, zero); @@ -1458,14 +1445,14 @@ namespace storm { } template - std::unique_ptr SparseMdpPrctlHelper::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) { + std::unique_ptr SparseMdpPrctlHelper::computeConditionalProbabilities(storm::solver::SolveGoal&& goal, 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) { std::chrono::high_resolution_clock::time_point start = std::chrono::high_resolution_clock::now(); // For the max-case, we can simply take the given target states. For the min-case, however, we need to // find the MECs of non-target states and make them the new target states. storm::storage::BitVector fixedTargetStates; - if (dir == OptimizationDirection::Maximize) { + if (!goal.minimize()) { fixedTargetStates = targetStates; } else { fixedTargetStates = storm::storage::BitVector(targetStates.size()); @@ -1484,8 +1471,9 @@ namespace storm { fixedTargetStates = storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, allStates, fixedTargetStates); // We solve the max-case and later adjust the result if the optimization direction was to minimize. - storm::storage::BitVector initialStatesBitVector(transitionMatrix.getRowGroupCount()); - initialStatesBitVector.set(initialState); + storm::storage::BitVector initialStatesBitVector = goal.relevantValues(); + STORM_LOG_THROW(initialStatesBitVector.getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Computing conditional probabilities in MDPs is only supported for models with exactly one initial state."); + storm::storage::sparse::state_type initialState = *initialStatesBitVector.begin(); // Extend the condition states by computing all states that have probability 1 to go to a condition state // under *all* schedulers. @@ -1589,8 +1577,14 @@ namespace storm { storm::storage::SparseMatrix newTransitionMatrix = builder.build(); STORM_LOG_DEBUG("Transformed model has " << newTransitionMatrix.getRowGroupCount() << " states and " << newTransitionMatrix.getNonzeroEntryCount() << " transitions."); storm::storage::SparseMatrix newBackwardTransitions = newTransitionMatrix.transpose(true); + + storm::solver::OptimizationDirection dir = goal.direction(); + if (goal.minimize()) { + goal.oneMinus(); + } + std::chrono::high_resolution_clock::time_point conditionalStart = std::chrono::high_resolution_clock::now(); - std::vector goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values); + std::vector goalProbabilities = std::move(computeUntilProbabilities(std::move(goal), newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).values); std::chrono::high_resolution_clock::time_point conditionalEnd = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Computed conditional probabilities in transformed model in " << std::chrono::duration_cast(conditionalEnd - conditionalStart).count() << "ms."); @@ -1598,22 +1592,20 @@ 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 MDPSparseModelCheckingHelperReturnType 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); - template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); - template std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, 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(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); + template std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template double SparseMdpPrctlHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template double SparseMdpPrctlHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template double SparseMdpPrctlHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); #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 MDPSparseModelCheckingHelperReturnType 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); - template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); - template std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(storm::solver::SolveGoal&& goal, 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(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint); + template std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponentVI(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 5cf2bcfaf..6160f318b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -33,42 +33,37 @@ namespace storm { template class SparseMdpPrctlHelper { public: - static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeBoundedUntilProbabilities(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, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); 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, ModelCheckerHint const& hint = ModelCheckerHint()); - - 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 MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(storm::solver::SolveGoal&& 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); + static std::vector computeGloballyProbabilities(storm::solver::SolveGoal&& goal, 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); template - static std::vector computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeInstantaneousRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template - static std::vector computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeCumulativeRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template - static MDPSparseModelCheckingHelperReturnType computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + static MDPSparseModelCheckingHelperReturnType computeReachabilityRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); - template - static MDPSparseModelCheckingHelperReturnType computeReachabilityRewards(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, 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); + static std::vector computeReachabilityRewards(storm::solver::SolveGoal&& goal, 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); #endif - static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageProbabilities(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template - static std::vector computeLongRunAverageRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeLongRunAverageRewards(storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - 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); + static std::unique_ptr computeConditionalProbabilities(storm::solver::SolveGoal&& goal, 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 MDPSparseModelCheckingHelperReturnType computeReachabilityRewardsHelper(storm::solver::SolveGoal const& goal, 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); + static MDPSparseModelCheckingHelperReturnType computeReachabilityRewardsHelper(storm::solver::SolveGoal&& goal, 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, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint()); template static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/storm/solver/AbstractEquationSolver.cpp b/src/storm/solver/AbstractEquationSolver.cpp index e80b0a101..788a8d789 100644 --- a/src/storm/solver/AbstractEquationSolver.cpp +++ b/src/storm/solver/AbstractEquationSolver.cpp @@ -38,6 +38,26 @@ namespace storm { return this->getTerminationCondition().terminateNow(values, guarantee); } + template + bool AbstractEquationSolver::hasRelevantValues() const { + return static_cast(relevantValues); + } + + template + storm::storage::BitVector const& AbstractEquationSolver::getRelevantValues()const { + return relevantValues.get(); + } + + template + void AbstractEquationSolver::setRelevantValues(storm::storage::BitVector&& relevantValues) { + this->relevantValues = std::move(relevantValues); + } + + template + void AbstractEquationSolver::clearRelevantValues() { + relevantValues = boost::none; + } + template bool AbstractEquationSolver::hasLowerBound(BoundType const& type) const { if (type == BoundType::Any) { diff --git a/src/storm/solver/AbstractEquationSolver.h b/src/storm/solver/AbstractEquationSolver.h index 6a55c34e1..72776d522 100644 --- a/src/storm/solver/AbstractEquationSolver.h +++ b/src/storm/solver/AbstractEquationSolver.h @@ -37,6 +37,26 @@ namespace storm { */ bool terminateNow(std::vector const& values, SolverGuarantee const& guarantee) const; + /*! + * Retrieves whether this solver has particularly relevant values. + */ + bool hasRelevantValues() const; + + /*! + * Retrieves the relevant values (if there are any). + */ + storm::storage::BitVector const& getRelevantValues() const; + + /*! + * Sets the relevant values. + */ + void setRelevantValues(storm::storage::BitVector&& valuesOfInterest); + + /*! + * Removes the values of interest (if there were any). + */ + void clearRelevantValues(); + enum class BoundType { Global, Local, @@ -122,6 +142,9 @@ namespace storm { // A termination condition to be used (can be unset). std::unique_ptr> terminationCondition; + // A bit vector containing the indices of the relevant values if they were set. + boost::optional relevantValues; + // A lower bound if one was set. boost::optional lowerBound; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 2fb2c5d57..78d7f033b 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -140,7 +140,7 @@ namespace storm { std::vector scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : std::vector(this->A->getRowGroupCount()); // Get a vector for storing the right-hand side of the inner equation system. - if(!auxiliaryRowGroupVector) { + if (!auxiliaryRowGroupVector) { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } std::vector& subB = *auxiliaryRowGroupVector; @@ -210,7 +210,7 @@ namespace storm { // Update environment variables. ++iterations; - status = updateStatusIfNotConverged(status, x, iterations); + status = updateStatusIfNotConverged(status, x, iterations, dir == storm::OptimizationDirection::Minimize ? SolverGuarantee::GreaterOrEqual : SolverGuarantee::LessOrEqual); } while (status == Status::InProgress); reportStatus(status, iterations); @@ -294,6 +294,10 @@ namespace storm { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } + // By default, the guarantee that we can provide is that our solution is always less-or-equal than the + // actual solution. + SolverGuarantee guarantee = SolverGuarantee::LessOrEqual; + if (this->hasInitialScheduler()) { // Resolve the nondeterminism according to the initial scheduler. bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem; @@ -313,6 +317,12 @@ namespace storm { submatrixSolver->setUpperBound(this->upperBound.get()); } submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector); + + // If we were given an initial scheduler and are in fact minimizing, our current solution becomes + // always greater-or-equal than the actual solution. + if (dir == storm::OptimizationDirection::Minimize) { + guarantee = SolverGuarantee::GreaterOrEqual; + } } // Allow aliased multiplications. @@ -343,7 +353,7 @@ namespace storm { // Update environment variables. std::swap(currentX, newX); ++iterations; - status = updateStatusIfNotConverged(status, *currentX, iterations); + status = updateStatusIfNotConverged(status, *currentX, iterations, guarantee); } reportStatus(status, iterations); @@ -404,8 +414,14 @@ namespace storm { precision *= storm::utility::convertNumber(2.0); } while (status == Status::InProgress && iterations < this->getSettings().getMaximalNumberOfIterations()) { + // Remember in which directions we took steps in this iteration. + bool lowerStep = false; + bool upperStep = false; + // In every thousandth iteration, we improve both bounds. if (iterations % 1000 == 0 || lowerDiff == upperDiff) { + lowerStep = true; + upperStep = true; if (useGaussSeidelMultiplication) { lowerDiff = (*lowerX)[0]; this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *lowerX, &b); @@ -428,20 +444,24 @@ namespace storm { lowerDiff = (*lowerX)[0]; this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *lowerX, &b); lowerDiff = (*lowerX)[0] - lowerDiff; + lowerStep = true; } else { upperDiff = (*upperX)[0]; this->linEqSolverA->multiplyAndReduceGaussSeidel(dir, this->A->getRowGroupIndices(), *upperX, &b); upperDiff = upperDiff - (*upperX)[0]; + upperStep = true; } } else { if (lowerDiff >= upperDiff) { this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), *lowerX, &b, *tmp); lowerDiff = (*tmp)[0] - (*lowerX)[0]; std::swap(tmp, lowerX); + lowerStep = true; } else { this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), *upperX, &b, *tmp); upperDiff = (*upperX)[0] - (*tmp)[0]; std::swap(tmp, upperX); + upperStep = true; } } } @@ -458,10 +478,12 @@ namespace storm { // Update environment variables. ++iterations; - } - - if (status != Status::Converged) { - status = Status::MaximalIterationsExceeded; + if (lowerStep) { + status = updateStatusIfNotConverged(status, *lowerX, iterations, SolverGuarantee::LessOrEqual); + } + if (upperStep) { + status = updateStatusIfNotConverged(status, *upperX, iterations, SolverGuarantee::GreaterOrEqual); + } } reportStatus(status, iterations); @@ -597,9 +619,9 @@ namespace storm { } template - typename IterativeMinMaxLinearEquationSolver::Status IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const { + typename IterativeMinMaxLinearEquationSolver::Status IterativeMinMaxLinearEquationSolver::updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const { if (status != Status::Converged) { - if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)) { + if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x, guarantee)) { status = Status::TerminatedEarly; } else if (iterations >= this->getSettings().getMaximalNumberOfIterations()) { status = Status::MaximalIterationsExceeded; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index b2b10ef29..fb7fee8f0 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -79,7 +79,7 @@ namespace storm { mutable std::unique_ptr> auxiliaryRowGroupVector2; // A.rowGroupCount() entries mutable std::unique_ptr> rowGroupOrdering; // A.rowGroupCount() entries - Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations) const; + Status updateStatusIfNotConverged(Status status, std::vector const& x, uint64_t iterations, SolverGuarantee const& guarantee) const; void reportStatus(Status status, uint64_t iterations) const; /// The settings of this solver. diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index b59eb5c2f..7d46584d7 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -392,7 +392,7 @@ namespace storm { bool useGaussSeidelMultiplication = this->getSettings().getPowerMethodMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel; bool converged = false; - bool terminate = this->terminateNow(*currentX, SolverGuarantee::GreaterOrEqual); + bool terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual); uint64_t iterations = 0; while (!converged && !terminate && iterations < this->getSettings().getMaximalNumberOfIterations()) { if (useGaussSeidelMultiplication) { @@ -404,7 +404,7 @@ namespace storm { // Now check for termination. converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, static_cast(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()); - terminate = this->terminateNow(*currentX, SolverGuarantee::GreaterOrEqual); + terminate = this->terminateNow(*currentX, SolverGuarantee::LessOrEqual); // Set up next iteration. std::swap(currentX, nextX); @@ -516,7 +516,7 @@ namespace storm { // the original precision. converged = storm::utility::vector::equalModuloPrecision(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()); if (lowerStep) { - terminate |= this->terminateNow(*lowerX, SolverGuarantee::GreaterOrEqual); + terminate |= this->terminateNow(*lowerX, SolverGuarantee::LessOrEqual); } if (upperStep) { terminate |= this->terminateNow(*upperX, SolverGuarantee::GreaterOrEqual); diff --git a/src/storm/solver/SolveGoal.cpp b/src/storm/solver/SolveGoal.cpp index 20c54a9b3..cd331b2fe 100644 --- a/src/storm/solver/SolveGoal.cpp +++ b/src/storm/solver/SolveGoal.cpp @@ -1,7 +1,12 @@ -#include "SolveGoal.h" +#include "storm/solver/SolveGoal.h" #include +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" + +#include "storm/modelchecker/CheckTask.h" + #include "storm/utility/solver.h" #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" @@ -14,46 +19,109 @@ namespace storm { namespace solver { template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - std::unique_ptr> p = factory.create(matrix); - p->setOptimizationDirection(goal.direction()); - p->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); - return p; + SolveGoal::SolveGoal() { + // Intentionally left empty. + } + + template + SolveGoal::SolveGoal(bool minimize) : optimizationDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) { + // Intentionally left empty. } - template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - if (goal.isBounded()) { - return configureMinMaxLinearEquationSolver(static_cast const&>(goal), factory, matrix); - } - std::unique_ptr> solver = factory.create(matrix); - solver->setOptimizationDirection(goal.direction()); - return solver; + template + SolveGoal::SolveGoal(OptimizationDirection optimizationDirection) : optimizationDirection(optimizationDirection) { + // Intentionally left empty. } template - std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - std::unique_ptr> solver = factory.create(matrix); - solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.thresholdValue(), goal.boundIsStrict(), goal.minimize())); - return solver; + SolveGoal::SolveGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType boundComparisonType, ValueType const& boundThreshold, storm::storage::BitVector const& relevantValues) : optimizationDirection(optimizationDirection), comparisonType(boundComparisonType), threshold(boundThreshold), relevantValueVector(relevantValues) { + // Intentionally left empty. } template - std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix) { - if (goal.isBounded()) { - return configureLinearEquationSolver(static_cast const&>(goal), factory, matrix); + bool SolveGoal::hasDirection() const { + return static_cast(optimizationDirection); + } + + template + void SolveGoal::oneMinus() { + if (optimizationDirection) { + if (optimizationDirection == storm::solver::OptimizationDirection::Minimize) { + optimizationDirection = storm::solver::OptimizationDirection::Maximize; + } else { + optimizationDirection = storm::solver::OptimizationDirection::Minimize; + } + } + if (threshold) { + this->threshold = storm::utility::one() - this->threshold.get(); + } + if (comparisonType) { + switch (comparisonType.get()) { + case storm::logic::ComparisonType::Less: comparisonType = storm::logic::ComparisonType::GreaterEqual; break; + case storm::logic::ComparisonType::LessEqual: comparisonType = storm::logic::ComparisonType::Greater; break; + case storm::logic::ComparisonType::Greater: comparisonType = storm::logic::ComparisonType::LessEqual; break; + case storm::logic::ComparisonType::GreaterEqual: comparisonType = storm::logic::ComparisonType::Less; break; + } } - return factory.create(matrix); } - - template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + + template + bool SolveGoal::minimize() const { + return optimizationDirection == OptimizationDirection::Minimize; + } + + template + OptimizationDirection SolveGoal::direction() const { + return optimizationDirection.get(); + } + + template + bool SolveGoal::isBounded() const { + return comparisonType && threshold && relevantValueVector; + } + + template + bool SolveGoal::boundIsALowerBound() const { + return (comparisonType.get() == storm::logic::ComparisonType::Greater || comparisonType.get() == storm::logic::ComparisonType::GreaterEqual); + } + + template + bool SolveGoal::boundIsStrict() const { + return (comparisonType.get() == storm::logic::ComparisonType::Greater || comparisonType.get() == storm::logic::ComparisonType::Less); + } + + template + ValueType const& SolveGoal::thresholdValue() const { + return threshold.get(); + } + + template + bool SolveGoal::hasRelevantValues() const { + return static_cast(relevantValueVector); + } + + template + storm::storage::BitVector const& SolveGoal::relevantValues() const { + return relevantValueVector.get(); + } + template + storm::storage::BitVector& SolveGoal::relevantValues() { + return relevantValueVector.get(); + } + + template + void SolveGoal::restrictRelevantValues(storm::storage::BitVector const& filter) { + if (relevantValueVector) { + relevantValueVector = relevantValueVector.get() % filter; + } + } + + template class SolveGoal; + #ifdef STORM_HAVE_CARL - template std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - template std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template class SolveGoal; + template class SolveGoal; #endif } } diff --git a/src/storm/solver/SolveGoal.h b/src/storm/solver/SolveGoal.h index 4a84898f2..c6f95151d 100644 --- a/src/storm/solver/SolveGoal.h +++ b/src/storm/solver/SolveGoal.h @@ -1,11 +1,11 @@ -#ifndef STORM_SOLVER_SOLVEGOAL_H_ -#define STORM_SOLVER_SOLVEGOAL_H_ +#pragma once #include +#include + #include "storm/solver/OptimizationDirection.h" #include "storm/logic/ComparisonType.h" -#include "storm/logic/Bound.h" #include "storm/storage/BitVector.h" #include "storm/solver/LinearEquationSolver.h" @@ -16,10 +16,17 @@ namespace storm { template class SparseMatrix; } - namespace utility { - namespace solver { - template class MinMaxLinearEquationSolverFactory; - template class LinearEquationSolverFactory; + namespace solver { + template class MinMaxLinearEquationSolverFactory; + template class LinearEquationSolverFactory; + } + + namespace modelchecker { + template class CheckTask; + } + namespace models { + namespace sparse { + template class Model; } } @@ -27,108 +34,89 @@ namespace storm { template class MinMaxLinearEquationSolver; template class LinearEquationSolver; + template class SolveGoal { public: - SolveGoal(bool minimize) : optimizationDirection(minimize ? OptimizationDirection::Minimize : OptimizationDirection::Maximize) { - // Intentionally left empty. + SolveGoal(); + + template + SolveGoal(storm::models::sparse::Model const& model, storm::modelchecker::CheckTask const& checkTask) { + if (checkTask.isOptimizationDirectionSet()) { + optimizationDirection = checkTask.getOptimizationDirection(); + } + if (checkTask.isOnlyInitialStatesRelevantSet()) { + relevantValueVector = model.getInitialStates(); + } + if (checkTask.isBoundSet()) { + comparisonType = checkTask.getBoundComparisonType(); + threshold = checkTask.getBoundThreshold(); + } } - SolveGoal(OptimizationDirection d) : optimizationDirection(d) { - // Intentionally left empty. - } + SolveGoal(bool minimize); + SolveGoal(OptimizationDirection d); + SolveGoal(OptimizationDirection d, storm::logic::ComparisonType boundComparisonType, ValueType const& boundThreshold, storm::storage::BitVector const& relevantValues); - virtual ~SolveGoal() { - // Intentionally left empty. - } - - bool minimize() const { - return optimizationDirection == OptimizationDirection::Minimize; - } + /*! + * Flips the comparison type, the direction, and computes the new threshold as 1 - old threshold. + */ + void oneMinus(); - OptimizationDirection direction() const { - return optimizationDirection; - } + bool hasDirection() const; + + bool minimize() const; - virtual bool isBounded() const { - return false; - } - - private: - OptimizationDirection optimizationDirection; - }; - - template - class BoundedGoal : public SolveGoal { - public: - BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType boundComparisonType, ValueType const& boundThreshold, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), comparisonType(boundComparisonType), threshold(boundThreshold), relevantValueVector(relevantValues) { - // Intentionally left empty. - } + OptimizationDirection direction() const; - virtual ~BoundedGoal() { - // Intentionally left empty. - } + bool isBounded() const; - bool isBounded() const override { - return true; - } + bool boundIsALowerBound() const; - bool boundIsALowerBound() const { - return (comparisonType == storm::logic::ComparisonType::Greater || comparisonType == storm::logic::ComparisonType::GreaterEqual); - } + bool boundIsStrict() const; - bool boundIsStrict() const { - return (comparisonType == storm::logic::ComparisonType::Greater || comparisonType == storm::logic::ComparisonType::Less); - } + ValueType const& thresholdValue() const; - ValueType const& thresholdValue() const { - return threshold; - } - - bool achieved(std::vector const& result) const { - for (auto const& i : relevantValueVector) { - switch(comparisonType) { - case storm::logic::ComparisonType::Greater: - if( result[i] <= threshold) return false; - break; - case storm::logic::ComparisonType::GreaterEqual: - if( result[i] < threshold) return false; - break; - case storm::logic::ComparisonType::Less: - if( result[i] >= threshold) return false; - break; - case storm::logic::ComparisonType::LessEqual: - if( result[i] > threshold) return false; - break; - } - } - return true; - } - - storm::storage::BitVector const& relevantValues() const { - return relevantValueVector; - } + bool hasRelevantValues() const; + + storm::storage::BitVector& relevantValues(); + storm::storage::BitVector const& relevantValues() const; + + void restrictRelevantValues(storm::storage::BitVector const& filter); private: - storm::logic::ComparisonType comparisonType; - ValueType threshold; - storm::storage::BitVector relevantValueVector; + boost::optional optimizationDirection; + + boost::optional comparisonType; + boost::optional threshold; + boost::optional relevantValueVector; }; - template - std::unique_ptr> configureMinMaxLinearEquationSolver(BoundedGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template + std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal&& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, MatrixType&& matrix) { + std::unique_ptr> solver = factory.create(std::forward(matrix)); + solver->setOptimizationDirection(goal.direction()); + if (goal.isBounded()) { + solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); + } else if (goal.hasRelevantValues()) { + solver->setRelevantValues(std::move(goal.relevantValues())); + } + return solver; + } - template - std::unique_ptr> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - - template - std::unique_ptr> configureLinearEquationSolver(BoundedGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); + template + std::unique_ptr> configureLinearEquationSolver(SolveGoal&& goal, storm::solver::LinearEquationSolverFactory const& factory, MatrixType&& matrix) { + std::unique_ptr> solver = factory.create(std::forward(matrix)); + if (goal.isBounded()) { + solver->setTerminationCondition(std::make_unique>(goal.relevantValues(), goal.boundIsStrict(), goal.thresholdValue(), goal.minimize())); + } + return solver; + } + + template + std::unique_ptr> configureLinearEquationSolver(SolveGoal&& goal, storm::solver::LinearEquationSolverFactory const& factory, MatrixType&& matrix) { + std::unique_ptr> solver = factory.create(std::forward(matrix)); + return solver; + } - template - std::unique_ptr> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory const& factory, storm::storage::SparseMatrix const& matrix); - } } - - -#endif /* STORM_SOLVER_SOLVEGOAL_H_ */ - diff --git a/src/storm/solver/SolverGuarantee.h b/src/storm/solver/SolverGuarantee.h index aecf92add..432482d88 100644 --- a/src/storm/solver/SolverGuarantee.h +++ b/src/storm/solver/SolverGuarantee.h @@ -5,6 +5,10 @@ namespace storm { namespace solver { + // The guarantees a solver can provide. + // GreaterOrEqual means that the provided solution is greater or equal than the actual solution. + // LessOrEqual means that the provided solution is less or equal than the actual solution. + // None means that the solver cannot provide any guarantees. enum class SolverGuarantee { GreaterOrEqual, LessOrEqual, None }; diff --git a/src/storm/solver/TerminationCondition.cpp b/src/storm/solver/TerminationCondition.cpp index 0352c77e7..fbacfbe56 100644 --- a/src/storm/solver/TerminationCondition.cpp +++ b/src/storm/solver/TerminationCondition.cpp @@ -20,7 +20,7 @@ namespace storm { template bool TerminateIfFilteredSumExceedsThreshold::terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee) const { - if (guarantee != SolverGuarantee::GreaterOrEqual) { + if (guarantee != SolverGuarantee::LessOrEqual) { return false; } @@ -36,7 +36,7 @@ namespace storm { template bool TerminateIfFilteredExtremumExceedsThreshold::terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee) const { - if (guarantee != SolverGuarantee::GreaterOrEqual) { + if (guarantee != SolverGuarantee::LessOrEqual) { return false; } @@ -52,7 +52,7 @@ namespace storm { template bool TerminateIfFilteredExtremumBelowThreshold::terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee) const { - if (guarantee != SolverGuarantee::LessOrEqual) { + if (guarantee != SolverGuarantee::GreaterOrEqual) { return false; } @@ -68,7 +68,7 @@ namespace storm { template class TerminateIfFilteredSumExceedsThreshold; template class TerminateIfFilteredExtremumExceedsThreshold; template class TerminateIfFilteredExtremumBelowThreshold; - #endif + } } diff --git a/src/storm/solver/TerminationCondition.h b/src/storm/solver/TerminationCondition.h index 3e9be9b40..529618443 100644 --- a/src/storm/solver/TerminationCondition.h +++ b/src/storm/solver/TerminationCondition.h @@ -11,13 +11,16 @@ namespace storm { template class TerminationCondition { public: + /*! + * Retrieves whether the guarantee provided by the solver for the current result is sufficient to terminate. + */ virtual bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const = 0; }; template class NoTerminationCondition : public TerminationCondition { public: - bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const; + virtual bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const override; }; template @@ -26,7 +29,7 @@ namespace storm { TerminateIfFilteredSumExceedsThreshold(storm::storage::BitVector const& filter, ValueType const& threshold, bool strict); bool terminateNow(std::vector const& currentValues, SolverGuarantee const& guarantee = SolverGuarantee::None) const; - + protected: ValueType threshold; storm::storage::BitVector filter;