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

refactored auxData in linear equation solvers 

Former-commit-id: 9e0deb255c
main
TimQu 9 years ago
parent
965d5b5e75
commit
48b82e7b14
13 changed files with 198 additions and 332 deletions
Unified View
  1. 1
      src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  2. 1
      src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  3. 141
      src/solver/GmmxxLinearEquationSolver.cpp
  4. 24
      src/solver/GmmxxLinearEquationSolver.h
  5. 58
      src/solver/LinearEquationSolver.cpp
  6. 41
      src/solver/LinearEquationSolver.h
  7. 2
      src/solver/MinMaxLinearEquationSolver.h
  8. 106
      src/solver/NativeLinearEquationSolver.cpp
  9. 14
      src/solver/NativeLinearEquationSolver.h
  10. 50
      src/solver/StandardMinMaxLinearEquationSolver.cpp
  11. 10
      src/solver/StandardMinMaxLinearEquationSolver.h
  12. 4
      src/utility/policyguessing.cpp
  13. 78
      test/functional/solver/GmmxxLinearEquationSolverTest.cpp

1
src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -629,7 +629,6 @@ namespace storm {
} }
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(uniformizedMatrix)); std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(uniformizedMatrix));
solver->allocateAuxMemory(storm::solver::LinearEquationSolverOperation::MultiplyRepeatedly);
if (!useMixedPoissonProbabilities && std::get<0>(foxGlynnResult) > 1) { if (!useMixedPoissonProbabilities && std::get<0>(foxGlynnResult) > 1) {
// Perform the matrix-vector multiplications (without adding). // Perform the matrix-vector multiplications (without adding).

1
src/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
View File

@ -365,7 +365,6 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true);
linEqMatrix.convertToEquationSystem(); linEqMatrix.convertToEquationSystem();
linEq.solver = linEq.factory.create(std::move(linEqMatrix)); linEq.solver = linEq.factory.create(std::move(linEqMatrix));
linEq.solver->allocateAuxMemory(storm::solver::LinearEquationSolverOperation::SolveEquations);
} }
// Get the results for the individual objectives. // Get the results for the individual objectives.

141
src/solver/GmmxxLinearEquationSolver.cpp
View File

