From be6d4f98541ce2a890ac5eada802e4a076f00984 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 13 Mar 2018 13:46:50 +0100 Subject: [PATCH] renamed 'sound power' to 'sound value iteration' --- .../modules/NativeEquationSolverSettings.cpp | 8 ++++---- src/storm/solver/NativeLinearEquationSolver.cpp | 12 ++++++------ src/storm/solver/NativeLinearEquationSolver.h | 2 +- src/storm/solver/SolverSelectionOptions.cpp | 4 ++-- src/storm/solver/SolverSelectionOptions.h | 2 +- .../storm/modelchecker/DtmcPrctlModelCheckerTest.cpp | 10 +++++----- src/test/storm/solver/LinearEquationSolverTest.cpp | 6 +++--- 7 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/storm/settings/modules/NativeEquationSolverSettings.cpp b/src/storm/settings/modules/NativeEquationSolverSettings.cpp index 123298b2c..a73d64bc2 100644 --- a/src/storm/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/storm/settings/modules/NativeEquationSolverSettings.cpp @@ -27,7 +27,7 @@ namespace storm { const std::string NativeEquationSolverSettings::powerMethodSymmetricUpdatesOptionName = "symmetricupdates"; NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) { - std::vector methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "soundpower", "interval-iteration", "ratsearch" }; + std::vector methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "sound-value-iteration", "svi", "interval-iteration", "ii", "ratsearch" }; this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The method to be used for solving linear equation systems with the native engine.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(methods)).setDefaultValueString("jacobi").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, maximalIterationsOptionName, false, "The maximal number of iterations to perform before iterative solving is aborted.").setShortName(maximalIterationsOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The maximal iteration count.").setDefaultValueUnsignedInteger(20000).build()).build()); @@ -67,9 +67,9 @@ 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") { + } else if (linearEquationSystemTechniqueAsString == "sound-value-iteration" || linearEquationSystemTechniqueAsString == "svi") { + return storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration; + } else if (linearEquationSystemTechniqueAsString == "interval-iteration" || linearEquationSystemTechniqueAsString == "ii") { return storm::solver::NativeLinearEquationSolverMethod::IntervalIteration; } else if (linearEquationSystemTechniqueAsString == "ratsearch") { return storm::solver::NativeLinearEquationSolverMethod::RationalSearch; diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index dd67522a1..e7d1cf5e5 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -566,7 +566,7 @@ namespace storm { template - bool NativeLinearEquationSolver::solveEquationsSoundPower(Environment const& env, std::vector& x, std::vector const& b) const { + bool NativeLinearEquationSolver::solveEquationsSoundValueIteration(Environment const& env, std::vector& x, std::vector const& b) const { // Prepare the solution vectors. assert(x.size() == this->A->getRowCount()); @@ -906,9 +906,9 @@ namespace storm { } else { STORM_LOG_WARN("The selected solution method does not guarantee exact results."); } - } else if (env.solver().isForceSoundness() && method != NativeLinearEquationSolverMethod::SoundPower && method != NativeLinearEquationSolverMethod::IntervalIteration && method != NativeLinearEquationSolverMethod::RationalSearch) { + } else if (env.solver().isForceSoundness() && method != NativeLinearEquationSolverMethod::SoundValueIteration && method != NativeLinearEquationSolverMethod::IntervalIteration && method != NativeLinearEquationSolverMethod::RationalSearch) { if (env.solver().native().isMethodSetFromDefault()) { - method = NativeLinearEquationSolverMethod::SoundPower; + method = NativeLinearEquationSolverMethod::SoundValueIteration; 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."); @@ -931,8 +931,8 @@ namespace storm { return this->solveEquationsWalkerChae(env, x, b); case NativeLinearEquationSolverMethod::Power: return this->solveEquationsPower(env, x, b); - case NativeLinearEquationSolverMethod::SoundPower: - return this->solveEquationsSoundPower(env, x, b); + case NativeLinearEquationSolverMethod::SoundValueIteration: + return this->solveEquationsSoundValueIteration(env, x, b); case NativeLinearEquationSolverMethod::IntervalIteration: return this->solveEquationsIntervalIteration(env, x, b); case NativeLinearEquationSolverMethod::RationalSearch: @@ -945,7 +945,7 @@ namespace storm { template LinearEquationSolverProblemFormat NativeLinearEquationSolver::getEquationProblemFormat(Environment const& env) const { auto method = getMethod(env, storm::NumberTraits::IsExact); - if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundPower || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::IntervalIteration) { + if (method == NativeLinearEquationSolverMethod::Power || method == NativeLinearEquationSolverMethod::SoundValueIteration || method == NativeLinearEquationSolverMethod::RationalSearch || method == NativeLinearEquationSolverMethod::IntervalIteration) { return LinearEquationSolverProblemFormat::FixedPointSystem; } else { return LinearEquationSolverProblemFormat::EquationSystem; diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index 46ba3628e..6622de17f 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -64,7 +64,7 @@ namespace storm { virtual bool solveEquationsJacobi(storm::Environment const& env, std::vector& x, std::vector const& b) const; 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 solveEquationsSoundValueIteration(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; diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index d2148e9bc..d50d4875f 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -94,8 +94,8 @@ namespace storm { return "WalkerChae"; case NativeLinearEquationSolverMethod::Power: return "Power"; - case NativeLinearEquationSolverMethod::SoundPower: - return "SoundPower"; + case NativeLinearEquationSolverMethod::SoundValueIteration: + return "SoundValueIteration"; case NativeLinearEquationSolverMethod::IntervalIteration: return "IntervalIteration"; case NativeLinearEquationSolverMethod::RationalSearch: diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 678bc1565..baea29dc1 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -15,7 +15,7 @@ namespace storm { ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological) ExtendEnumsWithSelectionField(SmtSolverType, Z3, Mathsat) - ExtendEnumsWithSelectionField(NativeLinearEquationSolverMethod, Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundPower, IntervalIteration, RationalSearch) + ExtendEnumsWithSelectionField(NativeLinearEquationSolverMethod, Jacobi, GaussSeidel, SOR, WalkerChae, Power, SoundValueIteration, 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 4ba411f18..ad6654ff4 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -206,7 +206,7 @@ namespace { } }; - class SparseNativeSoundPowerEnvironment { + class SparseNativeSoundValueIterationEnvironment { 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; @@ -217,7 +217,7 @@ namespace { storm::Environment env; env.solver().setForceSoundness(true); env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundPower); + env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration); env.solver().native().setPrecision(storm::utility::convertNumber(1e-6)); return env; } @@ -304,7 +304,7 @@ namespace { } }; - class HybridCuddNativeSoundPowerEnvironment { + class HybridCuddNativeSoundValueIterationEnvironment { public: static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Hybrid; @@ -481,13 +481,13 @@ namespace { SparseNativeWalkerChaeEnvironment, SparseNativeSorEnvironment, SparseNativePowerEnvironment, - SparseNativeSoundPowerEnvironment, + SparseNativeSoundValueIterationEnvironment, SparseNativeIntervalIterationEnvironment, SparseNativeRationalSearchEnvironment, SparseTopologicalEigenLUEnvironment, HybridSylvanGmmxxGmresEnvironment, HybridCuddNativeJacobiEnvironment, - HybridCuddNativeSoundPowerEnvironment, + HybridCuddNativeSoundValueIterationEnvironment, HybridSylvanNativeRationalSearchEnvironment, DdSylvanNativePowerEnvironment, DdCuddNativeJacobiEnvironment, diff --git a/src/test/storm/solver/LinearEquationSolverTest.cpp b/src/test/storm/solver/LinearEquationSolverTest.cpp index 3b5386c1f..f96f88e5d 100644 --- a/src/test/storm/solver/LinearEquationSolverTest.cpp +++ b/src/test/storm/solver/LinearEquationSolverTest.cpp @@ -24,7 +24,7 @@ namespace { } }; - class NativeDoubleSoundPowerEnvironment { + class NativeDoubleSoundValueIterationEnvironment { public: typedef double ValueType; static const bool isExact = false; @@ -32,7 +32,7 @@ namespace { storm::Environment env; env.solver().setForceSoundness(true); env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native); - env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundPower); + env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration); env.solver().native().setRelativeTerminationCriterion(false); env.solver().native().setPrecision(storm::utility::convertNumber("1e-6")); return env; @@ -293,7 +293,7 @@ namespace { typedef ::testing::Types< NativeDoublePowerEnvironment, - NativeDoubleSoundPowerEnvironment, + NativeDoubleSoundValueIterationEnvironment, NativeDoubleIntervalIterationEnvironment, NativeDoubleJacobiEnvironment, NativeDoubleGaussSeidelEnvironment,