sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

renamed 'sound power' to 'sound value iteration'

tempestpy_adaptions
TimQu 7 years ago
parent
a24de86ce1
commit
be6d4f9854
7 changed files with 22 additions and 22 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm/settings/modules/NativeEquationSolverSettings.cpp
  2. 12
      src/storm/solver/NativeLinearEquationSolver.cpp
  3. 2
      src/storm/solver/NativeLinearEquationSolver.h
  4. 4
      src/storm/solver/SolverSelectionOptions.cpp
  5. 2
      src/storm/solver/SolverSelectionOptions.h
  6. 10
      src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
  7. 6
      src/test/storm/solver/LinearEquationSolverTest.cpp

8
src/storm/settings/modules/NativeEquationSolverSettings.cpp
View File

@ -27,7 +27,7 @@ namespace storm {
const std::string NativeEquationSolverSettings::powerMethodSymmetricUpdatesOptionName = "symmetricupdates";
NativeEquationSolverSettings::NativeEquationSolverSettings() : ModuleSettings(moduleName) {
std::vector<std::string> methods = { "jacobi", "gaussseidel", "sor", "walkerchae", "power", "soundpower", "interval-iteration", "ratsearch" };
std::vector<std::string> 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;

12
src/storm/solver/NativeLinearEquationSolver.cpp
View File

@ -566,7 +566,7 @@ namespace storm {
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundPower(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> 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<typename ValueType>
LinearEquationSolverProblemFormat NativeLinearEquationSolver<ValueType>::getEquationProblemFormat(Environment const& env) const {
auto method = getMethod(env, storm::NumberTraits<ValueType>::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;

2
src/storm/solver/NativeLinearEquationSolver.h
View File

@ -64,7 +64,7 @@ namespace storm {
virtual bool solveEquationsJacobi(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsWalkerChae(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsPower(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsSoundPower(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsSoundValueIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsIntervalIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual bool solveEquationsRationalSearch(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;

4
src/storm/solver/SolverSelectionOptions.cpp
View File

@ -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:

2
src/storm/solver/SolverSelectionOptions.h
View File

@ -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)

10
src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp
View File

@ -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<storm::RationalNumber>(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,

6
src/test/storm/solver/LinearEquationSolverTest.cpp
View File

@ -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<storm::RationalNumber, std::string>("1e-6"));
return env;
@ -293,7 +293,7 @@ namespace {
typedef ::testing::Types<
NativeDoublePowerEnvironment,
NativeDoubleSoundPowerEnvironment,
NativeDoubleSoundValueIterationEnvironment,
NativeDoubleIntervalIterationEnvironment,
NativeDoubleJacobiEnvironment,
NativeDoubleGaussSeidelEnvironment,

Write Preview
Loading…
Cancel
Save