@ -111,12 +111,12 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), gmmxxMatrix(nullptr), settings(settings), auxiliaryJacobiMemory(nullptr) { GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings) {
this->setMatrix(A); this->setMatrix(A);
} }
template<typename ValueType> template<typename ValueType>
GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), gmmxxMatrix(nullptr), settings(settings), auxiliaryJacobiMemory(nullptr) { GmmxxLinearEquationSolver<ValueType>::GmmxxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, GmmxxLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings) {
this->setMatrix(std::move(A)); this->setMatrix(std::move(A));
} }
@ -124,66 +124,79 @@ namespace storm {
void GmmxxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& A) { void GmmxxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& A) {
localA.reset(); localA.reset();
this->A = &A; this->A = &A;
gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(A); resetAuxiliaryData();
jacobiDecomposition.reset();
} }
template<typename ValueType> template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& A) { void GmmxxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& A) {
localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A)); localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A));
this->A = localA.get(); this->A = localA.get();
gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(*localA); resetAuxiliaryData();
} }
template<typename ValueType> template<typename ValueType>
bool GmmxxLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const { bool GmmxxLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
auto method = this->getSettings().getSolutionMethod(); auto method = this->getSettings().getSolutionMethod();
auto preconditioner = this->getSettings().getPreconditioner(); auto preconditioner = this->getSettings().getPreconditioner();
STORM_LOG_INFO("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations)."); STORM_LOG_DEBUG("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations).");
if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi && preconditioner != GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) { if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi && preconditioner != GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) {
STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored."); STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored.");
} }
if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Bicgstab || method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Qmr || method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Gmres) { if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Bicgstab || method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Qmr || method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Gmres) {
// Translate the matrix into gmm++ format (if not already done)
if(!gmmxxA) {
gmmxxA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(*A);
}
// Make sure that the requested preconditioner is available
if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu && !iluPreconditioner) {
iluPreconditioner = std::make_unique<gmm::ilu_precond<gmm::csr_matrix<ValueType>>>(*gmmxxA);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) {
diagonalPreconditioner = std::make_unique<gmm::diagonal_precond<gmm::csr_matrix<ValueType>>>(*gmmxxA);
}
// Prepare an iteration object that determines the accuracy and the maximum number of iterations. // Prepare an iteration object that determines the accuracy and the maximum number of iterations.
gmm::iteration iter(this->getSettings().getPrecision(), 0, this->getSettings().getMaximalNumberOfIterations()); gmm::iteration iter(this->getSettings().getPrecision(), 0, this->getSettings().getMaximalNumberOfIterations());
// Invoke gmm with the corresponding settings
if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Bicgstab) { if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Bicgstab) {
if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) { if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) {
gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmxxMatrix), iter); gmm::bicgstab(*gmmxxA, x, b, *iluPreconditioner, iter);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) { } else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) {
gmm::bicgstab(*gmmxxMatrix, x, b, gmm::diagonal_precond<gmm::csr_matrix<ValueType>>(*gmmxxMatrix), iter); gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) { } else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) {
gmm::bicgstab(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); gmm::bicgstab(*gmmxxA, x, b, gmm::identity_matrix(), iter);
} }
} else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Qmr) { } else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Qmr) {
if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) { if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) {
gmm::qmr(*gmmxxMatrix, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmxxMatrix), iter); gmm::qmr(*gmmxxA, x, b, *iluPreconditioner, iter);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) { } else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) {
gmm::qmr(*gmmxxMatrix, x, b, gmm::diagonal_precond<gmm::csr_matrix<ValueType>>(*gmmxxMatrix), iter); gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) { } else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) {
gmm::qmr(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); gmm::qmr(*gmmxxA, x, b, gmm::identity_matrix(), iter);
} }
} else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Gmres) { } else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Gmres) {
if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) { if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Ilu) {
gmm::gmres(*gmmxxMatrix, x, b, gmm::ilu_precond<gmm::csr_matrix<ValueType>>(*gmmxxMatrix), this->getSettings().getNumberOfIterationsUntilRestart(), iter); gmm::gmres(*gmmxxA, x, b, *iluPreconditioner, this->getSettings().getNumberOfIterationsUntilRestart(), iter);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) { } else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::Diagonal) {
gmm::gmres(*gmmxxMatrix, x, b, gmm::diagonal_precond<gmm::csr_matrix<ValueType>>(*gmmxxMatrix), this->getSettings().getNumberOfIterationsUntilRestart(), iter); gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, this->getSettings().getNumberOfIterationsUntilRestart(), iter);
} else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) { } else if (preconditioner == GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) {
gmm::gmres(*gmmxxMatrix, x, b, gmm::identity_matrix(), this->getSettings().getNumberOfIterationsUntilRestart(), iter); gmm::gmres(*gmmxxA, x, b, gmm::identity_matrix(), this->getSettings().getNumberOfIterationsUntilRestart(), iter);
} }
} }
// Check if the solver converged and issue a warning otherwise. // Check if the solver converged and issue a warning otherwise.
if (iter.converged()) { if (iter.converged()) {
STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations."); STORM_LOG_DEBUG("Iterative solver converged after " << iter.get_iteration() << " iterations.");
return true; return true;
} else { } else {
STORM_LOG_WARN("Iterative solver did not converge."); STORM_LOG_WARN("Iterative solver did not converge.");
return false; return false;
} }
} else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi) { } else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi) {
uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(*A, x, b); uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(x, b);
// Check if the solver converged and issue a warning otherwise. // Check if the solver converged and issue a warning otherwise.
if (iterations < this->getSettings().getMaximalNumberOfIterations()) { if (iterations < this->getSettings().getMaximalNumberOfIterations()) {
@ -200,39 +213,44 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const { void GmmxxLinearEquationSolver<ValueType>::multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
if(!gmmxxA) {
gmmxxA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(*A);
}
if (b) { if (b) {
gmm::mult_add(*gmmxxMatrix, x, *b, result); gmm::mult_add(*gmmxxA, x, *b, result);
} else { } else {
gmm::mult(*gmmxxMatrix, x, result); gmm::mult(*gmmxxA, x, result);
} }
} }
template<typename ValueType> template<typename ValueType>
uint_fast64_t GmmxxLinearEquationSolver<ValueType>::solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b) const { uint_fast64_t GmmxxLinearEquationSolver<ValueType>::solveLinearEquationSystemWithJacobi(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool allocatedAuxMemory = !this->hasAuxMemory(LinearEquationSolverOperation::SolveEquations);
if (allocatedAuxMemory) {
this->allocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
}
// Get a Jacobi decomposition of the matrix A (if not already available). // Get a Jacobi decomposition of the matrix A (if not already available).
if(jacobiDecomposition == nullptr) { if(!jacobiDecomposition) {
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> nativeJacobiDecomposition = A.getJacobiDecomposition(); std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> nativeJacobiDecomposition = A->getJacobiDecomposition();
// Convert the LU matrix to gmm++'s format. // Convert the LU matrix to gmm++'s format.
jacobiDecomposition = std::make_unique<std::pair<gmm::csr_matrix<ValueType>, std::vector<ValueType>>>(*storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(std::move(nativeJacobiDecomposition.first)), jacobiDecomposition = std::make_unique<std::pair<gmm::csr_matrix<ValueType>, std::vector<ValueType>>>(*storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<ValueType>(std::move(nativeJacobiDecomposition.first)),
std::move(nativeJacobiDecomposition.second)); std::move(nativeJacobiDecomposition.second));
} }
gmm::csr_matrix<ValueType> const& jacobiLU = jacobiDecomposition->first;
std::vector<ValueType> const& jacobiD = jacobiDecomposition->second;
std::vector<ValueType>* currentX = &x; std::vector<ValueType>* currentX = &x;
std::vector<ValueType>* nextX = auxiliaryJacobiMemory.get(); if(!this->auxiliaryRowVector) {
this->auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
}
std::vector<ValueType>* nextX = this->auxiliaryRowVector.get();
// Set up additional environment variables. // Set up additional environment variables.
uint_fast64_t iterationCount = 0; uint_fast64_t iterationCount = 0;
bool converged = false; bool converged = false;
while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
// Compute D^-1 * (b - LU * x) and store result in nextX. // Compute D^-1 * (b - LU * x) and store result in nextX.
gmm::mult_add(jacobiDecomposition->first, gmm::scaled(*currentX, -storm::utility::one<ValueType>()), b, *nextX); gmm::mult_add(jacobiLU, gmm::scaled(*currentX, -storm::utility::one<ValueType>()), b, *nextX);
storm::utility::vector::multiplyVectorsPointwise(jacobiDecomposition->second, *nextX, *nextX); storm::utility::vector::multiplyVectorsPointwise(jacobiD, *nextX, *nextX);
// Now check if the process already converged within our precision. // Now check if the process already converged within our precision.
converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion()); converged = storm::utility::vector::equalModuloPrecision(*currentX, *nextX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion());
@ -246,21 +264,16 @@ namespace storm {
// If the last iteration did not write to the original x we have to swap the contents, because the // If the last iteration did not write to the original x we have to swap the contents, because the
// output has to be written to the input parameter x. // output has to be written to the input parameter x.
if (currentX == auxiliaryJacobiMemory.get()) { if (currentX == this->auxiliaryRowVector.get()) {
std::swap(x, *currentX); std::swap(x, *currentX);
} }
// If we allocated auxiliary memory, we need to dispose of it now.
if (allocatedAuxMemory) {
this->deallocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
}
return iterationCount; return iterationCount;
} }
template<typename ValueType> template<typename ValueType>
GmmxxLinearEquationSolverSettings<ValueType>& GmmxxLinearEquationSolver<ValueType>::getSettings() { void GmmxxLinearEquationSolver<ValueType>::setSettings(GmmxxLinearEquationSolverSettings<ValueType> const& newSettings) {
return settings; settings = newSettings;
} }
template<typename ValueType> template<typename ValueType>
@ -269,54 +282,12 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
bool GmmxxLinearEquationSolver<ValueType>::allocateAuxMemory(LinearEquationSolverOperation operation) const { void GmmxxLinearEquationSolver<ValueType>::resetAuxiliaryData() const {
bool result = false; gmmxxA.reset();
if (operation == LinearEquationSolverOperation::SolveEquations) { iluPreconditioner.reset();
if (this->getSettings().getSolutionMethod() == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi) { diagonalPreconditioner.reset();
if (!auxiliaryJacobiMemory) { jacobiDecomposition.reset();
auxiliaryJacobiMemory = std::make_unique<std::vector<ValueType>>(this->getMatrixRowCount()); LinearEquationSolver<ValueType>::resetAuxiliaryData();
result = true;
}
}
}
result |= LinearEquationSolver<ValueType>::allocateAuxMemory(operation);
return result;
}
template<typename ValueType>
bool GmmxxLinearEquationSolver<ValueType>::deallocateAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::SolveEquations) {
if (auxiliaryJacobiMemory) {
result = true;
auxiliaryJacobiMemory.reset();
}
}
result |= LinearEquationSolver<ValueType>::deallocateAuxMemory(operation);
return result;
}
template<typename ValueType>
bool GmmxxLinearEquationSolver<ValueType>::reallocateAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::SolveEquations) {
if (auxiliaryJacobiMemory) {
result = auxiliaryJacobiMemory->size() != this->getMatrixColumnCount();
auxiliaryJacobiMemory->resize(this->getMatrixRowCount());
}
}
result |= LinearEquationSolver<ValueType>::reallocateAuxMemory(operation);
return result;
}
template<typename ValueType>
bool GmmxxLinearEquationSolver<ValueType>::hasAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::SolveEquations) {
result |= static_cast<bool>(auxiliaryJacobiMemory);
}
result |= LinearEquationSolver<ValueType>::hasAuxMemory(operation);
return result;
} }
template<typename ValueType> template<typename ValueType>

