diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 0fc234c83..fe1f120de 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -256,7 +256,7 @@ namespace storm { // Initialize the x vector with the hint (if available) or with 1 for each element. // This is the initial guess for the iterative solvers. std::vector x; - if(hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { + if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasResultHint()) { x = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint().getResultHint(), maybeStates); } else { x = std::vector(submatrix.getColumnCount(), storm::utility::one()); diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp index f9da0758d..41de60629 100644 --- a/src/storm/solver/LinearEquationSolver.cpp +++ b/src/storm/solver/LinearEquationSolver.cpp @@ -11,6 +11,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" @@ -190,9 +191,36 @@ namespace storm { return this->create()->getRequirements(); } + template + GeneralLinearEquationSolverFactory::GeneralLinearEquationSolverFactory() { + auto const& coreSettings = storm::settings::getModule(); + auto const& generalSettings = storm::settings::getModule(); + + EquationSolverType actualEquationSolver = coreSettings.getEquationSolver(); + if (generalSettings.isSoundSet()) { + if (coreSettings.isEquationSolverSetFromDefaultValue()) { + STORM_LOG_WARN_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver to guarantee soundness. To select other solvers, please explicitly specify a solver."); + } else { + STORM_LOG_WARN_COND(actualEquationSolver == EquationSolverType::Native, "Switching to native equation solver from explicitly selected solver '" << storm::solver::toString(actualEquationSolver) << "' to guarantee soundness."); + } + actualEquationSolver = EquationSolverType::Native; + } + + setEquationSolverType(actualEquationSolver); + } + + template + GeneralLinearEquationSolverFactory::GeneralLinearEquationSolverFactory(EquationSolverType const& equationSolver) { + setEquationSolverType(equationSolver); + } + + template + void GeneralLinearEquationSolverFactory::setEquationSolverType(EquationSolverType const& equationSolver) { + this->equationSolver = equationSolver; + } + template std::unique_ptr> GeneralLinearEquationSolverFactory::create() const { - EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); switch (equationSolver) { case EquationSolverType::Gmmxx: return std::make_unique>(); case EquationSolverType::Native: return std::make_unique>(); diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h index 1aa0a0fa4..f17c9d865 100644 --- a/src/storm/solver/LinearEquationSolver.h +++ b/src/storm/solver/LinearEquationSolver.h @@ -215,6 +215,8 @@ namespace storm { storm::utility::VectorHelper vectorHelper; }; + enum class EquationSolverType; + template class LinearEquationSolverFactory { public: @@ -260,11 +262,23 @@ namespace storm { template class GeneralLinearEquationSolverFactory : public LinearEquationSolverFactory { public: + GeneralLinearEquationSolverFactory(); + GeneralLinearEquationSolverFactory(EquationSolverType const& equationSolver); + using LinearEquationSolverFactory::create; virtual std::unique_ptr> create() const override; virtual std::unique_ptr> clone() const override; + + private: + /*! + * Sets the equation solver type. + */ + void setEquationSolverType(EquationSolverType const& equationSolver); + + // The equation solver type. + EquationSolverType equationSolver; }; #ifdef STORM_HAVE_CARL