From 569b0122b84b2d1d8b011048227368964dd15c68 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 30 Aug 2017 21:30:02 +0200 Subject: [PATCH] introduced different minmax equation system types for requirement retrieval --- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 6 +++--- .../modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp | 8 ++------ .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 10 +++++----- .../modelchecker/prctl/helper/SparseMdpPrctlHelper.h | 2 +- src/storm/solver/MinMaxLinearEquationSolver.cpp | 6 +++--- src/storm/solver/MinMaxLinearEquationSolver.h | 10 ++++++++-- 6 files changed, 22 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index a7d28ecac..ecf2b6759 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -89,7 +89,7 @@ namespace storm { } // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic); @@ -376,7 +376,7 @@ namespace storm { std::vector x(numberOfSspStates); // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); @@ -584,7 +584,7 @@ namespace storm { std::vector b = probabilisticChoiceRewards; // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic)); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 6a6a15dd7..b94b8ad9c 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -79,7 +79,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Check for requirements of the solver. - std::vector requirements = linearEquationSolverFactory.getRequirements(); + std::vector requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); @@ -147,10 +147,6 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - // Check for requirements of the solver. - std::vector requirements = linearEquationSolverFactory.getRequirements(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); - std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->repeatedMultiply(dir, x, &explicitRepresentation.second, stepBound); @@ -278,7 +274,7 @@ namespace storm { std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Check for requirements of the solver. - std::vector requirements = linearEquationSolverFactory.getRequirements(); + std::vector requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); // Now solve the resulting equation system. diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 1e6cfb882..c901d29d3 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -159,7 +159,7 @@ namespace storm { std::pair>, boost::optional>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, boost::none, hint, skipEcWithinMaybeStatesCheck); // Now compute the results for the maybeStates - std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero(), storm::utility::one()); + std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero(), storm::utility::one(), storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.first); @@ -252,10 +252,10 @@ namespace storm { } template - std::pair, boost::optional>> SparseMdpPrctlHelper::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues, boost::optional>&& hintChoices, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { + std::pair, boost::optional>> SparseMdpPrctlHelper::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues, boost::optional>&& hintChoices, boost::optional const& lowerResultBound, boost::optional const& upperResultBound, storm::solver::MinMaxLinearEquationSolverSystemType const& equationSystemType) { // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(equationSystemType); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); // Set up the solver @@ -460,7 +460,7 @@ namespace storm { std::pair>, boost::optional>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck); // Now compute the results for the maybeStates - std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero()); + std::pair, boost::optional>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero(), boost::none, storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards); // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.first); @@ -658,7 +658,7 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); // Check for requirements of the solver. - std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(); + std::vector requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); std::vector sspResult(numberOfSspStates); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index e82c89cc2..3727601d1 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -41,7 +41,7 @@ namespace storm { static std::pair>, boost::optional>> extractHintInformationForMaybeStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck); - static std::pair, boost::optional>> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues = boost::none, boost::optional>&& hintChoices = boost::none, boost::optional const& lowerResultBound = boost::none, boost::optional const& upperResultBound = boost::none); + static std::pair, boost::optional>> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory, boost::optional>&& hintValues = boost::none, boost::optional>&& hintChoices = boost::none, boost::optional const& lowerResultBound = boost::none, boost::optional const& upperResultBound = boost::none, storm::solver::MinMaxLinearEquationSolverSystemType const& equationSystemType = storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities); 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()); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 011249ec6..4c2321de0 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -138,7 +138,7 @@ namespace storm { } template - std::vector MinMaxLinearEquationSolver::getRequirements() const { + std::vector MinMaxLinearEquationSolver::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const { return std::vector(); } @@ -210,10 +210,10 @@ namespace storm { } template - std::vector MinMaxLinearEquationSolverFactory::getRequirements() const { + std::vector MinMaxLinearEquationSolverFactory::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const { // Create dummy solver and ask it for requirements. std::unique_ptr> solver = this->create(); - return solver->getRequirements(); + return solver->getRequirements(equationSystemType); } template diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 992bd2cc5..626be302d 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -23,6 +23,12 @@ namespace storm { namespace solver { + enum class MinMaxLinearEquationSolverSystemType { + UntilProbabilities, + ReachabilityRewards, + StochasticShortestPath + }; + enum class MinMaxLinearEquationSolverRequirement { ValidSchedulerHint, ValidValueHint, @@ -170,7 +176,7 @@ namespace storm { /*! * Retrieves the requirements of this solver for solving equations with the current settings. */ - virtual std::vector getRequirements() const; + virtual std::vector getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -229,7 +235,7 @@ namespace storm { MinMaxMethod const& getMinMaxMethod() const; - std::vector getRequirements() const; + std::vector getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const;