24
src/solver/GmmxxLinearEquationSolver.h
View File

@ -95,29 +95,26 @@ namespace storm {
virtual bool solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override; virtual bool solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override; virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
GmmxxLinearEquationSolverSettings<ValueType>& getSettings(); void setSettings(GmmxxLinearEquationSolverSettings<ValueType> const& newSettings);
GmmxxLinearEquationSolverSettings<ValueType> const& getSettings() const; GmmxxLinearEquationSolverSettings<ValueType> const& getSettings() const;
virtual bool allocateAuxMemory(LinearEquationSolverOperation operation) const override; /*
virtual bool deallocateAuxMemory(LinearEquationSolverOperation operation) const override; * Clears auxiliary data that has possibly been stored during previous calls of the solver.
virtual bool reallocateAuxMemory(LinearEquationSolverOperation operation) const override; */
virtual bool hasAuxMemory(LinearEquationSolverOperation operation) const override; virtual void resetAuxiliaryData() const override;
private: private:
/*! /*!
* Solves the linear equation system A*x = b given by the parameters using the Jacobi method. * Solves the linear equation system A*x = b given by the parameters using the Jacobi method.
* *
* @param A The matrix specifying the coefficients of the linear equations.
* @param x The solution vector x. The initial values of x represent a guess of the real values to the * @param x The solution vector x. The initial values of x represent a guess of the real values to the
* solver, but may be set to zero. * solver, but may be set to zero.
* @param b The right-hand side of the equation system. * @param b The right-hand side of the equation system.
* @return The number of iterations needed until convergence if the solver converged and * @return The number of iterations needed until convergence if the solver converged and
* maximalNumberOfIteration otherwise. * maximalNumberOfIteration otherwise.
* @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the number of rows of A.
*/ */
uint_fast64_t solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix<ValueType> const& A, std::vector<ValueType>& x, std::vector<ValueType> const& b) const; uint_fast64_t solveLinearEquationSystemWithJacobi(std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
virtual uint64_t getMatrixRowCount() const override; virtual uint64_t getMatrixRowCount() const override;
virtual uint64_t getMatrixColumnCount() const override; virtual uint64_t getMatrixColumnCount() const override;
@ -130,14 +127,13 @@ namespace storm {
// the pointer refers to localA. // the pointer refers to localA.
storm::storage::SparseMatrix<ValueType> const* A; storm::storage::SparseMatrix<ValueType> const* A;
// The (gmm++) matrix associated with this equation solver.
std::unique_ptr<gmm::csr_matrix<ValueType>> gmmxxMatrix;
// The settings used by the solver. // The settings used by the solver.
GmmxxLinearEquationSolverSettings<ValueType> settings; GmmxxLinearEquationSolverSettings<ValueType> settings;
// Auxiliary storage for the Jacobi method. // Auxiliary data obtained during solving
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryJacobiMemory; mutable std::unique_ptr<gmm::csr_matrix<ValueType>> gmmxxA;
mutable std::unique_ptr<gmm::ilu_precond<gmm::csr_matrix<ValueType>>> iluPreconditioner;
mutable std::unique_ptr<gmm::diagonal_precond<gmm::csr_matrix<ValueType>>> diagonalPreconditioner;
mutable std::unique_ptr<std::pair<gmm::csr_matrix<ValueType>, std::vector<ValueType>>> jacobiDecomposition; mutable std::unique_ptr<std::pair<gmm::csr_matrix<ValueType>, std::vector<ValueType>>> jacobiDecomposition;
}; };

58
src/solver/LinearEquationSolver.cpp
View File

@ -14,21 +14,21 @@ namespace storm {
namespace solver { namespace solver {
template<typename ValueType> template<typename ValueType>
LinearEquationSolver<ValueType>::LinearEquationSolver() : auxiliaryRepeatedMultiplyMemory(nullptr) { LinearEquationSolver<ValueType>::LinearEquationSolver() {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename ValueType> template<typename ValueType>
void LinearEquationSolver<ValueType>::repeatedMultiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const { void LinearEquationSolver<ValueType>::repeatedMultiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
bool allocatedAuxMemory = !this->hasAuxMemory(LinearEquationSolverOperation::MultiplyRepeatedly); if(!auxiliaryRowVector) {
if (allocatedAuxMemory) { auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
this->allocateAuxMemory(LinearEquationSolverOperation::MultiplyRepeatedly);
} }
// Set up some temporary variables so that we can just swap pointers instead of copying the result after // Set up some temporary variables so that we can just swap pointers instead of copying the result after
// each iteration. // each iteration.
std::vector<ValueType>* currentX = &x; std::vector<ValueType>* currentX = &x;
std::vector<ValueType>* nextX = auxiliaryRepeatedMultiplyMemory.get(); std::vector<ValueType>* nextX = auxiliaryRowVector.get();
// Now perform matrix-vector multiplication as long as we meet the bound. // Now perform matrix-vector multiplication as long as we meet the bound.
for (uint_fast64_t i = 0; i < n; ++i) { for (uint_fast64_t i = 0; i < n; ++i) {
@ -38,56 +38,16 @@ namespace storm {
// If we performed an odd number of repetitions, we need to swap the contents of currentVector and x, // If we performed an odd number of repetitions, we need to swap the contents of currentVector and x,
// because the output is supposed to be stored in the input vector x. // because the output is supposed to be stored in the input vector x.
if (currentX == auxiliaryRepeatedMultiplyMemory.get()) { if (currentX == auxiliaryRowVector.get()) {
std::swap(x, *currentX); std::swap(x, *currentX);
} }
// If we allocated auxiliary memory, we need to dispose of it now.
if (allocatedAuxMemory) {
this->deallocateAuxMemory(LinearEquationSolverOperation::MultiplyRepeatedly);
}
} }
template<typename ValueType> template<typename ValueType>
bool LinearEquationSolver<ValueType>::allocateAuxMemory(LinearEquationSolverOperation operation) const { void LinearEquationSolver<ValueType>::resetAuxiliaryData() const {
if (!auxiliaryRepeatedMultiplyMemory) { auxiliaryRowVector.reset();
auxiliaryRepeatedMultiplyMemory = std::make_unique<std::vector<ValueType>>(this->getMatrixColumnCount());
return true;
}
return false;
} }
template<typename ValueType>
bool LinearEquationSolver<ValueType>::deallocateAuxMemory(LinearEquationSolverOperation operation) const {
if (operation == LinearEquationSolverOperation::MultiplyRepeatedly) {
if (auxiliaryRepeatedMultiplyMemory) {
auxiliaryRepeatedMultiplyMemory.reset();
return true;
}
}
return false;
}
template<typename ValueType>
bool LinearEquationSolver<ValueType>::reallocateAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::MultiplyRepeatedly) {
if (auxiliaryRepeatedMultiplyMemory) {
result = auxiliaryRepeatedMultiplyMemory->size() != this->getMatrixColumnCount();
auxiliaryRepeatedMultiplyMemory->resize(this->getMatrixColumnCount());
}
}
return result;
}
template<typename ValueType>
bool LinearEquationSolver<ValueType>::hasAuxMemory(LinearEquationSolverOperation operation) const {
if (operation == LinearEquationSolverOperation::MultiplyRepeatedly) {
return static_cast<bool>(auxiliaryRepeatedMultiplyMemory);
}
return false;
}
template<typename ValueType> template<typename ValueType>
std::unique_ptr<LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const { std::unique_ptr<LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return create(matrix); return create(matrix);

41
src/solver/LinearEquationSolver.h
View File

@ -68,40 +68,15 @@ namespace storm {
*/ */
void repeatedMultiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const; void repeatedMultiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const;
// Methods related to allocating/freeing auxiliary storage. /*
* Clears auxiliary data that has possibly been stored during previous calls of the solver.
/*!
* Allocates auxiliary memory that can be used to perform the provided operation. Repeated calls to the
* corresponding function can then be run without allocating/deallocating this memory repeatedly.
* Note: Since the allocated memory is fit to the currently selected options of the solver, they must not
* be changed any more after allocating the auxiliary memory until it is deallocated again.
*
* @return True iff auxiliary memory was allocated.
*/
virtual bool allocateAuxMemory(LinearEquationSolverOperation operation) const;
/*!
* Destroys previously allocated auxiliary memory for the provided operation.
*
* @return True iff auxiliary memory was deallocated.
*/
virtual bool deallocateAuxMemory(LinearEquationSolverOperation operation) const;
/*!
* If the matrix dimensions changed and auxiliary memory was allocated, this function needs to be called to
* update the auxiliary memory.
*
* @return True iff the auxiliary memory was reallocated.
*/
virtual bool reallocateAuxMemory(LinearEquationSolverOperation operation) const;
/*!
* Checks whether the solver has allocated auxiliary memory for the provided operation.
*
* @return True iff auxiliary memory was previously allocated (and not yet deallocated).
*/ */
virtual bool hasAuxMemory(LinearEquationSolverOperation operation) const; virtual void resetAuxiliaryData() const;
protected:
// auxiliary storage. If set, this vector has getMatrixRowCount() entries.
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowVector;
private: private:
/*! /*!
* Retrieves the row count of the matrix associated with this solver. * Retrieves the row count of the matrix associated with this solver.
@ -113,8 +88,6 @@ namespace storm {
*/ */
virtual uint64_t getMatrixColumnCount() const = 0; virtual uint64_t getMatrixColumnCount() const = 0;
// Auxiliary memory for repeated matrix-vector multiplication.
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRepeatedMultiplyMemory;
}; };
template<typename ValueType> template<typename ValueType>

2
src/solver/MinMaxLinearEquationSolver.h
View File

@ -129,7 +129,7 @@ namespace storm {
virtual bool getRelative() const = 0; virtual bool getRelative() const = 0;
/* /*
* Resets the auxiliary data that has been stored during previous calls of this solver * Clears auxiliary data that has possibly been stored during previous calls of the solver.
*/ */
virtual void resetAuxiliaryData() const; virtual void resetAuxiliaryData() const;

106
src/solver/NativeLinearEquationSolver.cpp
View File

@ -84,12 +84,12 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings), auxiliarySolvingMemory(nullptr) { NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, NativeLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings) {
this->setMatrix(A); this->setMatrix(A);
} }
template<typename ValueType> template<typename ValueType>
NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, NativeLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings), auxiliarySolvingMemory(nullptr) { NativeLinearEquationSolver<ValueType>::NativeLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, NativeLinearEquationSolverSettings<ValueType> const& settings) : localA(nullptr), A(nullptr), settings(settings) {
this->setMatrix(std::move(A)); this->setMatrix(std::move(A));
} }
@ -97,20 +97,21 @@ namespace storm {
void NativeLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& A) { void NativeLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& A) {
localA.reset(); localA.reset();
this->A = &A; this->A = &A;
resetAuxiliaryData();
} }
template<typename ValueType> template<typename ValueType>
void NativeLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& A) { void NativeLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& A) {
localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A)); localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A));
this->A = localA.get(); this->A = localA.get();
resetAuxiliaryData();
} }
template<typename ValueType> template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const { bool NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
bool allocatedAuxStorage = !this->hasAuxMemory(LinearEquationSolverOperation::SolveEquations); if(!this->auxiliaryRowVector) {
if (allocatedAuxStorage) { this->auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
this->allocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
} }
if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::GaussSeidel) { if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings<ValueType>::SolutionMethod::GaussSeidel) {
@ -125,29 +126,29 @@ namespace storm {
A->performSuccessiveOverRelaxationStep(omega, x, b); A->performSuccessiveOverRelaxationStep(omega, x, b);
// Now check if the process already converged within our precision. // Now check if the process already converged within our precision.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*auxiliarySolvingMemory, x, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x)); converged = storm::utility::vector::equalModuloPrecision<ValueType>(*this->auxiliaryRowVector, x, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()) || (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x));
// If we did not yet converge, we need to backup the contents of x. // If we did not yet converge, we need to backup the contents of x.
if (!converged) { if (!converged) {
*auxiliarySolvingMemory = x; *this->auxiliaryRowVector = x;
} }
// Increase iteration count so we can abort if convergence is too slow. // Increase iteration count so we can abort if convergence is too slow.
++iterationCount; ++iterationCount;
} }
// If we allocated auxiliary memory, we need to dispose of it now.
if (allocatedAuxStorage) {
this->deallocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
}
return converged; return converged;
} else { } else {
// Get a Jacobi decomposition of the matrix A. // Get a Jacobi decomposition of the matrix A.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> jacobiDecomposition = A->getJacobiDecomposition(); if(!jacobiDecomposition) {
jacobiDecomposition = std::make_unique<std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>>>(A->getJacobiDecomposition());
}
storm::storage::SparseMatrix<ValueType> const& jacobiLU = jacobiDecomposition->first;
std::vector<ValueType> const& jacobiD = jacobiDecomposition->second;
std::vector<ValueType>* currentX = &x; std::vector<ValueType>* currentX = &x;
std::vector<ValueType>* nextX = auxiliarySolvingMemory.get(); std::vector<ValueType>* nextX = this->auxiliaryRowVector.get();
// Set up additional environment variables. // Set up additional environment variables.
uint_fast64_t iterationCount = 0; uint_fast64_t iterationCount = 0;
@ -155,9 +156,9 @@ namespace storm {
while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) { while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations() && !(this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(*currentX))) {
// Compute D^-1 * (b - LU * x) and store result in nextX. // Compute D^-1 * (b - LU * x) and store result in nextX.
jacobiDecomposition.first.multiplyWithVector(*currentX, *nextX); jacobiLU.multiplyWithVector(*currentX, *nextX);
storm::utility::vector::subtractVectors(b, *nextX, *nextX); storm::utility::vector::subtractVectors(b, *nextX, *nextX);
storm::utility::vector::multiplyVectorsPointwise(jacobiDecomposition.second, *nextX, *nextX); storm::utility::vector::multiplyVectorsPointwise(jacobiD, *nextX, *nextX);
// Now check if the process already converged within our precision. // Now check if the process already converged within our precision.
converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion()); converged = storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *nextX, static_cast<ValueType>(this->getSettings().getPrecision()), this->getSettings().getRelativeTerminationCriterion());
@ -171,18 +172,12 @@ namespace storm {
// If the last iteration did not write to the original x we have to swap the contents, because the // If the last iteration did not write to the original x we have to swap the contents, because the
// output has to be written to the input parameter x. // output has to be written to the input parameter x.
if (currentX == auxiliarySolvingMemory.get()) { if (currentX == this->auxiliaryRowVector.get()) {
std::swap(x, *currentX); std::swap(x, *currentX);
} }
// If we allocated auxiliary memory, we need to dispose of it now.
if (allocatedAuxStorage) {
this->deallocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
}
return iterationCount < this->getSettings().getMaximalNumberOfIterations(); return iterationCount < this->getSettings().getMaximalNumberOfIterations();
} }
} }
template<typename ValueType> template<typename ValueType>
@ -194,17 +189,21 @@ namespace storm {
} }
} else { } else {
// If the two vectors are aliases, we need to create a temporary. // If the two vectors are aliases, we need to create a temporary.
std::vector<ValueType> tmp(result.size()); if(!this->auxiliaryRowVector) {
A->multiplyWithVector(x, tmp); this->auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
}
A->multiplyWithVector(x, *this->auxiliaryRowVector);
if (b != nullptr) { if (b != nullptr) {
storm::utility::vector::addVectors(tmp, *b, result); storm::utility::vector::addVectors(*this->auxiliaryRowVector, *b, result);
} else {
result.swap(*this->auxiliaryRowVector);
} }
} }
} }
template<typename ValueType> template<typename ValueType>
NativeLinearEquationSolverSettings<ValueType>& NativeLinearEquationSolver<ValueType>::getSettings() { void NativeLinearEquationSolver<ValueType>::setSettings(NativeLinearEquationSolverSettings<ValueType> const& newSettings) {
return settings; settings = newSettings;
} }
template<typename ValueType> template<typename ValueType>
@ -213,52 +212,9 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::allocateAuxMemory(LinearEquationSolverOperation operation) const { void NativeLinearEquationSolver<ValueType>::resetAuxiliaryData() const {
bool result = false; jacobiDecomposition.reset();
if (operation == LinearEquationSolverOperation::SolveEquations) { LinearEquationSolver<ValueType>::resetAuxiliaryData();
if (!auxiliarySolvingMemory) {
auxiliarySolvingMemory = std::make_unique<std::vector<ValueType>>(this->getMatrixRowCount());
result = true;
}
}
result |= LinearEquationSolver<ValueType>::allocateAuxMemory(operation);
return result;
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::deallocateAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::SolveEquations) {
if (auxiliarySolvingMemory) {
result = true;
auxiliarySolvingMemory.reset();
}
}
result |= LinearEquationSolver<ValueType>::deallocateAuxMemory(operation);
return result;
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::reallocateAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::SolveEquations) {
if (auxiliarySolvingMemory) {
result = auxiliarySolvingMemory->size() != this->getMatrixColumnCount();
auxiliarySolvingMemory->resize(this->getMatrixRowCount());
}
}
result |= LinearEquationSolver<ValueType>::reallocateAuxMemory(operation);
return result;
}
template<typename ValueType>
bool NativeLinearEquationSolver<ValueType>::hasAuxMemory(LinearEquationSolverOperation operation) const {
bool result = false;
if (operation == LinearEquationSolverOperation::SolveEquations) {
result |= static_cast<bool>(auxiliarySolvingMemory);
}
result |= LinearEquationSolver<ValueType>::hasAuxMemory(operation);
return result;
} }
template<typename ValueType> template<typename ValueType>
@ -301,4 +257,4 @@ namespace storm {
template class NativeLinearEquationSolver<double>; template class NativeLinearEquationSolver<double>;
template class NativeLinearEquationSolverFactory<double>; template class NativeLinearEquationSolverFactory<double>;
} }
} }

