From 3727018ef407b782f2dec2494a960e505dc1fe5f Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 15 Feb 2016 19:11:25 +0100 Subject: [PATCH] added functionality to sparse MDP helper to compute until probabilities just for maybe states (and produce the corresponding scheduler) Former-commit-id: 79aae02a133eca9339f581d01bcc386f19e0f7df --- .../prctl/SparseMdpPrctlModelChecker.cpp | 6 +++- .../prctl/helper/SparseMdpPrctlHelper.cpp | 34 +++++++++++++------ .../prctl/helper/SparseMdpPrctlHelper.h | 2 ++ src/solver/MinMaxLinearEquationSolver.cpp | 8 ++++- src/solver/MinMaxLinearEquationSolver.h | 7 ++-- .../GmmxxMdpPrctlModelCheckerTest.cpp | 26 +++++++++++--- 6 files changed, 63 insertions(+), 20 deletions(-) diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index b13906151..710d926a7 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -88,7 +88,11 @@ namespace storm { 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); - return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; } template diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index cb03e5724..adec586dd 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -120,19 +120,13 @@ namespace storm { // the accumulated probability of going from state i to some 'yes' state. std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); - // Create vector for results for maybe states. - std::vector x(maybeStates.getNumberOfSetBits()); - - // Solve the corresponding system of equations. - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); - solver->setTrackScheduler(produceScheduler); - solver->solveEquationSystem(x, b); + MDPSparseModelCheckingHelperReturnType resultForMaybeStates = computeUntilProbabilitiesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory); // Set values of resulting vector according to result. - storm::utility::vector::setVectorValues(result, maybeStates, x); - + storm::utility::vector::setVectorValues(result, maybeStates, resultForMaybeStates.values); + if (produceScheduler) { - storm::storage::Scheduler const& subscheduler = solver->getScheduler(); + storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler; uint_fast64_t currentSubState = 0; for (auto maybeState : maybeStates) { scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); @@ -158,6 +152,26 @@ namespace storm { return MDPSparseModelCheckingHelperReturnType(std::move(result), std::move(scheduler)); } + + template + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + // If requested, we will produce a scheduler. + std::unique_ptr scheduler; + + // Create vector for results for maybe states. + std::vector x(submatrix.getRowGroupCount()); + + // Solve the corresponding system of equations. + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix); + solver->setTrackScheduler(produceScheduler); + solver->solveEquationSystem(x, b); + + if (produceScheduler) { + scheduler = std::make_unique(std::move(solver->getScheduler())); + } + + return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + } 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::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index f09e40d4a..0b47759d7 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -37,6 +37,8 @@ namespace storm { static std::vector computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::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::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + static MDPSparseModelCheckingHelperReturnType computeUntilProbabilitiesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix const& submatrix, std::vector const& b, bool produceScheduler, storm::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); 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::utility::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp index 294b32c2a..5041469bc 100644 --- a/src/solver/MinMaxLinearEquationSolver.cpp +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -34,7 +34,13 @@ namespace storm { } template - storm::storage::Scheduler const& AbstractMinMaxLinearEquationSolver::getScheduler() const { + storm::storage::TotalScheduler const& AbstractMinMaxLinearEquationSolver::getScheduler() const { + STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); + return *scheduler.get(); + } + + template + storm::storage::TotalScheduler& AbstractMinMaxLinearEquationSolver::getScheduler() { STORM_LOG_THROW(scheduler, storm::exceptions::InvalidSettingsException, "Cannot retrieve scheduler, because none was generated."); return *scheduler.get(); } diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 78781c68a..71ea10ee2 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -10,7 +10,7 @@ #include "src/solver/AbstractEquationSolver.h" #include "src/solver/SolverSelectionOptions.h" #include "src/storage/sparse/StateType.h" -#include "src/storage/Scheduler.h" +#include "src/storage/TotalScheduler.h" #include "src/solver/OptimizationDirection.h" #include "src/exceptions/InvalidSettingsException.h" @@ -32,7 +32,8 @@ namespace storm { bool isTrackSchedulerSet() const; bool hasScheduler() const; - storm::storage::Scheduler const& getScheduler() const; + storm::storage::TotalScheduler const& getScheduler() const; + storm::storage::TotalScheduler& getScheduler(); void setOptimizationDirection(OptimizationDirection d); void resetOptimizationDirection(); @@ -59,7 +60,7 @@ namespace storm { bool trackScheduler; // The scheduler (if it could be successfully generated). - mutable boost::optional> scheduler; + mutable boost::optional> scheduler; }; /*! diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 14239a438..725e1376d 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -193,7 +193,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/scheduler_generation.nm"); - + // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; @@ -206,7 +206,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { std::shared_ptr> mdp = model->as>(); EXPECT_EQ(7ul, mdp->getNumberOfChoices()); - + auto solverFactory = std::make_unique>(storm::solver::EquationSolverTypeSelection::Gmmxx); solverFactory->setPreferredTechnique(storm::solver::MinMaxTechniqueSelection::PolicyIteration); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); @@ -218,9 +218,25 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { std::unique_ptr result = checker.check(checkTask); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0, scheduler.getChoice(0)); + EXPECT_EQ(1, scheduler.getChoice(1)); + EXPECT_EQ(0, scheduler.getChoice(2)); + EXPECT_EQ(0, scheduler.getChoice(3)); + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); - checkTask.replaceFormula(*formula); - - result = checker.check(checkTask); + checkTask = storm::modelchecker::CheckTask(*formula); + checkTask.setProduceSchedulers(true); + result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1, scheduler2.getChoice(0)); + EXPECT_EQ(2, scheduler2.getChoice(1)); + EXPECT_EQ(0, scheduler2.getChoice(2)); + EXPECT_EQ(0, scheduler2.getChoice(3)); }