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

Renamed 'sound power' to interval iteration and 'quick sound power' to 'sound power'

tempestpy_adaptions
TimQu 7 years ago
parent
ea25c8fd2e
commit
a6c6118733
6 changed files with 29 additions and 33 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. 6
      src/storm/settings/modules/NativeEquationSolverSettings.cpp
  2. 36
      src/storm/solver/NativeLinearEquationSolver.cpp
  3. 2
      src/storm/solver/NativeLinearEquationSolver.h
  4. 8
      src/storm/solver/SolverSelectionOptions.cpp
  5. 2
      src/storm/solver/SolverSelectionOptions.h
  6. 8
      src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp

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

@ -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.");
}

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

@ -396,10 +396,10 @@ 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>::solveEquationsIntervalIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> 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<ValueType>* lowerX = &x;
this->createLowerBoundsVector(*lowerX);
@ -557,8 +557,8 @@ namespace storm {
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquationsQuickSoundPower(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (QuickPower)");
bool NativeLinearEquationSolver<ValueType>::solveEquationsSoundPower(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> 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<typename ValueType>
LinearEquationSolverProblemFormat NativeLinearEquationSolver<ValueType>::getEquationProblemFormat(Environment const& env) const {
auto method = getMethod(env, storm::NumberTraits<ValueType>::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<ValueType>::IsExact);
if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) {
if (method == NativeLinearEquationSolverMethod::IntervalIteration) {
requirements.requireBounds();
} else if (method == NativeLinearEquationSolverMethod::RationalSearch) {
requirements.requireLowerBounds();

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

@ -72,7 +72,7 @@ namespace storm {
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 solveEquationsQuickSoundPower(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;
template<typename RationalType, typename ImpreciseType>

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

@ -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";
}

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

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

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

@ -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<storm::RationalNumber>(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<storm::RationalNumber>(1e-6));
return env;
@ -482,7 +482,7 @@ namespace {
SparseNativeSorEnvironment,
SparseNativePowerEnvironment,
SparseNativeSoundPowerEnvironment,
SparseNativeQuickSoundPowerEnvironment,
SparseNativeIntervalIterationEnvironment,
SparseNativeRationalSearchEnvironment,
SparseTopologicalEigenLUEnvironment,
HybridSylvanGmmxxGmresEnvironment,

Write Preview
Loading…
Cancel
Save