Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
AcyclicLinearEquationSolver.cpp
Go to the documentation of this file.
2
6
7namespace storm {
8namespace solver {
9
10template<typename ValueType>
14
15template<typename ValueType>
19
20template<typename ValueType>
24
25template<typename ValueType>
27 localA.reset();
28 this->A = &A;
29 clearCache();
30}
31
32template<typename ValueType>
34 localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A));
35 this->A = localA.get();
36 clearCache();
37}
38
39template<typename ValueType>
41 return this->A->getRowCount();
42}
43
44template<typename ValueType>
45uint64_t AcyclicLinearEquationSolver<ValueType>::getMatrixColumnCount() const {
46 return this->A->getColumnCount();
47}
48
49template<typename ValueType>
50bool AcyclicLinearEquationSolver<ValueType>::internalSolveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
51 STORM_LOG_ASSERT(x.size() == this->A->getRowGroupCount(), "Provided x-vector has invalid size.");
52 STORM_LOG_ASSERT(b.size() == this->A->getRowCount(), "Provided b-vector has invalid size.");
53
54 if (!multiplier) {
55 // We have not allocated cache memory, yet
56 rowOrdering = helper::computeTopologicalGroupOrdering(*this->A);
57 if (!rowOrdering) {
58 // It is not required to reorder the elements.
59 this->multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, *this->A);
60 } else {
61 bFactors.clear();
62 orderedMatrix = helper::createReorderedMatrix(*this->A, *rowOrdering, bFactors);
63 this->multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, *orderedMatrix);
64 }
65 auxiliaryRowVector = std::vector<ValueType>(this->A->getRowCount());
66 auxiliaryRowVector2 = std::vector<ValueType>(this->A->getRowCount());
67 }
68
69 std::vector<ValueType>* xPtr = &x;
70 std::vector<ValueType> const* bPtr = &b;
71 if (rowOrdering) {
72 STORM_LOG_ASSERT(rowOrdering->size() == b.size(), "b-vector has unexpected size.");
73 auxiliaryRowVector->resize(b.size());
74 storm::utility::vector::selectVectorValues(*auxiliaryRowVector, *rowOrdering, b);
75 for (auto const& bFactor : bFactors) {
76 (*auxiliaryRowVector)[bFactor.first] *= bFactor.second;
77 }
78 bPtr = &auxiliaryRowVector.get();
79 xPtr = &auxiliaryRowVector2.get();
80 }
81
82 this->multiplier->multiplyGaussSeidel(env, *xPtr, bPtr, true);
83
84 if (rowOrdering) {
85 for (uint64_t newRow = 0; newRow < x.size(); ++newRow) {
86 x[(*rowOrdering)[newRow]] = (*xPtr)[newRow];
87 }
88 }
89
90 if (!this->isCachingEnabled()) {
91 this->clearCache();
92 }
93 return true;
94}
95
96template<typename ValueType>
100
101template<typename ValueType>
103 // Return the requirements of the underlying solver
105 requirements.requireAcyclic();
106 return requirements;
107}
108
109template<typename ValueType>
111 multiplier.reset();
112 orderedMatrix = boost::none;
113 rowOrdering = boost::none;
114 auxiliaryRowVector = boost::none;
115 auxiliaryRowVector2 = boost::none;
116 bFactors.clear();
117}
118
119// Explicitly instantiate the min max linear equation solver.
121
124} // namespace solver
125} // namespace storm
This solver can be used on equation systems that are known to be acyclic.
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.
LinearEquationSolverRequirements & requireAcyclic(bool critical=true)
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
A class that holds a possibly non-square matrix in the compressed row storage format.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
storm::storage::SparseMatrix< ValueType > createReorderedMatrix(storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< uint64_t > const &newToOrigIndexMap, std::vector< std::pair< uint64_t, ValueType > > &bFactors)
reorders the row group such that the i'th row of the new matrix corresponds to the order[i]'th row of...
boost::optional< std::vector< uint64_t > > computeTopologicalGroupOrdering(storm::storage::SparseMatrix< ValueType > const &matrix)
Returns a reordering of the matrix row(groups) and columns such that we can solve the (minmax or line...
void selectVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Selects the elements from a vector at the specified positions and writes them consecutively into anot...
Definition vector.h:184