Storm 1.14.0.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>
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>
40uint64_t AcyclicLinearEquationSolver<ValueType>::getMatrixRowCount() const {
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 if (bFactor.second) {
77 (*auxiliaryRowVector)[bFactor.first] *= *bFactor.second;
78 } else {
79 // A selfloop of probability one: the equation for this row can only be satisfied if it contributes nothing.
80 STORM_LOG_ASSERT(storm::utility::isZero((*auxiliaryRowVector)[bFactor.first]),
81 "Expected a zero b vector entry for a row with a selfloop of probability one.");
82 }
83 }
84 bPtr = &auxiliaryRowVector.get();
85 xPtr = &auxiliaryRowVector2.get();
86 }
87
88 this->multiplier->multiplyGaussSeidel(env, *xPtr, bPtr, true);
89
90 if (rowOrdering) {
91 for (uint64_t newRow = 0; newRow < x.size(); ++newRow) {
92 x[(*rowOrdering)[newRow]] = (*xPtr)[newRow];
93 }
94 }
95
96 if (!this->isCachingEnabled()) {
97 this->clearCache();
98 }
99 return true;
100}
101
102template<typename ValueType>
106
107template<typename ValueType>
109 // Return the requirements of the underlying solver
111 requirements.requireAcyclic();
112 return requirements;
113}
114
115template<typename ValueType>
117 multiplier.reset();
118 orderedMatrix = boost::none;
119 rowOrdering = boost::none;
120 auxiliaryRowVector = boost::none;
121 auxiliaryRowVector2 = boost::none;
122 bFactors.clear();
123}
124
125// Explicitly instantiate the min max linear equation solver.
127
130} // namespace solver
131} // 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.
bool isCachingEnabled() const
Retrieves whether some of the generated data during solver calls should be cached.
LinearEquationSolverRequirements & requireAcyclic(bool critical=true)
std::unique_ptr< Multiplier< ValueType, SolutionType > > 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:9
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...
storm::storage::SparseMatrix< ValueType > createReorderedMatrix(storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< uint64_t > const &newToOrigIndexMap, std::vector< std::pair< uint64_t, std::optional< ValueType > > > &bFactors)
reorders the row group such that the i'th row of the new matrix corresponds to the order[i]'th row of...
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
bool isZero(ValueType const &a)
Definition constants.cpp:42