Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GmmxxLinearEquationSolver.cpp
Go to the documentation of this file.
2
3#include <cmath>
4#include <utility>
5
12
13namespace storm {
14namespace solver {
15
16template<typename ValueType>
20
21template<typename ValueType>
25
26template<typename ValueType>
30
31template<typename ValueType>
33#ifdef STORM_HAVE_GMM
35 clearCache();
36#else
37 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GMM. Yet, a method was called that "
38 "requires this support.";
39#endif
40}
41
42template<typename ValueType>
44#ifdef STORM_HAVE_GMM
46 clearCache();
47#else
48 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GMM. Yet, a method was called that "
49 "requires this support.";
50#endif
51}
52
53template<typename ValueType>
54GmmxxLinearEquationSolverMethod GmmxxLinearEquationSolver<ValueType>::getMethod(Environment const& env) const {
55 STORM_LOG_ERROR_COND(!env.solver().isForceSoundness(), "This linear equation solver does not support sound computations. Using unsound methods now...");
56 STORM_LOG_ERROR_COND(!env.solver().isForceExact(), "This linear equation solver does not support exact computations. Using unsound methods now...");
57 return env.solver().gmmxx().getMethod();
58}
59
60template<typename ValueType>
61bool GmmxxLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
62#ifdef STORM_HAVE_GMM
63 auto method = getMethod(env);
64 auto preconditioner = env.solver().gmmxx().getPreconditioner();
65
66 STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with Gmmxx linear equation solver with method '" << toString(method)
67 << "' and preconditioner '" << toString(preconditioner) << "'.");
68
69 if (method == GmmxxLinearEquationSolverMethod::Bicgstab || method == GmmxxLinearEquationSolverMethod::Qmr ||
70 method == GmmxxLinearEquationSolverMethod::Gmres) {
71 // Make sure that the requested preconditioner is available
72 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu && !iluPreconditioner) {
73 iluPreconditioner = std::make_unique<gmm::ilu_precond<gmm::csr_matrix<ValueType>>>(*gmmxxA);
74 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
75 diagonalPreconditioner = std::make_unique<gmm::diagonal_precond<gmm::csr_matrix<ValueType>>>(*gmmxxA);
76 }
77
78 // Prepare an iteration object that determines the accuracy and the maximum number of iterations.
79 gmm::size_type maxIter = std::numeric_limits<gmm::size_type>::max();
80 if (env.solver().gmmxx().getMaximalNumberOfIterations() < static_cast<uint64_t>(maxIter)) {
81 maxIter = env.solver().gmmxx().getMaximalNumberOfIterations();
82 }
83 gmm::iteration iter(storm::utility::convertNumber<ValueType>(env.solver().gmmxx().getPrecision()), 0, maxIter);
84 iter.set_callback([](const gmm::iteration& iteration) -> void {
85 STORM_LOG_THROW(!storm::utility::resources::isTerminate(), storm::exceptions::AbortException,
86 "Gmm++ (externally) aborted after " << iteration.get_iteration() << " iterations.");
87 });
88
89 // We use throwing an exception to abort within Gmm++
90 try {
91 // Invoke gmm with the corresponding settings
92 if (method == GmmxxLinearEquationSolverMethod::Bicgstab) {
93 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) {
94 gmm::bicgstab(*gmmxxA, x, b, *iluPreconditioner, iter);
95 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
96 gmm::bicgstab(*gmmxxA, x, b, *diagonalPreconditioner, iter);
97 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) {
98 gmm::bicgstab(*gmmxxA, x, b, gmm::identity_matrix(), iter);
99 }
100 } else if (method == GmmxxLinearEquationSolverMethod::Qmr) {
101 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) {
102 gmm::qmr(*gmmxxA, x, b, *iluPreconditioner, iter);
103 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
104 gmm::qmr(*gmmxxA, x, b, *diagonalPreconditioner, iter);
105 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) {
106 gmm::qmr(*gmmxxA, x, b, gmm::identity_matrix(), iter);
107 }
108 } else if (method == GmmxxLinearEquationSolverMethod::Gmres) {
109 if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Ilu) {
110 gmm::gmres(*gmmxxA, x, b, *iluPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter);
111 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::Diagonal) {
112 gmm::gmres(*gmmxxA, x, b, *diagonalPreconditioner, env.solver().gmmxx().getRestartThreshold(), iter);
113 } else if (preconditioner == GmmxxLinearEquationSolverPreconditioner::None) {
114 gmm::gmres(*gmmxxA, x, b, gmm::identity_matrix(), env.solver().gmmxx().getRestartThreshold(), iter);
115 }
116 }
117 } catch (storm::exceptions::AbortException const& e) {
118 // Do nothing
119 }
120
121 if (!this->isCachingEnabled()) {
122 clearCache();
123 }
124
125 // Make sure that all results conform to the bounds.
126 storm::utility::vector::clip(x, this->lowerBound, this->upperBound);
127
128 // Check if the solver converged and issue a warning otherwise.
129 if (iter.converged()) {
130 STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iteration(s).");
131 return true;
132 } else {
133 STORM_LOG_WARN("Iterative solver did not converge within " << iter.get_iteration() << " iteration(s).");
134 return false;
135 }
136 }
137
138 STORM_LOG_ERROR("Selected method is not available");
139 return false;
140#else
141 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GMM. Yet, a method was called that "
142 "requires this support.";
143#endif
144}
145
146template<typename ValueType>
150
151template<typename ValueType>
153#ifdef STORM_HAVE_GMM
154 iluPreconditioner.reset();
155 diagonalPreconditioner.reset();
157#else
158 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GMM. Yet, a method was called that "
159 "requires this support.";
160#endif
161}
162
163template<typename ValueType>
165#ifdef STORM_HAVE_GMM
166 return gmmxxA->nr;
167#else
168 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GMM. Yet, a method was called that "
169 "requires this support.";
170#endif
171}
172
173template<typename ValueType>
174uint64_t GmmxxLinearEquationSolver<ValueType>::getMatrixColumnCount() const {
175#ifdef STORM_HAVE_GMM
176 return gmmxxA->nc;
177#else
178 throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for GMM. Yet, a method was called that "
179 "requires this support.";
180#endif
181}
182
183template<typename ValueType>
184std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
185 return std::make_unique<storm::solver::GmmxxLinearEquationSolver<ValueType>>();
186}
187
188template<typename ValueType>
189std::unique_ptr<LinearEquationSolverFactory<ValueType>> GmmxxLinearEquationSolverFactory<ValueType>::clone() const {
190 return std::make_unique<GmmxxLinearEquationSolverFactory<ValueType>>(*this);
191}
192
193// Explicitly instantiate the solver.
196
197} // namespace solver
198} // namespace storm
SolverEnvironment & solver()
storm::RationalNumber const & getPrecision() const
uint64_t const & getMaximalNumberOfIterations() const
storm::solver::GmmxxLinearEquationSolverMethod const & getMethod() const
uint64_t const & getRestartThreshold() const
storm::solver::GmmxxLinearEquationSolverPreconditioner const & getPreconditioner() const
GmmxxSolverEnvironment & gmmxx()
virtual std::unique_ptr< LinearEquationSolverFactory< ValueType > > clone() const override
Creates a copy of this factory.
virtual std::unique_ptr< storm::solver::LinearEquationSolver< ValueType > > create(Environment const &env) const override
Creates an equation solver with the current settings, but without a matrix.
A class that uses the gmm++ library to implement the LinearEquationSolver interface.
virtual bool internalSolveEquations(Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const &b) const override
virtual void setMatrix(storm::storage::SparseMatrix< ValueType > const &A) override
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(Environment const &env) const override
Retrieves the format in which this solver expects to solve equations.
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_INFO(message)
Definition logging.h:29
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_ERROR(message)
Definition logging.h:31
#define STORM_LOG_ERROR_COND(cond, message)
Definition macros.h:52
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::string toString(GurobiSolverMethod const &method)
Yields a string representation of the GurobiSolverMethod.
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
void clip(std::vector< ValueType > &x, boost::optional< ValueType > const &lowerBound, boost::optional< ValueType > const &upperBound)
Takes the input vector and ensures that all entries conform to the bounds.
Definition vector.h:892
LabParser.cpp.
Definition cli.cpp:18