diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index bd33e747e..1ca0b3728 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -415,10 +415,10 @@ namespace storm { } // Solve MEC with the method specified in the settings - storm::solver::MinMaxMethod method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); - if (method == storm::solver::MinMaxMethod::LinearProgramming) { + storm::solver::LraMethod method = storm::settings::getModule().getLraMethod(); + if (method == storm::solver::LraMethod::LinearProgramming) { return computeLraForMaximalEndComponentLP(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec); - } else if (method == storm::solver::MinMaxMethod::ValueIteration) { + } else if (method == storm::solver::LraMethod::ValueIteration) { return computeLraForMaximalEndComponentVI(dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec, minMaxLinearEquationSolverFactory); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index ca2c1c6ff..c8dab63c4 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -692,10 +692,10 @@ namespace storm { } // Solve MEC with the method specified in the settings - storm::solver::MinMaxMethod method = storm::settings::getModule().getMinMaxEquationSolvingMethod(); - if (method == storm::solver::MinMaxMethod::LinearProgramming) { + storm::solver::LraMethod method = storm::settings::getModule().getLraMethod(); + if (method == storm::solver::LraMethod::LinearProgramming) { return computeLraForMaximalEndComponentLP(dir, transitionMatrix, rewardModel, mec); - } else if (method == storm::solver::MinMaxMethod::ValueIteration) { + } else if (method == storm::solver::LraMethod::ValueIteration) { return computeLraForMaximalEndComponentVI(dir, transitionMatrix, rewardModel, mec, minMaxLinearEquationSolverFactory); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index dccb37a7a..398eaaeac 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -17,6 +17,7 @@ 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"; MinMaxEquationSolverSettings::MinMaxEquationSolverSettings() : ModuleSettings(moduleName) { std::vector minMaxSolvingTechniques = {"vi", "value-iteration", "pi", "policy-iteration", "linear-programming", "lp", "acyclic"}; @@ -28,6 +29,11 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").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.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of a long run average computation method.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lraMethods)).setDefaultValueString("vi").build()).build()); + } storm::solver::MinMaxMethod MinMaxEquationSolverSettings::getMinMaxEquationSolvingMethod() const { @@ -72,6 +78,17 @@ 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 << "'."); + } + + } } } diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.h b/src/storm/settings/modules/MinMaxEquationSolverSettings.h index 6129b731f..35bee18ac 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -75,6 +75,13 @@ namespace storm { */ ConvergenceCriterion getConvergenceCriterion() const; + /*! + * Retrieves the selected long run average method. + * + * @return The selected long run average method. + */ + storm::solver::LraMethod getLraMethod() const; + // The name of the module. static const std::string moduleName; @@ -84,6 +91,7 @@ namespace storm { static const std::string maximalIterationsOptionShortName; static const std::string precisionOptionName; static const std::string absoluteOptionName; + static const std::string lraMethodOptionName; }; } diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index 047311388..5a516c8dd 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -18,6 +18,16 @@ namespace storm { return "invalid"; } + std::string toString(LraMethod m) { + switch(m) { + case LraMethod::LinearProgramming: + return "linearprogramming"; + case LraMethod::ValueIteration: + return "valueiteration"; + } + return "invalid"; + } + std::string toString(LpSolverType t) { switch(t) { case LpSolverType::Gurobi: diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 8f531a0f9..141bc8a0e 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -8,6 +8,7 @@ namespace storm { namespace solver { ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, Acyclic) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) + ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration) ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3) ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination)