From 8cdbf281fae2e4f97eea6c6427d2b4a19193ad80 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 19 Aug 2017 11:12:13 +0200 Subject: [PATCH] make minmax solvers use policy iteration when --exact is set and no other method was explicitly set --- src/storm/settings/Argument.cpp | 10 ++++++++-- src/storm/settings/Argument.h | 5 +++++ src/storm/settings/ArgumentBase.h | 4 +++- .../modules/MinMaxEquationSolverSettings.cpp | 4 ++++ .../modules/MinMaxEquationSolverSettings.h | 11 +++++++++-- .../solver/IterativeMinMaxLinearEquationSolver.h | 2 +- src/storm/solver/MinMaxLinearEquationSolver.cpp | 15 ++++++++++++++- 7 files changed, 44 insertions(+), 7 deletions(-) diff --git a/src/storm/settings/Argument.cpp b/src/storm/settings/Argument.cpp index ddb39c0ab..555bcdb9d 100644 --- a/src/storm/settings/Argument.cpp +++ b/src/storm/settings/Argument.cpp @@ -12,12 +12,12 @@ namespace storm { namespace settings { template - Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(false), defaultValue(), hasDefaultValue(false), wasSetFromDefaultValueFlag(false) { // Intentionally left empty. } template - Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true) { + Argument::Argument(std::string const& name, std::string const& description, std::vector>> const& validators, bool isOptional, T defaultValue): ArgumentBase(name, description), argumentValue(), argumentType(inferToEnumType()), validators(validators), isOptional(isOptional), defaultValue(), hasDefaultValue(true), wasSetFromDefaultValueFlag(false) { this->setDefaultValue(defaultValue); } @@ -71,6 +71,12 @@ namespace storm { STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument " << name << " has none."); bool result = this->setFromTypeValue(this->defaultValue, false); STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument " << name << ", because it was rejected."); + this->wasSetFromDefaultValueFlag = true; + } + + template + bool Argument::wasSetFromDefaultValue() const { + return wasSetFromDefaultValueFlag; } template diff --git a/src/storm/settings/Argument.h b/src/storm/settings/Argument.h index 080d06409..2074557cf 100644 --- a/src/storm/settings/Argument.h +++ b/src/storm/settings/Argument.h @@ -85,6 +85,8 @@ namespace storm { void setFromDefaultValue() override; + virtual bool wasSetFromDefaultValue() const override; + virtual std::string getValueAsString() const override; virtual int_fast64_t getValueAsInteger() const override; @@ -116,6 +118,9 @@ namespace storm { // A flag indicating whether a default value has been provided. bool hasDefaultValue; + // A flag indicating whether the argument was set from the default value. + bool wasSetFromDefaultValueFlag; + /*! * Sets the default value of the argument to the provided value. * diff --git a/src/storm/settings/ArgumentBase.h b/src/storm/settings/ArgumentBase.h index 6808bd815..b48a46183 100644 --- a/src/storm/settings/ArgumentBase.h +++ b/src/storm/settings/ArgumentBase.h @@ -80,6 +80,8 @@ namespace storm { */ virtual void setFromDefaultValue() = 0; + virtual bool wasSetFromDefaultValue() const = 0; + /*! * Tries to set the value of the argument from the given string. * @@ -134,7 +136,7 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, ArgumentBase const& argument); - protected: + protected: // A flag indicating whether the argument has been set. bool hasBeenSet; diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index 398eaaeac..de9ce1746 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -50,6 +50,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } + bool MinMaxEquationSolverSettings::isMinMaxEquationSolvingMethodSetFromDefaultValue() const { + return !this->getOption(solvingMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(solvingMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue(); + } + bool MinMaxEquationSolverSettings::isMinMaxEquationSolvingMethodSet() const { return this->getOption(solvingMethodOptionName).getHasOptionBeenSet(); } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index 35bee18ac..1ce4a9db7 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -27,12 +27,19 @@ namespace storm { bool isMinMaxEquationSolvingMethodSet() const; /*! - * Retrieves the selected min/max equation solving technique. + * Retrieves the selected min/max equation solving method. * - * @return The selected min/max equation solving technique. + * @return The selected min/max equation solving method. */ storm::solver::MinMaxMethod getMinMaxEquationSolvingMethod() const; + /*! + * Retrieves whether the min/max equation solving method is set from its default value. + * + * @return True iff if it is set from its default value. + */ + bool isMinMaxEquationSolvingMethodSetFromDefaultValue() const; + /*! * Retrieves whether the maximal iteration count has been set. * diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 301db3049..e197f88b0 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -73,7 +73,7 @@ namespace storm { IterativeMinMaxLinearEquationSolverSettings settings; }; - template + template class IterativeMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: IterativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false); diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 08c70bd58..aa68fd9e3 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -154,7 +154,19 @@ namespace storm { template void MinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethodSelection const& newMethod) { if (newMethod == MinMaxMethodSelection::FROMSETTINGS) { - setMinMaxMethod(storm::settings::getModule().getMinMaxEquationSolvingMethod()); + bool wasSet = false; + auto const& minMaxSettings = storm::settings::getModule(); + if (std::is_same::value) { + if (minMaxSettings.isMinMaxEquationSolvingMethodSetFromDefaultValue()) { + STORM_LOG_WARN("Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method."); + this->setMinMaxMethod(MinMaxMethod::PolicyIteration); + wasSet = true; + } + } + + if (!wasSet) { + setMinMaxMethod(minMaxSettings.getMinMaxEquationSolvingMethod()); + } } else { setMinMaxMethod(convert(newMethod)); } @@ -162,6 +174,7 @@ namespace storm { template void MinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethod const& newMethod) { + STORM_LOG_WARN_COND(!(std::is_same::value) || newMethod == MinMaxMethod::PolicyIteration, "The selected solution method does not guarantee exact result. Consider using policy iteration."); method = newMethod; }