From a6c61187332b059da9b3e9788ab578656c7df8a0 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 15 Feb 2018 13:18:52 +0100 Subject: [PATCH] Renamed 'sound power' to interval iteration and 'quick sound power' to 'sound power' --- .../modules/NativeEquationSolverSettings.cpp | 6 ++-- .../solver/NativeLinearEquationSolver.cpp | 36 ++++++++----------- src/storm/solver/NativeLinearEquationSolver.h | 2 +- src/storm/solver/SolverSelectionOptions.cpp | 8 +++-- src/storm/solver/SolverSelectionOptions.h | 2 +- .../DtmcPrctlModelCheckerTest.cpp | 8 ++--- 6 files changed, 29 insertions(+), 33 deletions(-) diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index c07d56dff..ce92cef82 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -67,10 +67,12 @@ namespace storm { return storm::solver::NativeLinearEquationSolverMethod::WalkerChae; } else if (linearEquationSystemTechniqueAsString == "power") { return storm::solver::NativeLinearEquationSolverMethod::Power; + } else if (linearEquationSystemTechniqueAsString == "soundpower") { + return storm::solver::NativeLinearEquationSolverMethod::SoundPower; + } else if (linearEquationSystemTechniqueAsString == "interval-iteration") { + return storm::solver::NativeLinearEquationSolverMethod::IntervalIteration; } else if (linearEquationSystemTechniqueAsString == "ratsearch") { return storm::solver::NativeLinearEquationSolverMethod::RationalSearch; - } else if (linearEquationSystemTechniqueAsString == "qpower") { - return storm::solver::NativeLinearEquationSolverMethod::QuickPower; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected."); } diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index ad1c9136c..360acb2b8 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -396,10 +396,10 @@ namespace storm { } template - bool NativeLinearEquationSolver::solveEquationsSoundPower(Environment const& env, std::vector& x, std::vector const& b) const { + bool NativeLinearEquationSolver::solveEquationsIntervalIteration(Environment const& env, std::vector& x, std::vector const& b) const { STORM_LOG_THROW(this->hasLowerBound(), storm::exceptions::UnmetRequirementException, "Solver requires lower bound, but none was given."); STORM_LOG_THROW(this->hasUpperBound(), storm::exceptions::UnmetRequirementException, "Solver requires upper bound, but none was given."); - STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (SoundPower)"); + STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (IntervalIteration)"); std::vector* lowerX = &x; this->createLowerBoundsVector(*lowerX); @@ -557,8 +557,8 @@ namespace storm { } template - bool NativeLinearEquationSolver::solveEquationsQuickSoundPower(Environment const& env, std::vector& x, std::vector const& b) const { - STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (QuickPower)"); + bool NativeLinearEquationSolver::solveEquationsSoundPower(Environment const& env, std::vector& x, std::vector const& b) const { + STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (SoundPower)"); bool useGaussSeidelMultiplication = env.solver().native().getPowerMethodMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel; // Prepare the solution vectors. @@ -597,11 +597,6 @@ namespace storm { } uint64_t maxIter = env.solver().native().getMaximalNumberOfIterations(); - //std::cout << *this->A << std::endl; - //std::cout << storm::utility::vector::toString(b) << std::endl; - - //std::cout << "solving eq sys.. " << std::endl; - uint64_t iterations = 0; bool converged = false; bool terminate = false; @@ -1018,9 +1013,9 @@ namespace storm { } else { STORM_LOG_WARN("The selected solution method does not guarantee exact results."); } - } else if (env.solver().isForceSoundness() && method != NativeLinearEquationSolverMethod::Power && method != NativeLinearEquationSolverMethod::RationalSearch && method != NativeLinearEquationSolverMethod::QuickPower) { + } else if (env.solver().isForceSoundness() && method != NativeLinearEquationSolverMethod::SoundPower && method != NativeLinearEquationSolverMethod::IntervalIteration && method != NativeLinearEquationSolverMethod::RationalSearch) { if (env.solver().native().isMethodSetFromDefault()) { - method = NativeLinearEquationSolverMethod::Power; + method = NativeLinearEquationSolverMethod::SoundPower; STORM_LOG_INFO("Selecting '" + toString(method) + "' as the solution technique to guarantee sound results. If you want to override this, please explicitly specify a different method."); } else { STORM_LOG_WARN("The selected solution method does not guarantee sound results."); @@ -1042,13 +1037,11 @@ namespace storm { case NativeLinearEquationSolverMethod::WalkerChae: return this->solveEquationsWalkerChae(env, x, b); case NativeLinearEquationSolverMethod::Power: - if (env.solver().isForceSoundness()) { - return this->solveEquationsSoundPower(env, x, b); - } else { - return this->solveEquationsPower(env, x, b); - } - case NativeLinearEquationSolverMethod::QuickPower: - return this->solveEquationsQuickSoundPower(env, x, b); + return this->solveEquationsPower(env, x, b); + case NativeLinearEquationSolverMethod::SoundPower: + return this->solveEquationsSoundPower(env, x, b); + case NativeLinearEquationSolverMethod::IntervalIteration: + return this->solveEquationsIntervalIteration(env, x, b); case NativeLinearEquationSolverMethod::RationalSearch: return this->solveEquationsRationalSearch(env, x, b); } @@ -1119,7 +1112,7 @@ namespace storm { template LinearEquationSolverProblemFormat NativeLinearEquationSolver::getEquationProblemFormat(Environment const& env) const { auto method = getMethod(env, storm::NumberTraits::IsExact); - if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::QuickPower) { + if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundPower || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::IntervalIteration) { return LinearEquationSolverProblemFormat::FixedPointSystem; } else { return LinearEquationSolverProblemFormat::EquationSystem; @@ -1131,11 +1124,10 @@ namespace storm { LinearEquationSolverRequirements requirements; if (task != LinearEquationSolverTask::Multiply) { if (env.solver().native().isForceBoundsSet()) { - requirements.requiresLowerBounds(); - requirements.requiresUpperBounds(); + requirements.requireBounds(); } auto method = getMethod(env, storm::NumberTraits::IsExact); - if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) { + if (method == NativeLinearEquationSolverMethod::IntervalIteration) { requirements.requireBounds(); } else if (method == NativeLinearEquationSolverMethod::RationalSearch) { requirements.requireLowerBounds(); diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index fbb5d4357..795f5ef19 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -72,7 +72,7 @@ namespace storm { virtual bool solveEquationsWalkerChae(storm::Environment const& env, std::vector& x, std::vector const& b) const; virtual bool solveEquationsPower(storm::Environment const& env, std::vector& x, std::vector const& b) const; virtual bool solveEquationsSoundPower(storm::Environment const& env, std::vector& x, std::vector const& b) const; - virtual bool solveEquationsQuickSoundPower(storm::Environment const& env, std::vector& x, std::vector const& b) const; + virtual bool solveEquationsIntervalIteration(storm::Environment const& env, std::vector& x, std::vector const& b) const; virtual bool solveEquationsRationalSearch(storm::Environment const& env, std::vector& x, std::vector const& b) const; template diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index 7344dde0a..21693781a 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -73,7 +73,7 @@ namespace storm { } std::string toString(NativeLinearEquationSolverMethod t) { - switch( t) { + switch(t) { case NativeLinearEquationSolverMethod::Jacobi: return "Jacobi"; case NativeLinearEquationSolverMethod::GaussSeidel: @@ -84,10 +84,12 @@ namespace storm { return "WalkerChae"; case NativeLinearEquationSolverMethod::Power: return "Power"; + case NativeLinearEquationSolverMethod::SoundPower: + return "SoundPower"; + case NativeLinearEquationSolverMethod::IntervalIteration: + return "IntervalIteration"; case NativeLinearEquationSolverMethod::RationalSearch: return "RationalSearch"; - case NativeLinearEquationSolverMethod::QuickPower: - return "QuickPower"; } return "invalid"; } diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index a4bc6d614..e92c0ee0e 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -14,7 +14,7 @@ namespace storm { ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological) ExtendEnumsWithSelectionField(SmtSolverType, Z3, Mathsat) - ExtendEnumsWithSelectionField(NativeLinearEquationSolverMethod, Jacobi, GaussSeidel, SOR, WalkerChae, Power, RationalSearch, QuickPower) + ExtendEnumsWithSelectionField(NativeLinearEquationSolverMethod, Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundPower, IntervalIteration, RationalSearch) ExtendEnumsWithSelectionField(GmmxxLinearEquationSolverMethod, Bicgstab, Qmr, Gmres) ExtendEnumsWithSelectionField(GmmxxLinearEquationSolverPreconditioner, Ilu, Diagonal, None) ExtendEnumsWithSelectionField(EigenLinearEquationSolverMethod, SparseLU, Bicgstab, DGmres, Gmres) diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index bb569e5a5..4ba411f18 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -217,13 +217,13 @@ namespace { storm::Environment env; env.solver().setForceSoundness(true); env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power); + env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundPower); env.solver().native().setPrecision(storm::utility::convertNumber(1e-6)); return env; } }; - class SparseNativeQuickSoundPowerEnvironment { + class SparseNativeIntervalIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; @@ -234,7 +234,7 @@ namespace { storm::Environment env; env.solver().setForceSoundness(true); env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::QuickPower); + env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::IntervalIteration); env.solver().native().setRelativeTerminationCriterion(false); env.solver().native().setPrecision(storm::utility::convertNumber(1e-6)); return env; @@ -482,7 +482,7 @@ namespace { SparseNativeSorEnvironment, SparseNativePowerEnvironment, SparseNativeSoundPowerEnvironment, - SparseNativeQuickSoundPowerEnvironment, + SparseNativeIntervalIterationEnvironment, SparseNativeRationalSearchEnvironment, SparseTopologicalEigenLUEnvironment, HybridSylvanGmmxxGmresEnvironment,