From 7cd7cd60a76ccddfcb9d243d776efe34c731cb2d Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 3 Jan 2018 13:29:12 +0100 Subject: [PATCH] Added new minmax settings: force computation of a priori bouds and tweak the qvi restart heuristic --- .../solver/MinMaxSolverEnvironment.cpp | 28 ++++++++++++++++++- .../solver/MinMaxSolverEnvironment.h | 10 ++++++- .../modules/MinMaxEquationSolverSettings.cpp | 20 +++++++++++++ .../modules/MinMaxEquationSolverSettings.h | 17 +++++++++++ .../solver/LpMinMaxLinearEquationSolver.cpp | 4 +++ .../SymbolicMinMaxLinearEquationSolver.cpp | 4 +++ 6 files changed, 81 insertions(+), 2 deletions(-) diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp index ed4b6145b..d44eac259 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp @@ -17,12 +17,14 @@ namespace storm { considerRelativeTerminationCriterion = minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Relative; STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion"); multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle(); + forceBounds = minMaxSettings.isForceBoundsSet(); + qviRestartThreshold = minMaxSettings.getQviRestartThreshold(); + qviRestartMaxIterations = minMaxSettings.getQviRestartMaxIterations(); } MinMaxSolverEnvironment::~MinMaxSolverEnvironment() { // Intentionally left empty } - storm::solver::MinMaxMethod const& MinMaxSolverEnvironment::getMethod() const { return minMaxMethod; @@ -69,6 +71,30 @@ namespace storm { multiplicationStyle = value; } + bool MinMaxSolverEnvironment::isForceBoundsSet() const { + return forceBounds; + } + + void MinMaxSolverEnvironment::setForceBounds(bool value) { + forceBounds = value; + } + + storm::RationalNumber MinMaxSolverEnvironment::getQviRestartThreshold() const { + return qviRestartThreshold; + } + + void MinMaxSolverEnvironment::setQviRestartThreshold(storm::RationalNumber value) { + qviRestartThreshold = value; + } + + uint64_t MinMaxSolverEnvironment::getQviRestartMaxIterations() const { + return qviRestartMaxIterations; + } + + void MinMaxSolverEnvironment::setQviRestartMaxIterations(uint64_t value) { + qviRestartMaxIterations = value; + } + } diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index 6cca14221..999ed18bd 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -25,6 +25,12 @@ namespace storm { void setRelativeTerminationCriterion(bool value); storm::solver::MultiplicationStyle const& getMultiplicationStyle() const; void setMultiplicationStyle(storm::solver::MultiplicationStyle value); + bool isForceBoundsSet() const; + void setForceBounds(bool value); + storm::RationalNumber getQviRestartThreshold() const; + void setQviRestartThreshold(storm::RationalNumber value); + uint64_t getQviRestartMaxIterations() const; + void setQviRestartMaxIterations(uint64_t value); private: storm::solver::MinMaxMethod minMaxMethod; @@ -33,7 +39,9 @@ namespace storm { storm::RationalNumber precision; bool considerRelativeTerminationCriterion; storm::solver::MultiplicationStyle multiplicationStyle; - + bool forceBounds; + storm::RationalNumber qviRestartThreshold; + uint64_t qviRestartMaxIterations; }; } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index 7141d0eb4..35145e829 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -19,6 +19,8 @@ namespace storm { const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute"; const std::string MinMaxEquationSolverSettings::lraMethodOptionName = "lramethod"; const std::string MinMaxEquationSolverSettings::valueIterationMultiplicationStyleOptionName = "vimult"; + const std::string MinMaxEquationSolverSettings::forceBoundsOptionName = "forcebounds"; + const std::string MinMaxEquationSolverSettings::quickValueIterationRestartOptionName = "qvirestart"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration"}; @@ -38,6 +40,12 @@ namespace storm { std::vector multiplicationStyles = {"gaussseidel", "regular", "gs", "r"}; this->addOption(storm::settings::OptionBuilder(moduleName, valueIterationMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for value iteration.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a multiplication style.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(multiplicationStyles)).setDefaultValueString("gaussseidel").build()).build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, forceBoundsOptionName, false, "If set, minmax solver always require that a priori bounds for the solution are computed.").build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, quickValueIterationRestartOptionName, false, "Controls when a restart of quick value iteration is triggered.") + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The minimal (relative) bound improvement that triggers a restart").addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorIncluding(0.0, 1.0)).setDefaultValueDouble(0.5).build()) + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxiters", "The maximal number of iterations within which a restart can be triggered.").setDefaultValueUnsignedInteger(300).build()).build()); } storm::solver::MinMaxMethod MinMaxEquationSolverSettings::getMinMaxEquationSolvingMethod() const { @@ -108,6 +116,18 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'."); } + bool MinMaxEquationSolverSettings::isForceBoundsSet() const { + return this->getOption(forceBoundsOptionName).getHasOptionBeenSet(); + } + + double MinMaxEquationSolverSettings::getQviRestartThreshold() const { + return this->getOption(quickValueIterationRestartOptionName).getArgumentByName("threshold").getValueAsDouble(); + } + + uint_fast64_t MinMaxEquationSolverSettings::getQviRestartMaxIterations() const { + return this->getOption(quickValueIterationRestartOptionName).getArgumentByName("maxiters").getValueAsUnsignedInteger(); + } + } } } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index bc9697476..eeb60be4e 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -97,6 +97,21 @@ namespace storm { */ storm::solver::MultiplicationStyle getValueIterationMultiplicationStyle() const; + /*! + * Retrieves whether the force bounds option has been set. + */ + bool isForceBoundsSet() const; + + /*! + * Retrieves the restart threshold for quick value iteration + */ + double getQviRestartThreshold() const; + + /*! + * Retrieves the maximal number of iterations within which a restart of quick value iteration can be triggered. + */ + uint_fast64_t getQviRestartMaxIterations() const; + // The name of the module. static const std::string moduleName; @@ -108,6 +123,8 @@ namespace storm { static const std::string absoluteOptionName; static const std::string lraMethodOptionName; static const std::string valueIterationMultiplicationStyleOptionName; + static const std::string forceBoundsOptionName; + static const std::string quickValueIterationRestartOptionName; }; } diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 80668c4fc..2067c7949 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -120,6 +120,10 @@ namespace storm { requirements.requireNoEndComponents(); } + if (env.solver().minMax().isForceBoundsSet()) { + requirements.requireBounds(); + } + return requirements; } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index b599face7..b9f8551c3 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -458,6 +458,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "The selected min max technique is not supported by this solver."); } + if (env.solver().minMax().isForceBoundsSet()) { + requirements.requireBounds(); + } + return requirements; }