diff --git a/src/storm/environment/solver/TopologicalSolverEnvironment.cpp b/src/storm/environment/solver/TopologicalSolverEnvironment.cpp index 244adc1fa..678c6cb6c 100644 --- a/src/storm/environment/solver/TopologicalSolverEnvironment.cpp +++ b/src/storm/environment/solver/TopologicalSolverEnvironment.cpp @@ -13,10 +13,8 @@ namespace storm { underlyingEquationSolverType = topologicalSettings.getUnderlyingEquationSolverType(); underlyingEquationSolverTypeSetFromDefault = topologicalSettings.isUnderlyingEquationSolverTypeSetFromDefaultValue(); - std::cout << "Get topo env minmax from settings!!" << std::endl; - underlyingMinMaxMethod = storm::solver::MinMaxMethod::ValueIteration; - underlyingEquationSolverTypeSetFromDefault = false; - + underlyingMinMaxMethod = topologicalSettings.getUnderlyingMinMaxMethod(); + underlyingEquationSolverTypeSetFromDefault = topologicalSettings.isUnderlyingMinMaxMethodSetFromDefaultValue(); } TopologicalSolverEnvironment::~TopologicalSolverEnvironment() { diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index 35145e829..c0728c579 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::quickValueIterationRestartOptionName = "qvirestart"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration"}; + std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration", "topological"}; 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("vi").build()).build()); @@ -60,6 +60,8 @@ namespace storm { return storm::solver::MinMaxMethod::RationalSearch; } else if (minMaxEquationSolvingTechnique == "quick-value-iteration" || minMaxEquationSolvingTechnique == "qvi") { return storm::solver::MinMaxMethod::QuickValueIteration; + } else if (minMaxEquationSolvingTechnique == "topological") { + return storm::solver::MinMaxMethod::Topological; } 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 c5f74a124..ec551fae1 100644 --- a/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp +++ b/src/storm/settings/modules/TopologicalEquationSolverSettings.cpp @@ -28,6 +28,9 @@ 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", "linear-programming", "lp", "ratsearch", "qvi", "quick-value-iteration"}; + 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(linearEquationSolver)).setDefaultValueString("value-iteration").build()).build()); } bool TopologicalEquationSolverSettings::isUnderlyingEquationSolverTypeSet() const { @@ -52,11 +55,39 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << equationSolverName << "'."); } + bool TopologicalEquationSolverSettings::isUnderlyingMinMaxMethodSet() const { + return this->getOption(underlyingMinMaxMethodOptionName).getHasOptionBeenSet(); + } + + bool TopologicalEquationSolverSettings::isUnderlyingMinMaxMethodSetFromDefaultValue() const { + return !this->getOption(underlyingMinMaxMethodOptionName).getHasOptionBeenSet() || this->getOption(underlyingMinMaxMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue(); + } + + storm::solver::MinMaxMethod TopologicalEquationSolverSettings::getUnderlyingMinMaxMethod() const { + std::string minMaxEquationSolvingTechnique = this->getOption(underlyingMinMaxMethodOptionName).getArgumentByName("name").getValueAsString(); + if (minMaxEquationSolvingTechnique == "value-iteration" || minMaxEquationSolvingTechnique == "vi") { + return storm::solver::MinMaxMethod::ValueIteration; + } else if (minMaxEquationSolvingTechnique == "policy-iteration" || minMaxEquationSolvingTechnique == "pi") { + return storm::solver::MinMaxMethod::PolicyIteration; + } else if (minMaxEquationSolvingTechnique == "linear-programming" || minMaxEquationSolvingTechnique == "lp") { + return storm::solver::MinMaxMethod::LinearProgramming; + } else if (minMaxEquationSolvingTechnique == "ratsearch") { + return storm::solver::MinMaxMethod::RationalSearch; + } else if (minMaxEquationSolvingTechnique == "quick-value-iteration" || minMaxEquationSolvingTechnique == "qvi") { + return storm::solver::MinMaxMethod::QuickValueIteration; + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown underlying equation solver '" << equationSolverName << "'."); + } + bool TopologicalEquationSolverSettings::check() const { if (this->isUnderlyingEquationSolverTypeSet() && getUnderlyingEquationSolverType() == storm::solver::EquationSolverType::Topological) { STORM_LOG_WARN("Underlying solver type of the topological solver can not be the topological solver."); return false; } + if (this->isUnderlyingMinMaxMethodSet() && getUnderlyingMinMaxMethod() == storm::solver::MinMaxMethod::Topological) { + STORM_LOG_WARN("Underlying minmax method of the topological solver can not be topological."); + return false; + } return true; } diff --git a/src/storm/settings/modules/TopologicalEquationSolverSettings.h b/src/storm/settings/modules/TopologicalEquationSolverSettings.h index 45014db32..f9ddefd78 100644 --- a/src/storm/settings/modules/TopologicalEquationSolverSettings.h +++ b/src/storm/settings/modules/TopologicalEquationSolverSettings.h @@ -40,6 +40,27 @@ namespace storm { */ storm::solver::EquationSolverType getUnderlyingEquationSolverType() const; + /*! + * Retrieves whether the underlying equation solver type has been set. + * + * @return True iff the linear equation system technique has been set. + */ + bool isUnderlyingMinMaxMethodSet() const; + + /*! + * Retrieves whether the underlying minmax method is set from its default value. + * + * @return True iff it was set from its default value. + */ + bool isUnderlyingMinMaxMethodSetFromDefaultValue() const; + + /*! + * Retrieves the method that is to be used for solving systems of linear equations. + * + * @return The method to use. + */ + storm::solver::MinMaxMethod getUnderlyingMinMaxMethod() const; + bool check() const override; // The name of the module. @@ -48,6 +69,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string underlyingEquationSolverOptionName; + static const std::string underlyingMinMaxMethodOptionName; }; } // namespace modules