From 6e3639c8f1e66cab4f299320005e133304710693 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 2 Dec 2018 17:48:56 +0100 Subject: [PATCH] Added new minmax method: Vi-to-Pi, which first performs value iteration with doubles, to find a good initial policy for (potentially exact) policy iteration. --- .../modules/MinMaxEquationSolverSettings.cpp | 4 +- .../TopologicalEquationSolverSettings.cpp | 7 ++- .../IterativeMinMaxLinearEquationSolver.cpp | 47 +++++++++++++++++-- .../IterativeMinMaxLinearEquationSolver.h | 2 + .../solver/MinMaxLinearEquationSolver.cpp | 4 +- src/storm/solver/SolverSelectionOptions.cpp | 2 + src/storm/solver/SolverSelectionOptions.h | 2 +- .../modelchecker/MdpPrctlModelCheckerTest.cpp | 16 +++++++ 8 files changed, 72 insertions(+), 12 deletions(-) diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index 0a2943efd..d953bfc7a 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -23,7 +23,7 @@ namespace storm { const std::string MinMaxEquationSolverSettings::intervalIterationSymmetricUpdatesOptionName = "symmetricupdates"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration", "topological"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration", "topological", "vi-to-pi"}; this->addOption(storm::settings::OptionBuilder(moduleName, solvingMethodOptionName, false, "Sets which min/max linear equation solving technique is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a min/max linear equation solving technique.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("topological").build()).build()); @@ -64,6 +64,8 @@ namespace storm { return storm::solver::MinMaxMethod::SoundValueIteration; } else if (minMaxEquationSolvingTechnique == "topological") { return storm::solver::MinMaxMethod::Topological; + } else if (minMaxEquationSolvingTechnique == "vi-to-pi") { + return storm::solver::MinMaxMethod::ViToPi; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); diff --git a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp index 88a0c48fd..6445a871e 100644 --- a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp +++ b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp @@ -29,7 +29,7 @@ namespace storm { std::vector linearEquationSolver = {"gmm++", "native", "eigen", "elimination"}; this->addOption(storm::settings::OptionBuilder(moduleName, underlyingEquationSolverOptionName, true, "Sets which solver is considered for solving the underlying equation systems.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build()); - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "lp", "linear-programming", "rs", "ratsearch", "ii", "interval-iteration", "svi", "sound-value-iteration", "vi-to-pi"}; this->addOption(storm::settings::OptionBuilder(moduleName, underlyingMinMaxMethodOptionName, true, "Sets which minmax method is considered for solving the underlying minmax equation systems.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the used min max method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(minMaxSolvingTechniques)).setDefaultValueString("value-iteration").build()).build()); } @@ -78,10 +78,9 @@ namespace storm { return storm::solver::MinMaxMethod::IntervalIteration; } else if (minMaxEquationSolvingTechnique == "sound-value-iteration" || minMaxEquationSolvingTechnique == "svi") { return storm::solver::MinMaxMethod::SoundValueIteration; + } else if (minMaxEquationSolvingTechnique == "vi-to-pi") { + return storm::solver::MinMaxMethod::ViToPi; } - - - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 51289fb52..becaa1d17 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -42,12 +42,12 @@ namespace storm { // Adjust the method if none was specified and we want exact or sound computations. auto method = env.solver().minMax().getMethod(); - if (isExactMode && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch) { + if (isExactMode && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch && method != MinMaxMethod::ViToPi) { if (env.solver().minMax().isMethodSetFromDefault()) { STORM_LOG_INFO("Selecting 'Policy iteration' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a different method."); method = MinMaxMethod::PolicyIteration; } else { - STORM_LOG_WARN("The selected solution method does not guarantee exact results."); + STORM_LOG_WARN("The selected solution method " << toString(method) << " does not guarantee exact results."); } } else if (env.solver().isForceSoundness() && method != MinMaxMethod::SoundValueIteration && method != MinMaxMethod::IntervalIteration && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch) { if (env.solver().minMax().isMethodSetFromDefault()) { @@ -57,7 +57,7 @@ namespace storm { STORM_LOG_WARN("The selected solution method does not guarantee sound results."); } } - STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::IntervalIteration, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method."); + STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::ViToPi, storm::exceptions::InvalidEnvironmentException, "This solver does not support the selected method."); return method; } @@ -80,6 +80,9 @@ namespace storm { case MinMaxMethod::SoundValueIteration: result = solveEquationsSoundValueIteration(env, dir, x, b); break; + case MinMaxMethod::ViToPi: + result = solveEquationsViToPi(env, dir, x, b); + break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "This solver does not implement the selected solution method"); } @@ -117,7 +120,12 @@ namespace storm { bool IterativeMinMaxLinearEquationSolver::solveEquationsPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { // Create the initial scheduler. std::vector scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : std::vector(this->A->getRowGroupCount()); - + return performPolicyIteration(env, dir, x, b, std::move(scheduler)); + } + + template + bool IterativeMinMaxLinearEquationSolver::performPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector&& initialPolicy) const { + std::vector scheduler = std::move(initialPolicy); // Get a vector for storing the right-hand side of the inner equation system. if (!auxiliaryRowGroupVector) { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); @@ -226,6 +234,7 @@ namespace storm { bool needsLinEqSolver = false; needsLinEqSolver |= method == MinMaxMethod::PolicyIteration; needsLinEqSolver |= method == MinMaxMethod::ValueIteration && (this->hasInitialScheduler() || hasInitialScheduler); + needsLinEqSolver |= method == MinMaxMethod::ViToPi; MinMaxLinearEquationSolverRequirements requirements = needsLinEqSolver ? MinMaxLinearEquationSolverRequirements(this->linearEquationSolverFactory->getRequirements(env)) : MinMaxLinearEquationSolverRequirements(); if (method == MinMaxMethod::ValueIteration) { @@ -265,6 +274,12 @@ namespace storm { requirements.requireNoEndComponents(); } requirements.requireBounds(false); + } else if (method == MinMaxMethod::ViToPi) { + // Since we want to use value iteration to extract an initial scheduler, it helps to eliminate all end components first. + // TODO: We might get around this, as the initial value iteration scheduler is only a heuristic. + if (!this->hasUniqueSolution()) { + requirements.requireNoEndComponents(); + } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "Unsupported technique for iterative MinMax linear equation solver."); } @@ -666,6 +681,30 @@ namespace storm { return status == SolverStatus::Converged; } + template + bool IterativeMinMaxLinearEquationSolver::solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { + // First create an (inprecise) vi solver to get a good initial strategy for the (potentially precise) policy iteration solver. + std::vector initialSched; + { + Environment viEnv = env; + viEnv.solver().minMax().setMethod(MinMaxMethod::ValueIteration); + auto impreciseSolver = GeneralMinMaxLinearEquationSolverFactory().create(viEnv, this->A->template toValueType()); + impreciseSolver->setHasUniqueSolution(this->hasUniqueSolution()); + impreciseSolver->setTrackScheduler(true); + if (this->hasInitialScheduler()) { + auto initSched = this->getInitialScheduler(); + impreciseSolver->setInitialScheduler(std::move(initSched)); + } + STORM_LOG_THROW(!impreciseSolver->getRequirements(viEnv, dir).hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "The value-iteration based solver has an unmet requirement."); + auto xVi = storm::utility::vector::convertNumericVector(x); + auto bVi = storm::utility::vector::convertNumericVector(b); + impreciseSolver->solveEquations(viEnv, dir, xVi, bVi); + initialSched = impreciseSolver->getSchedulerChoices(); + } + STORM_LOG_INFO("Found initial policy using Value Iteration. Starting Policy iteration now."); + return performPolicyIteration(env, dir, x, b, std::move(initialSched)); + } + template bool IterativeMinMaxLinearEquationSolver::isSolution(storm::OptimizationDirection dir, storm::storage::SparseMatrix const& matrix, std::vector const& values, std::vector const& b) { storm::utility::ConstantsComparator comparator; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 33da6e68e..4166a47aa 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -36,11 +36,13 @@ namespace storm { bool solveInducedEquationSystem(Environment const& env, std::unique_ptr>& linearEquationSolver, std::vector const& scheduler, std::vector& x, std::vector& subB, std::vector const& originalB) const; bool solveEquationsPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool performPolicyIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b, std::vector&& initialPolicy) const; bool valueImproved(OptimizationDirection dir, ValueType const& value1, ValueType const& value2) const; bool solveEquationsValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsIntervalIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsSoundValueIteration(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; + bool solveEquationsViToPi(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsRationalSearch(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index e9b5a0fdd..be724ea0d 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -192,7 +192,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create(Environment const& env) const { std::unique_ptr> result; auto method = env.solver().minMax().getMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::ViToPi) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(); @@ -211,7 +211,7 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::create(Environment const& env) const { std::unique_ptr> result; auto method = env.solver().minMax().getMethod(); - if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) { + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration || method == MinMaxMethod::ViToPi) { result = std::make_unique>(std::make_unique>()); } else if (method == MinMaxMethod::LinearProgramming) { result = std::make_unique>(std::make_unique>()); diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index d50d4875f..0a457be7e 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -20,6 +20,8 @@ namespace storm { return "soundvalueiteration"; case MinMaxMethod::TopologicalCuda: return "topologicalcuda"; + case MinMaxMethod::ViToPi: + return "vi-to-pi"; } return "invalid"; } diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index baea29dc1..448878b72 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -6,7 +6,7 @@ namespace storm { namespace solver { - ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, TopologicalCuda) + ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, TopologicalCuda, ViToPi) ExtendEnumsWithSelectionField(MultiplierType, Native, Gmmxx) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration) diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index 6ef58edb5..939cf4275 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -157,6 +157,21 @@ namespace { return env; } }; + + class SparseRationalViToPiEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const MdpEngine engine = MdpEngine::PrismSparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::Mdp ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ViToPi); + return env; + } + }; + class SparseRationalRationalSearchEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models @@ -406,6 +421,7 @@ namespace { SparseDoubleTopologicalValueIterationEnvironment, SparseDoubleTopologicalSoundValueIterationEnvironment, SparseRationalPolicyIterationEnvironment, + SparseRationalViToPiEnvironment, SparseRationalRationalSearchEnvironment, HybridCuddDoubleValueIterationEnvironment, HybridSylvanDoubleValueIterationEnvironment,