diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 6e6a39acf..1975ebf45 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -16,6 +16,7 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" +#include "storm/utility/NumberTraits.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" @@ -824,7 +825,12 @@ namespace storm { } // Solve MEC with the method specified in the settings - storm::solver::LraMethod method = storm::settings::getModule().getLraMethod(); + auto minMaxSettings = storm::settings::getModule(); + storm::solver::LraMethod method = minMaxSettings.getLraMethod(); + if (storm::NumberTraits::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) { + STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); + method = storm::solver::LraMethod::LinearProgramming; + } if (method == storm::solver::LraMethod::LinearProgramming) { return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, exitRateVector, markovianStates, rewardModel, mec); } else if (method == storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 81c53dfd9..8c7b93738 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -34,6 +34,7 @@ #include "storm/utility/Stopwatch.h" #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/export.h" +#include "storm/utility/NumberTraits.h" #include "storm/transformer/EndComponentEliminator.h" @@ -1478,7 +1479,12 @@ namespace storm { } // Solve MEC with the method specified in the settings - storm::solver::LraMethod method = storm::settings::getModule().getLraMethod(); + auto minMaxSettings = storm::settings::getModule(); + storm::solver::LraMethod method = minMaxSettings.getLraMethod(); + if (storm::NumberTraits::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) { + STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); + method = storm::solver::LraMethod::LinearProgramming; + } if (method == storm::solver::LraMethod::LinearProgramming) { return computeLraForMaximalEndComponentLP(env, dir, transitionMatrix, rewardModel, mec); } else if (method == storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 343d3c3d1..3925012e3 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -112,6 +112,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } + bool CoreSettings::isLpSolverSetFromDefaultValue() const { + return !this->getOption(lpSolverOptionName).getHasOptionBeenSet() || this->getOption(lpSolverOptionName).getArgumentByName("name").wasSetFromDefaultValue(); + } + storm::solver::SmtSolverType CoreSettings::getSmtSolver() const { std::string smtSolverName = this->getOption(smtSolverOptionName).getArgumentByName("name").getValueAsString(); if (smtSolverName == "z3") { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index 8a07a48d0..483e61df3 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -94,6 +94,13 @@ namespace storm { * @return The selected LP solver. */ storm::solver::LpSolverType getLpSolver() const; + + /*! + * Retrieves whether the lp solver has been set from its default value. + * + * @return True iff it has been set from its default value. + */ + bool isLpSolverSetFromDefaultValue() const; /*! * Retrieves the selected SMT solver. diff --git a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp index d0e891b56..0a2943efd 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.cpp @@ -111,6 +111,10 @@ namespace storm { 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 43d3d1b00..2b958d374 100644 --- a/src/storm/settings/modules/MinMaxEquationSolverSettings.h +++ b/src/storm/settings/modules/MinMaxEquationSolverSettings.h @@ -93,6 +93,11 @@ namespace storm { */ 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. * diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 6955f5eed..34982374e 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -15,6 +15,7 @@ #include "storm/solver/MathsatSmtSolver.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/utility/NumberTraits.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -25,8 +26,11 @@ namespace storm { template std::unique_ptr> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; - if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { + if (solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { t = storm::settings::getModule().getLpSolver(); + if (storm::NumberTraits::IsExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule().isLpSolverSetFromDefaultValue()) { + t = storm::solver::LpSolverType::Z3; + } } else { t = convert(solvT); }