From e54a035ab98e508849b9b7b627d2dcc9eba30670 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 4 Mar 2020 16:04:43 +0100 Subject: [PATCH] SolverEnvironment: Added the switch `forceExact` to switch to exact solving methods more conveniently. --- src/storm/environment/solver/SolverEnvironment.cpp | 9 +++++++++ src/storm/environment/solver/SolverEnvironment.h | 3 +++ .../modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 2 +- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 2 +- src/storm/solver/EigenLinearEquationSolver.cpp | 2 +- src/storm/solver/GmmxxLinearEquationSolver.cpp | 1 + .../solver/IterativeMinMaxLinearEquationSolver.cpp | 4 ++-- src/storm/solver/LinearEquationSolver.cpp | 11 +++++++++-- src/storm/solver/NativeLinearEquationSolver.cpp | 6 +++--- src/storm/solver/StandardGameSolver.cpp | 2 +- 11 files changed, 32 insertions(+), 12 deletions(-) diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 9825d926b..edde86615 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -23,6 +23,7 @@ namespace storm { SolverEnvironment::SolverEnvironment() { forceSoundness = storm::settings::getModule().isSoundSet(); + forceExact = storm::settings::getModule().isExactSet(); linearEquationSolverType = storm::settings::getModule().getEquationSolver(); linearEquationSolverTypeSetFromDefault = storm::settings::getModule().isEquationSolverSetFromDefaultValue(); } @@ -111,6 +112,14 @@ namespace storm { SolverEnvironment::forceSoundness = value; } + bool SolverEnvironment::isForceExact() const { + return forceExact; + } + + void SolverEnvironment::setForceExact(bool value) { + SolverEnvironment::forceExact = value; + } + storm::solver::EquationSolverType const& SolverEnvironment::getLinearEquationSolverType() const { return linearEquationSolverType; } diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h index 4f0a88869..487213918 100644 --- a/src/storm/environment/solver/SolverEnvironment.h +++ b/src/storm/environment/solver/SolverEnvironment.h @@ -48,6 +48,8 @@ namespace storm { bool isForceSoundness() const; void setForceSoundness(bool value); + bool isForceExact() const; + void setForceExact(bool value); storm::solver::EquationSolverType const& getLinearEquationSolverType() const; void setLinearEquationSolverType(storm::solver::EquationSolverType const& value, bool isSetFromDefault = false); @@ -70,6 +72,7 @@ namespace storm { storm::solver::EquationSolverType linearEquationSolverType; bool linearEquationSolverTypeSetFromDefault; bool forceSoundness; + bool forceExact; }; } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 6d82a6d79..5911b4044 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -576,7 +576,7 @@ namespace storm { } storm::solver::LraMethod method = env.solver().lra().getDetLraMethod(); - if (storm::NumberTraits::IsExact && env.solver().lra().isDetLraMethodSetFromDefault() && method == storm::solver::LraMethod::ValueIteration) { + if ((storm::NumberTraits::IsExact || env.solver().isForceExact()) && env.solver().lra().isDetLraMethodSetFromDefault() && method == storm::solver::LraMethod::ValueIteration) { method = storm::solver::LraMethod::GainBiasEquations; STORM_LOG_INFO("Selecting " << storm::solver::toString(method) << " 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."); } else if (env.solver().isForceSoundness() && env.solver().lra().isDetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 8e6f427ab..0fac47232 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -820,7 +820,7 @@ namespace storm { // Solve MEC with the method specified in the settings storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod(); - if (storm::NumberTraits::IsExact && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) { + if ((storm::NumberTraits::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && 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; } else if (env.solver().isForceSoundness() && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 0bcc31726..122814633 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1477,7 +1477,7 @@ namespace storm { // Solve MEC with the method specified in the settings storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod(); - if (storm::NumberTraits::IsExact && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) { + if ((storm::NumberTraits::IsExact || env.solver().isForceExact()) && env.solver().lra().isNondetLraMethodSetFromDefault() && 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; } else if (env.solver().isForceSoundness() && env.solver().lra().isNondetLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) { diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index 6c96715cf..0ca9a4554 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -107,7 +107,7 @@ namespace storm { auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); - auto solutionMethod = getMethod(env, false); + auto solutionMethod = getMethod(env, env.solver().isForceExact()); if (solutionMethod == EigenLinearEquationSolverMethod::SparseLU) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with sparse LU factorization (Eigen library)."); StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index 9ce51fa72..a42386c0e 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -46,6 +46,7 @@ namespace storm { template GmmxxLinearEquationSolverMethod GmmxxLinearEquationSolver::getMethod(Environment const& env) const { STORM_LOG_ERROR_COND(!env.solver().isForceSoundness(), "This linear equation solver does not support sound computations. Using unsound methods now..."); + STORM_LOG_ERROR_COND(!env.solver().isForceExact(), "This linear equation solver does not support exact computations. Using unsound methods now..."); return env.solver().gmmxx().getMethod(); } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index df53fb538..44a2ee9a5 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -64,7 +64,7 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector& x, std::vector const& b) const { bool result = false; - switch (getMethod(env, storm::NumberTraits::IsExact)) { + switch (getMethod(env, storm::NumberTraits::IsExact || env.solver().isForceExact())) { case MinMaxMethod::ValueIteration: result = solveEquationsValueIteration(env, dir, x, b); break; @@ -228,7 +228,7 @@ namespace storm { template MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { - auto method = getMethod(env, storm::NumberTraits::IsExact); + auto method = getMethod(env, storm::NumberTraits::IsExact || env.solver().isForceExact()); // Check whether a linear equation solver is needed and potentially start with its requirements bool needsLinEqSolver = false; diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp index 8207efcff..5d2884d86 100644 --- a/src/storm/solver/LinearEquationSolver.cpp +++ b/src/storm/solver/LinearEquationSolver.cpp @@ -128,8 +128,15 @@ namespace storm { std::unique_ptr> GeneralLinearEquationSolverFactory::create(Environment const& env) const { EquationSolverType type = env.solver().getLinearEquationSolverType(); - // Adjust the solver type if none was specified and we want sound computations - if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) { + // Adjust the solver type if none was specified and we want sound/exact computations + if (env.solver().isForceExact() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) { + if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) { + type = EquationSolverType::Eigen; + STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee exact results. If you want to override this, please explicitly specify a different solver."); + } else { + STORM_LOG_WARN("The selected solver does not yield exact results."); + } + } else if (env.solver().isForceSoundness() && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination && type != EquationSolverType::Topological) { if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) { type = EquationSolverType::Native; STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee sound results. If you want to override this, please explicitly specify a different solver."); diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index ca0142249..a79bc6b3e 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -922,7 +922,7 @@ namespace storm { template bool NativeLinearEquationSolver::internalSolveEquations(Environment const& env, std::vector& x, std::vector const& b) const { - switch(getMethod(env, storm::NumberTraits::IsExact)) { + switch(getMethod(env, storm::NumberTraits::IsExact || env.solver().isForceExact())) { case NativeLinearEquationSolverMethod::SOR: return this->solveEquationsSOR(env, x, b, storm::utility::convertNumber(env.solver().native().getSorOmega())); case NativeLinearEquationSolverMethod::GaussSeidel: @@ -946,7 +946,7 @@ namespace storm { template LinearEquationSolverProblemFormat NativeLinearEquationSolver::getEquationProblemFormat(Environment const& env) const { - auto method = getMethod(env, storm::NumberTraits::IsExact); + auto method = getMethod(env, storm::NumberTraits::IsExact || env.solver().isForceExact()); if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundValueIteration || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::IntervalIteration) { return LinearEquationSolverProblemFormat::FixedPointSystem; } else { @@ -957,7 +957,7 @@ namespace storm { template LinearEquationSolverRequirements NativeLinearEquationSolver::getRequirements(Environment const& env) const { LinearEquationSolverRequirements requirements; - auto method = getMethod(env, storm::NumberTraits::IsExact); + auto method = getMethod(env, storm::NumberTraits::IsExact || env.solver().isForceExact()); if (method == NativeLinearEquationSolverMethod::IntervalIteration) { requirements.requireBounds(); } else if (method == NativeLinearEquationSolverMethod::RationalSearch) { diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index a818f2706..8fcc46a80 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -72,7 +72,7 @@ namespace storm { template bool StandardGameSolver::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector& x, std::vector const& b, std::vector* player1Choices, std::vector* player2Choices) const { - auto method = getMethod(env, std::is_same::value); + auto method = getMethod(env, std::is_same::value || env.solver().isForceExact()); STORM_LOG_INFO("Solving stochastic two player game over " << x.size() << " states using " << toString(method) << "."); switch (method) { case GameMethod::ValueIteration: