From 068c1b3ea67b40510386b02f685c1d7ad47fc1cb Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 3 Dec 2019 10:58:25 +0100 Subject: [PATCH] Removed obsolete settings --- .../solver/MinMaxSolverEnvironment.cpp | 17 ----------------- .../solver/MinMaxSolverEnvironment.h | 5 ----- .../modules/MinMaxEquationSolverSettings.cpp | 19 ------------------- .../modules/MinMaxEquationSolverSettings.h | 13 ------------- .../prctl/mdp/LraMdpPrctlModelCheckerTest.cpp | 12 ++++++------ 5 files changed, 6 insertions(+), 60 deletions(-) diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp index 63f29573e..63cf5c698 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.cpp +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.cpp @@ -22,8 +22,6 @@ namespace storm { STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion"); multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle(); symmetricUpdates = minMaxSettings.isForceIntervalIterationSymmetricUpdatesSet(); - lraMethod = minMaxSettings.getLraMethod(); - lraMethodSetFromDefault = minMaxSettings.isLraMethodSetFromDefaultValue(); } MinMaxSolverEnvironment::~MinMaxSolverEnvironment() { @@ -83,19 +81,4 @@ namespace storm { symmetricUpdates = value; } - storm::solver::LraMethod const& MinMaxSolverEnvironment::getLraMethod() const { - return lraMethod; - } - - bool const& MinMaxSolverEnvironment::isLraMethodSetFromDefault() const { - return lraMethodSetFromDefault; - } - - void MinMaxSolverEnvironment::setLraMethod(storm::solver::LraMethod value, bool isSetFromDefault) { - lraMethod = value; - lraMethodSetFromDefault = isSetFromDefault; - } - - - } diff --git a/src/storm/environment/solver/MinMaxSolverEnvironment.h b/src/storm/environment/solver/MinMaxSolverEnvironment.h index 104eee739..b0a19d8c4 100644 --- a/src/storm/environment/solver/MinMaxSolverEnvironment.h +++ b/src/storm/environment/solver/MinMaxSolverEnvironment.h @@ -27,9 +27,6 @@ namespace storm { void setMultiplicationStyle(storm::solver::MultiplicationStyle value); bool isSymmetricUpdatesSet() const; void setSymmetricUpdates(bool value); - storm::solver::LraMethod const& getLraMethod() const; - bool const& isLraMethodSetFromDefault() const; - void setLraMethod(storm::solver::LraMethod value, bool isSetFromDefault = false); private: storm::solver::MinMaxMethod minMaxMethod; @@ -39,8 +36,6 @@ namespace storm { bool considerRelativeTerminationCriterion; storm::solver::MultiplicationStyle multiplicationStyle; bool symmetricUpdates; - storm::solver::LraMethod lraMethod; - bool lraMethodSetFromDefault; }; } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index eb429d272..c8a4f7141 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -17,7 +17,6 @@ namespace storm { const std::string MinMaxEquationSolverSettings::maximalIterationsOptionShortName = "i"; const std::string MinMaxEquationSolverSettings::precisionOptionName = "precision"; const std::string MinMaxEquationSolverSettings::absoluteOptionName = "absolute"; - const std::string MinMaxEquationSolverSettings::lraMethodOptionName = "lramethod"; const std::string MinMaxEquationSolverSettings::markovAutomatonBoundedReachabilityMethodOptionName = "mamethod"; const std::string MinMaxEquationSolverSettings::valueIterationMultiplicationStyleOptionName = "vimult"; const std::string MinMaxEquationSolverSettings::intervalIterationSymmetricUpdatesOptionName = "symmetricupdates"; @@ -33,10 +32,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").setIsAdvanced().build()); - std::vector lraMethods = {"vi", "value-iteration", "linear-programming", "lp"}; - this->addOption(storm::settings::OptionBuilder(moduleName, lraMethodOptionName, false, "Sets which method is preferred for computing long run averages.").setIsAdvanced() - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a long run average computation method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lraMethods)).setDefaultValueString("vi").build()).build()); - std::vector maMethods = {"imca", "unifplus"}; this->addOption(storm::settings::OptionBuilder(moduleName, markovAutomatonBoundedReachabilityMethodOptionName, false, "The method to use to solve bounded reachability queries on MAs.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build()); @@ -103,20 +98,6 @@ namespace storm { return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute : MinMaxEquationSolverSettings::ConvergenceCriterion::Relative; } - storm::solver::LraMethod MinMaxEquationSolverSettings::getLraMethod() const { - std::string lraMethodString = this->getOption(lraMethodOptionName).getArgumentByName("name").getValueAsString(); - if (lraMethodString == "value-iteration" || lraMethodString == "vi") { - return storm::solver::LraMethod::ValueIteration; - } else if (lraMethodString == "linear-programming" || lraMethodString == "lp") { - return storm::solver::LraMethod::LinearProgramming; - } - STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown lra solving technique '" << lraMethodString << "'."); - } - - bool MinMaxEquationSolverSettings::isLraMethodSetFromDefaultValue() const { - return !this->getOption(lraMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(lraMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue(); - } - MinMaxEquationSolverSettings::MarkovAutomatonBoundedReachabilityMethod MinMaxEquationSolverSettings::getMarkovAutomatonBoundedReachabilityMethod() const { std::string techniqueAsString = this->getOption(markovAutomatonBoundedReachabilityMethodOptionName).getArgumentByName("name").getValueAsString(); if (techniqueAsString == "imca") { diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index 2b958d374..5e7bf9b98 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -86,18 +86,6 @@ namespace storm { */ ConvergenceCriterion getConvergenceCriterion() const; - /*! - * Retrieves the selected long run average method. - * - * @return The selected long run average method. - */ - storm::solver::LraMethod getLraMethod() const; - - /*! - * Retrieves whether the LraMethod was set from a default value. - */ - bool isLraMethodSetFromDefaultValue() const; - /*! * Retrieves the method to be used for bounded reachability on MAs. * @@ -126,7 +114,6 @@ namespace storm { static const std::string maximalIterationsOptionShortName; static const std::string precisionOptionName; static const std::string absoluteOptionName; - static const std::string lraMethodOptionName; static const std::string markovAutomatonBoundedReachabilityMethodOptionName; static const std::string valueIterationMultiplicationStyleOptionName; static const std::string intervalIterationSymmetricUpdatesOptionName; diff --git a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp index 0a6ed97a3..ff5140626 100755 --- a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp @@ -22,7 +22,7 @@ #include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm-parsers/parser/AutoParser.h" -#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" namespace { @@ -34,8 +34,8 @@ namespace { typedef storm::models::sparse::Mdp ModelType; static storm::Environment createEnvironment() { storm::Environment env; - env.solver().minMax().setLraMethod(storm::solver::LraMethod::ValueIteration); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::ValueIteration); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-10)); return env; } }; @@ -47,8 +47,8 @@ namespace { typedef storm::models::sparse::Mdp ModelType; static storm::Environment createEnvironment() { storm::Environment env; - env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming); - env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::LinearProgramming); + env.solver().lra().setPrecision(storm::utility::convertNumber(1e-10)); return env; } }; @@ -60,7 +60,7 @@ namespace { typedef storm::models::sparse::Mdp ModelType; static storm::Environment createEnvironment() { storm::Environment env; - env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming); + env.solver().lra().setNondetLraMethod(storm::solver::LraMethod::LinearProgramming); return env; } };