Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
NativeLinearEquationSolver.h
Go to the documentation of this file.
1#ifndef STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_
2#define STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_
3
4#include <ostream>
5
7
12
14
15namespace storm {
16
17class Environment;
18
19namespace solver {
20
24template<typename ValueType>
26 public:
30
31 virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& A) override;
32 virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& A) override;
33
35 virtual LinearEquationSolverRequirements getRequirements(Environment const& env) const override;
36
37 virtual void clearCache() const override;
38
39 protected:
40 virtual bool internalSolveEquations(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
41
42 private:
43 struct PowerIterationResult {
44 PowerIterationResult(uint64_t iterations, SolverStatus status) : iterations(iterations), status(status) {
45 // Intentionally left empty.
46 }
47
48 uint64_t iterations;
49 SolverStatus status;
50 };
51
52 template<typename ValueTypePrime>
54
55 PowerIterationResult performPowerIteration(Environment const& env, std::vector<ValueType>*& currentX, std::vector<ValueType>*& newX,
56 std::vector<ValueType> const& b, ValueType const& precision, bool relative, SolverGuarantee const& guarantee,
57 uint64_t currentIterations, uint64_t maxIterations,
58 storm::solver::MultiplicationStyle const& multiplicationStyle) const;
59
60 void logIterations(bool converged, bool terminate, uint64_t iterations) const;
61
62 virtual uint64_t getMatrixRowCount() const override;
63 virtual uint64_t getMatrixColumnCount() const override;
64
65 NativeLinearEquationSolverMethod getMethod(Environment const& env, bool isExactMode) const;
66
67 virtual bool solveEquationsSOR(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b, ValueType const& omega) const;
68 virtual bool solveEquationsJacobi(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
69 virtual bool solveEquationsWalkerChae(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
70 virtual bool solveEquationsPower(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
71 virtual bool solveEquationsSoundValueIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
72 virtual bool solveEquationsOptimisticValueIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
73 virtual bool solveEquationsIntervalIteration(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
74 virtual bool solveEquationsRationalSearch(storm::Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
75
76 void setUpViOperator() const;
77
78 // If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted
79 // when the solver is destructed.
80 std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;
81
82 // A pointer to the original sparse matrix given to this solver. If the solver takes posession of the matrix
83 // the pointer refers to localA.
85
86 mutable std::shared_ptr<storm::solver::helper::ValueIterationOperator<ValueType, true>> viOperator;
87
88 // An object to dispatch all multiplication operations.
89 mutable std::unique_ptr<Multiplier<ValueType>> multiplier;
90
91 struct JacobiDecomposition {
92 JacobiDecomposition(Environment const& env, storm::storage::SparseMatrix<ValueType> const& A);
93
95 std::vector<ValueType> DVector;
96 std::unique_ptr<storm::solver::Multiplier<ValueType>> multiplier;
97 };
98 mutable std::unique_ptr<JacobiDecomposition> jacobiDecomposition;
99
100 struct WalkerChaeData {
101 WalkerChaeData(Environment const& env, storm::storage::SparseMatrix<ValueType> const& originalMatrix, std::vector<ValueType> const& originalB);
102
103 void computeWalkerChaeMatrix(storm::storage::SparseMatrix<ValueType> const& originalMatrix);
104 void computeNewB(std::vector<ValueType> const& originalB);
105 void precomputeAuxiliaryData();
106
108 std::vector<ValueType> b;
109 ValueType t;
110 std::unique_ptr<storm::solver::Multiplier<ValueType>> multiplier;
111
112 // Auxiliary data.
113 std::vector<ValueType> columnSums;
114 std::vector<ValueType> newX;
115 };
116 mutable std::unique_ptr<WalkerChaeData> walkerChaeData;
117};
118
119template<typename ValueType>
121 public:
123
124 virtual std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> create(Environment const& env) const override;
125
126 virtual std::unique_ptr<LinearEquationSolverFactory<ValueType>> clone() const override;
127};
128} // namespace solver
129} // namespace storm
130
131#endif /* STORM_SOLVER_NATIVELINEAREQUATIONSOLVER_H_ */
An interface that represents an abstract linear equation solver.
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.
virtual std::unique_ptr< LinearEquationSolverFactory< ValueType > > clone() const override
Creates a copy of this factory.
A class that uses storm's native matrix operations to implement the LinearEquationSolver interface.
virtual LinearEquationSolverProblemFormat getEquationProblemFormat(storm::Environment const &env) const override
Retrieves the format in which this solver expects to solve equations.
virtual bool internalSolveEquations(storm::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 LinearEquationSolverRequirements getRequirements(Environment const &env) const override
Retrieves the requirements of the solver under the current settings.
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18