From 5f831d156f6b35753b110bedfaec4df90216cd30 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 Jan 2018 18:01:41 +0100 Subject: [PATCH] forceBounds option for native solver --- .../environment/solver/NativeSolverEnvironment.cpp | 10 ++++++++++ src/storm/environment/solver/NativeSolverEnvironment.h | 3 +++ .../settings/modules/NativeEquationSolverSettings.cpp | 8 ++++++++ .../settings/modules/NativeEquationSolverSettings.h | 7 +++++++ src/storm/solver/NativeLinearEquationSolver.cpp | 4 ++++ 5 files changed, 32 insertions(+) diff --git a/src/storm/environment/solver/NativeSolverEnvironment.cpp b/src/storm/environment/solver/NativeSolverEnvironment.cpp index 3a3d0cb08..b11b906df 100644 --- a/src/storm/environment/solver/NativeSolverEnvironment.cpp +++ b/src/storm/environment/solver/NativeSolverEnvironment.cpp @@ -18,6 +18,7 @@ namespace storm { STORM_LOG_ASSERT(considerRelativeTerminationCriterion || nativeSettings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion"); powerMethodMultiplicationStyle = nativeSettings.getPowerMethodMultiplicationStyle(); sorOmega = storm::utility::convertNumber(nativeSettings.getOmega()); + forceBounds = nativeSettings.isForceBoundsSet(); } NativeSolverEnvironment::~NativeSolverEnvironment() { @@ -77,4 +78,13 @@ namespace storm { sorOmega = value; } + bool NativeSolverEnvironment::isForceBoundsSet() const { + return forceBounds; + } + + void NativeSolverEnvironment::setForceBounds(bool value) { + forceBounds = value; + } + + } diff --git a/src/storm/environment/solver/NativeSolverEnvironment.h b/src/storm/environment/solver/NativeSolverEnvironment.h index 51b96f613..675b553b0 100644 --- a/src/storm/environment/solver/NativeSolverEnvironment.h +++ b/src/storm/environment/solver/NativeSolverEnvironment.h @@ -27,6 +27,8 @@ namespace storm { void setPowerMethodMultiplicationStyle(storm::solver::MultiplicationStyle value); storm::RationalNumber const& getSorOmega() const; void setSorOmega(storm::RationalNumber const& value); + bool isForceBoundsSet() const; + void setForceBounds(bool value); private: storm::solver::NativeLinearEquationSolverMethod method; @@ -36,6 +38,7 @@ namespace storm { bool considerRelativeTerminationCriterion; storm::solver::MultiplicationStyle powerMethodMultiplicationStyle; storm::RationalNumber sorOmega; + bool forceBounds; }; } diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index 628e0bd75..a34679ae8 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -23,6 +23,7 @@ namespace storm { const std::string NativeEquationSolverSettings::precisionOptionName = "precision"; const std::string NativeEquationSolverSettings::absoluteOptionName = "absolute"; const std::string NativeEquationSolverSettings::powerMethodMultiplicationStyleOptionName = "powmult"; + const std::string NativeEquationSolverSettings::forceBoundsOptionName = "forcebounds"; NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) { std::vector methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "ratsearch", "qpower" }; @@ -39,6 +40,9 @@ namespace storm { std::vector multiplicationStyles = {"gaussseidel", "regular", "gs", "r"}; this->addOption(storm::settings::OptionBuilder(moduleName, powerMethodMultiplicationStyleOptionName, false, "Sets which method multiplication style to prefer for the power method.") .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, the equation solver always require that a priori bounds for the solution are computed.").build()); + } bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const { @@ -107,6 +111,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown multiplication style '" << multiplicationStyleString << "'."); } + bool NativeEquationSolverSettings::isForceBoundsSet() const { + return this->getOption(forceBoundsOptionName).getHasOptionBeenSet(); + } + bool NativeEquationSolverSettings::check() const { // This list does not include the precision, because this option is shared with other modules. bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet(); diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.h b/src/storm/settings/modules/NativeEquationSolverSettings.h index 32d3caed1..67d68cb2d 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.h +++ b/src/storm/settings/modules/NativeEquationSolverSettings.h @@ -100,6 +100,11 @@ namespace storm { */ storm::solver::MultiplicationStyle getPowerMethodMultiplicationStyle() const; + /*! + * Retrieves whether the force bounds option has been set. + */ + bool isForceBoundsSet() const; + bool check() const override; // The name of the module. @@ -114,6 +119,8 @@ namespace storm { static const std::string precisionOptionName; static const std::string absoluteOptionName; static const std::string powerMethodMultiplicationStyleOptionName; + static const std::string forceBoundsOptionName; + }; } // namespace modules diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 76e261961..06e9efebb 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -1128,6 +1128,10 @@ namespace storm { LinearEquationSolverRequirements NativeLinearEquationSolver::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const { LinearEquationSolverRequirements requirements; if (task != LinearEquationSolverTask::Multiply) { + if (env.solver().native().isForceBoundsSet()) { + requirements.requiresLowerBounds(); + requirements.requiresUpperBounds(); + } auto method = getMethod(env, storm::NumberTraits::IsExact); if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) { requirements.requireBounds();