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

disabled iterative lin eq. solver restarts as this does not significantly improve the runtimes

tempestpy_adaptions
TimQu 8 years ago
parent
8c58008acf
commit
44cd4376a0
3 changed files with 3 additions and 103 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. 45
      src/storm/solver/GameSolver.cpp
  2. 59
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  3. 2
      src/storm/solver/StandardMinMaxLinearEquationSolver.h

45
src/storm/solver/GameSolver.cpp
View File

@ -56,49 +56,8 @@ namespace storm {
submatrixSolver->setCachingEnabled(true);
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
ValueType linEqPrecision = this->getPrecision();
uint_fast64_t hintIterations = 0;
std::vector<ValueType> otherTmpResult(tmpResult.size());
bool vectorsNotEqual = false;
do {
vectorsNotEqual = false;
// Set the precision of the underlying solver
auto* gmmSolver = dynamic_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(submatrixSolver.get());
auto* nativeSolver = dynamic_cast<storm::solver::NativeLinearEquationSolver<ValueType>*>(submatrixSolver.get());
auto* eigenSolver = dynamic_cast<storm::solver::EigenLinearEquationSolver<ValueType>*>(submatrixSolver.get());
auto* eliminationSolver = dynamic_cast<storm::solver::EliminationLinearEquationSolver<ValueType>*>(submatrixSolver.get());
if (gmmSolver) {
auto newSettings = gmmSolver->getSettings();
newSettings.setPrecision(linEqPrecision);
gmmSolver->setSettings(newSettings);
} else if (nativeSolver) {
auto newSettings = nativeSolver->getSettings();
newSettings.setPrecision(linEqPrecision);
nativeSolver->setSettings(newSettings);
} else if (eigenSolver) {
eigenSolver->getSettings().setPrecision(linEqPrecision);
} else if (eliminationSolver) {
// elimination solver does not consider a precision so nothing to do
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Changing the precision for the given linear equation solver type is not implemented");
}
// invoke the solver
submatrixSolver->solveEquations(x, tmpResult);
submatrixSolver->multiply(x, nullptr, otherTmpResult);
linEqPrecision *= storm::utility::convertNumber<ValueType>(0.5);
++hintIterations;
auto otherTmpResIt = otherTmpResult.begin();
auto xIt = x.begin();
for(auto tmpResIt = tmpResult.begin(); tmpResIt != tmpResult.end(); ++tmpResIt) {
if (!storm::utility::vector::equalModuloPrecision(*tmpResIt + *xIt, *otherTmpResIt + *xIt, this->getPrecision(), this->getRelative())) {
vectorsNotEqual = true;
break;
}
++otherTmpResIt; ++xIt;
}
} while (vectorsNotEqual);
STORM_LOG_WARN_COND(hintIterations == 1, "required " << hintIterations << " linear equation solver invokations to apply the scheduler hints in GameSolver");
// invoke the solver
submatrixSolver->solveEquations(x, tmpResult);
}
// Now perform the actual value iteration.

59
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -113,7 +113,6 @@ namespace storm {
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
auto solver = linearEquationSolverFactory->create(std::move(submatrix));
setPrecisionRelativeOfLinearEquationSolver(solver, this->getPrecision(), this->getRelative());
if (this->lowerBound) {
solver->setLowerBound(this->lowerBound.get());
}
@ -244,31 +243,7 @@ namespace storm {
submatrixSolver->setCachingEnabled(true);
if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); }
if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); }
ValueType linEqPrecision = this->getPrecision();
// Temporarily shrink the auxiliary row vector
auxiliaryRowVector->resize(A.getRowGroupCount());
auxiliaryRowVector->reserve(A.getRowCount());
uint_fast64_t hintIterations = 0;
bool vectorsNotEqual = false;
do {
vectorsNotEqual = false;
setPrecisionRelativeOfLinearEquationSolver(submatrixSolver, linEqPrecision, this->getRelative());
submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
submatrixSolver->multiply(x, nullptr, *auxiliaryRowVector);
linEqPrecision *= storm::utility::convertNumber<ValueType>(0.5);
++hintIterations;
auto otherTmpResIt = auxiliaryRowVector->begin();
auto xIt = x.begin();
for(auto tmpResIt = auxiliaryRowGroupVector->begin(); tmpResIt != auxiliaryRowGroupVector->end(); ++tmpResIt) {
if (!storm::utility::vector::equalModuloPrecision(*tmpResIt + *xIt, *otherTmpResIt + *xIt, this->getPrecision(), this->getRelative())) {
vectorsNotEqual = true;
break;
}
++otherTmpResIt; ++xIt;
}
} while (vectorsNotEqual);
STORM_LOG_WARN_COND(hintIterations == 1, "required " << hintIterations << " linear equation solver invokations to apply the scheduler hint");
auxiliaryRowVector->resize(A.getRowCount());
submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
}
std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
@ -377,38 +352,6 @@ namespace storm {
}
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, ValueType precision, bool relative) const {
auto* gmmSolver = dynamic_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(linEqSolver.get());
auto* nativeSolver = dynamic_cast<storm::solver::NativeLinearEquationSolver<ValueType>*>(linEqSolver.get());
auto* eigenSolver = dynamic_cast<storm::solver::EigenLinearEquationSolver<ValueType>*>(linEqSolver.get());
auto* eliminationSolver = dynamic_cast<storm::solver::EliminationLinearEquationSolver<ValueType>*>(linEqSolver.get());
if (gmmSolver) {
auto newSettings = gmmSolver->getSettings();
newSettings.setPrecision(precision);
newSettings.setRelativeTerminationCriterion(relative);
gmmSolver->setSettings(newSettings);
} else if (nativeSolver) {
auto newSettings = nativeSolver->getSettings();
newSettings.setPrecision(precision);
newSettings.setRelativeTerminationCriterion(relative);
nativeSolver->setSettings(newSettings);
} else if (eigenSolver) {
eigenSolver->getSettings().setPrecision(precision);
// no relative flag for eigen solver
} else if (eliminationSolver) {
// elimination solver does not consider a precision so nothing to do
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Changing the precision for the given linear equation solver type is not implemented");
}
}
template<>
void StandardMinMaxLinearEquationSolver<storm::RationalNumber>::setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalNumber>>& linEqSolver, storm::RationalNumber precision, bool relative) const {
// Intentionally left empty
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverSettings<ValueType> const& StandardMinMaxLinearEquationSolver<ValueType>::getSettings() const {
return settings;

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

@ -66,8 +66,6 @@ namespace storm {
Status updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations) const;
void reportStatus(Status status, uint64_t iterations) const;
void setPrecisionRelativeOfLinearEquationSolver(std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, ValueType precision, bool relative) const;
/// The settings of this solver.
StandardMinMaxLinearEquationSolverSettings<ValueType> settings;

Write Preview
Loading…
Cancel
Save