14
src/solver/NativeLinearEquationSolver.h
View File

@ -52,15 +52,14 @@ namespace storm {
virtual bool solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override; virtual bool solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override; virtual void multiply(std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
NativeLinearEquationSolverSettings<ValueType>& getSettings(); void setSettings(NativeLinearEquationSolverSettings<ValueType> const& newSettings);
NativeLinearEquationSolverSettings<ValueType> const& getSettings() const; NativeLinearEquationSolverSettings<ValueType> const& getSettings() const;
virtual bool allocateAuxMemory(LinearEquationSolverOperation operation) const override; /*
virtual bool deallocateAuxMemory(LinearEquationSolverOperation operation) const override; * Clears auxiliary data that has possibly been stored during previous calls of the solver.
virtual bool reallocateAuxMemory(LinearEquationSolverOperation operation) const override; */
virtual bool hasAuxMemory(LinearEquationSolverOperation operation) const override; virtual void resetAuxiliaryData() const override;
storm::storage::SparseMatrix<ValueType> const& getMatrix() const { return *A; }
private: private:
virtual uint64_t getMatrixRowCount() const override; virtual uint64_t getMatrixRowCount() const override;
virtual uint64_t getMatrixColumnCount() const override; virtual uint64_t getMatrixColumnCount() const override;
@ -76,8 +75,7 @@ namespace storm {
// The settings used by the solver. // The settings used by the solver.
NativeLinearEquationSolverSettings<ValueType> settings; NativeLinearEquationSolverSettings<ValueType> settings;
// Auxiliary memory for the equation solving methods. mutable std::unique_ptr<std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>>> jacobiDecomposition;
mutable std::unique_ptr<std::vector<ValueType>> auxiliarySolvingMemory;
}; };
template<typename ValueType> template<typename ValueType>

50
src/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -99,10 +99,10 @@ namespace storm {
std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupCount()); std::vector<storm::storage::sparse::state_type> scheduler(this->A.getRowGroupCount());
// Get a vector for storing the right-hand side of the inner equation system. // Get a vector for storing the right-hand side of the inner equation system.
if(!auxiliaryData.rowGroupVector) { if(!auxiliaryRowGroupVector) {
auxiliaryData.rowGroupVector = std::make_unique<std::vector<ValueType>>(this->A.getRowGroupCount()); auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A.getRowGroupCount());
} }
std::vector<ValueType>& subB = *auxiliaryData.rowGroupVector; std::vector<ValueType>& subB = *auxiliaryRowGroupVector;
// Resolve the nondeterminism according to the current scheduler. // Resolve the nondeterminism according to the current scheduler.
storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true); storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(scheduler, true);
@ -111,7 +111,6 @@ namespace storm {
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. // 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)); auto solver = linearEquationSolverFactory->create(std::move(submatrix));
solver->allocateAuxMemory(LinearEquationSolverOperation::SolveEquations);
Status status = Status::InProgress; Status status = Status::InProgress;
uint64_t iterations = 0; uint64_t iterations = 0;
@ -139,6 +138,8 @@ namespace storm {
choiceValue += b[choice]; choiceValue += b[choice];
// If the value is strictly better than the solution of the inner system, we need to improve the scheduler. // If the value is strictly better than the solution of the inner system, we need to improve the scheduler.
// TODO: If the underlying solver is not precise, this might run forever (i.e. when a state has two choices where the (exact) values are equal).
// only changing the scheduler if the values are not equal (modulo precision) would make this unsound.
if (valueImproved(dir, x[group], choiceValue)) { if (valueImproved(dir, x[group], choiceValue)) {
schedulerImproved = true; schedulerImproved = true;
scheduler[group] = choice - this->A.getRowGroupIndices()[group]; scheduler[group] = choice - this->A.getRowGroupIndices()[group];
@ -205,19 +206,19 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const { bool StandardMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
if(!auxiliaryData.linEqSolver) { if(!linEqSolverA) {
auxiliaryData.linEqSolver = linearEquationSolverFactory->create(A); linEqSolverA = linearEquationSolverFactory->create(A);
} }
if (!auxiliaryData.rowVector.get()) { if (!auxiliaryRowVector.get()) {
auxiliaryData.rowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount()); auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount());
} }
std::vector<ValueType>& multiplyResult = *auxiliaryData.rowVector; std::vector<ValueType>& multiplyResult = *auxiliaryRowVector;
if (!auxiliaryData.rowGroupVector.get()) { if (!auxiliaryRowGroupVector.get()) {
auxiliaryData.rowGroupVector = std::make_unique<std::vector<ValueType>>(A.getRowGroupCount()); auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(A.getRowGroupCount());
} }
std::vector<ValueType>* newX = auxiliaryData.rowGroupVector.get(); std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
std::vector<ValueType>* currentX = &x; std::vector<ValueType>* currentX = &x;
@ -227,7 +228,7 @@ namespace storm {
Status status = Status::InProgress; Status status = Status::InProgress;
while (status == Status::InProgress) { while (status == Status::InProgress) {
// Compute x' = A*x + b. // Compute x' = A*x + b.
auxiliaryData.linEqSolver->multiply(*currentX, &b, multiplyResult); linEqSolverA->multiply(*currentX, &b, multiplyResult);
// Reduce the vector x' by applying min/max for all non-deterministic choices. // Reduce the vector x' by applying min/max for all non-deterministic choices.
storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices()); storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices());
@ -248,14 +249,14 @@ namespace storm {
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
// is currently stored in currentX, but x is the output vector. // is currently stored in currentX, but x is the output vector.
if (currentX == auxiliaryData.rowGroupVector.get()) { if (currentX == auxiliaryRowGroupVector.get()) {
std::swap(x, *currentX); std::swap(x, *currentX);
} }
// If requested, we store the scheduler for retrieval. // If requested, we store the scheduler for retrieval.
if (this->isTrackSchedulerSet()) { if (this->isTrackSchedulerSet()) {
if(iterations==0){ //may happen due to custom termination condition. Then we need to compute x'= A*x+b if(iterations==0){ //may happen due to custom termination condition. Then we need to compute x'= A*x+b
auxiliaryData.linEqSolver->multiply(x, &b, multiplyResult); linEqSolverA->multiply(x, &b, multiplyResult);
} }
std::vector<storm::storage::sparse::state_type> choices(this->A.getRowGroupCount()); std::vector<storm::storage::sparse::state_type> choices(this->A.getRowGroupCount());
// Reduce the multiplyResult and keep track of the choices made // Reduce the multiplyResult and keep track of the choices made
@ -272,17 +273,17 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const { void StandardMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const {
if(!auxiliaryData.linEqSolver) { if(!linEqSolverA) {
auxiliaryData.linEqSolver = linearEquationSolverFactory->create(A); linEqSolverA = linearEquationSolverFactory->create(A);
} }
if (!auxiliaryData.rowVector.get()) { if (!auxiliaryRowVector.get()) {
auxiliaryData.rowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount()); auxiliaryRowVector = std::make_unique<std::vector<ValueType>>(A.getRowCount());
} }
std::vector<ValueType>& multiplyResult = *auxiliaryData.rowVector; std::vector<ValueType>& multiplyResult = *auxiliaryRowVector;
for (uint64_t i = 0; i < n; ++i) { for (uint64_t i = 0; i < n; ++i) {
auxiliaryData.linEqSolver->multiply(x, b, multiplyResult); linEqSolverA->multiply(x, b, multiplyResult);
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack. // element of the min/max operator stack.
@ -325,9 +326,10 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::resetAuxiliaryData() const { void StandardMinMaxLinearEquationSolver<ValueType>::resetAuxiliaryData() const {
auxiliaryData.linEqSolver.reset(); linEqSolverA.reset();
auxiliaryData.rowVector.reset(); auxiliaryRowVector.reset();
auxiliaryData.rowGroupVector.reset(); auxiliaryRowGroupVector.reset();
MinMaxLinearEquationSolver<ValueType>::resetAuxiliaryData();
} }
template<typename ValueType> template<typename ValueType>

10
src/solver/StandardMinMaxLinearEquationSolver.h
View File

@ -60,13 +60,9 @@ namespace storm {
Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
}; };
struct AuxiliaryData { mutable std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolverA;
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolver; mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowVector; // A.rowCount() entries
std::unique_ptr<std::vector<ValueType>> rowVector; // A.rowCount() entries mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector; // A.rowGroupCount() entries
std::unique_ptr<std::vector<ValueType>> rowGroupVector; // A.rowGroupCount() entries
};
mutable AuxiliaryData auxiliaryData;
Status updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations) const; Status updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations) const;
void reportStatus(Status status, uint64_t iterations) const; void reportStatus(Status status, uint64_t iterations) const;

4
src/utility/policyguessing.cpp
View File

@ -171,14 +171,16 @@ namespace storm {
storm::utility::vector::selectVectorValues(subB, probGreater0States, b); storm::utility::vector::selectVectorValues(subB, probGreater0States, b);
std::unique_ptr<storm::solver::GmmxxLinearEquationSolver<ValueType>> linEqSysSolver(static_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(storm::solver::GmmxxLinearEquationSolverFactory<ValueType>().create(eqSysA).release())); std::unique_ptr<storm::solver::GmmxxLinearEquationSolver<ValueType>> linEqSysSolver(static_cast<storm::solver::GmmxxLinearEquationSolver<ValueType>*>(storm::solver::GmmxxLinearEquationSolverFactory<ValueType>().create(eqSysA).release()));
auto& eqSettings = linEqSysSolver->getSettings(); auto eqSettings = linEqSysSolver->getSettings();
eqSettings.setRelativeTerminationCriterion(relative); eqSettings.setRelativeTerminationCriterion(relative);
eqSettings.setMaximalNumberOfIterations(500); eqSettings.setMaximalNumberOfIterations(500);
linEqSysSolver->setSettings(eqSettings);
std::size_t iterations = 0; std::size_t iterations = 0;
std::vector<ValueType> copyX(subX.size()); std::vector<ValueType> copyX(subX.size());
ValueType precisionChangeFactor = storm::utility::one<ValueType>(); ValueType precisionChangeFactor = storm::utility::one<ValueType>();
do { do {
eqSettings.setPrecision(eqSettings.getPrecision() * precisionChangeFactor); eqSettings.setPrecision(eqSettings.getPrecision() * precisionChangeFactor);
linEqSysSolver->setSettings(eqSettings);
if(!linEqSysSolver->solveEquations(subX, subB)){ if(!linEqSysSolver->solveEquations(subX, subB)){
// break; //Solver did not converge.. so we have to go on with the current solution. // break; //Solver did not converge.. so we have to go on with the current solution.
} }

78
test/functional/solver/GmmxxLinearEquationSolverTest.cpp
View File

@ -54,11 +54,13 @@ TEST(GmmxxLinearEquationSolver, gmres) {
std::vector<double> b = {16, -4, -7}; std::vector<double> b = {16, -4, -7};
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Gmres); auto settings = solver.getSettings();
solver.getSettings().setPrecision(1e-6); settings.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Gmres);
solver.getSettings().setMaximalNumberOfIterations(10000); settings.setPrecision(1e-6);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None); settings.setMaximalNumberOfIterations(10000);
solver.getSettings().setNumberOfIterationsUntilRestart(50); settings.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None);
settings.setNumberOfIterationsUntilRestart(50);
solver.setSettings(settings);
ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -86,16 +88,20 @@ TEST(GmmxxLinearEquationSolver, qmr) {
std::vector<double> b = {16, -4, -7}; std::vector<double> b = {16, -4, -7};
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Qmr); auto settings = solver.getSettings();
solver.getSettings().setPrecision(1e-6); settings.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Qmr);
solver.getSettings().setMaximalNumberOfIterations(10000); settings.setPrecision(1e-6);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None); settings.setMaximalNumberOfIterations(10000);
settings.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None);
solver.setSettings(settings);
storm::solver::GmmxxLinearEquationSolver<double> solver2(A); storm::solver::GmmxxLinearEquationSolver<double> solver2(A);
solver2.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Qmr); auto settings2 = solver2.getSettings();
solver2.getSettings().setPrecision(1e-6); settings2.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Qmr);
solver2.getSettings().setMaximalNumberOfIterations(10000); settings2.setPrecision(1e-6);
solver2.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None); settings2.setMaximalNumberOfIterations(10000);
settings2.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None);
solver2.setSettings(settings2);
ASSERT_NO_THROW(solver2.solveEquations(x, b)); ASSERT_NO_THROW(solver2.solveEquations(x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -123,10 +129,12 @@ TEST(GmmxxLinearEquationSolver, bicgstab) {
std::vector<double> b = {16, -4, -7}; std::vector<double> b = {16, -4, -7};
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Bicgstab); auto settings = solver.getSettings();
solver.getSettings().setPrecision(1e-6); settings.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Bicgstab);
solver.getSettings().setMaximalNumberOfIterations(10000); settings.setPrecision(1e-6);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None); settings.setMaximalNumberOfIterations(10000);
settings.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None);
solver.setSettings(settings);
ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -154,10 +162,12 @@ TEST(GmmxxLinearEquationSolver, jacobi) {
std::vector<double> b = {11, -16, 1}; std::vector<double> b = {11, -16, 1};
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Jacobi); auto settings = solver.getSettings();
solver.getSettings().setPrecision(1e-6); settings.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Jacobi);
solver.getSettings().setMaximalNumberOfIterations(10000); settings.setPrecision(1e-6);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None); settings.setMaximalNumberOfIterations(10000);
settings.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::None);
solver.setSettings(settings);
ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -184,11 +194,13 @@ TEST(GmmxxLinearEquationSolver, gmresilu) {
std::vector<double> b = {16, -4, -7}; std::vector<double> b = {16, -4, -7};
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Gmres); auto settings = solver.getSettings();
solver.getSettings().setPrecision(1e-6); settings.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Gmres);
solver.getSettings().setMaximalNumberOfIterations(10000); settings.setPrecision(1e-6);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::Ilu); settings.setMaximalNumberOfIterations(10000);
solver.getSettings().setNumberOfIterationsUntilRestart(50); settings.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::Ilu);
settings.setNumberOfIterationsUntilRestart(50);
solver.setSettings(settings);
ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[1] - 3), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -215,11 +227,13 @@ TEST(GmmxxLinearEquationSolver, gmresdiag) {
std::vector<double> b = {16, -4, -7}; std::vector<double> b = {16, -4, -7};
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
solver.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Gmres); auto settings = solver.getSettings();
solver.getSettings().setPrecision(1e-6); settings.setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings<double>::SolutionMethod::Gmres);
solver.getSettings().setMaximalNumberOfIterations(10000); settings.setPrecision(1e-6);
solver.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::Diagonal); settings.setMaximalNumberOfIterations(10000);
solver.getSettings().setNumberOfIterationsUntilRestart(50); settings.setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings<double>::Preconditioner::Diagonal);
settings.setNumberOfIterationsUntilRestart(50);
solver.setSettings(settings);
ASSERT_NO_THROW(solver.solveEquations(x, b)); ASSERT_NO_THROW(solver.solveEquations(x, b));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
@ -248,4 +262,4 @@ TEST(GmmxxLinearEquationSolver, MatrixVectorMultiplication) {
storm::solver::GmmxxLinearEquationSolver<double> solver(A); storm::solver::GmmxxLinearEquationSolver<double> solver(A);
ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4)); ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4));
ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision()); ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
} }
Write Preview
|||||||
100:0
Loading…
Cancel
Save