Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
AcyclicMinMaxLinearEquationSolver.cpp
Go to the documentation of this file.
2
4
6
7namespace storm {
8namespace solver {
9
10template<typename ValueType>
14
15template<typename ValueType>
20
21template<typename ValueType>
26
27template<typename ValueType>
29 std::vector<ValueType> const& b) const {
30 STORM_LOG_ASSERT(x.size() == this->A->getRowGroupCount(), "Provided x-vector has invalid size.");
31 STORM_LOG_ASSERT(b.size() == this->A->getRowCount(), "Provided b-vector has invalid size.");
32
33 if (!multiplier) {
34 // We have not allocated cache memory, yet
35 rowGroupOrdering = helper::computeTopologicalGroupOrdering(*this->A);
36 if (!rowGroupOrdering) {
37 // It is not required to reorder the elements.
38 this->multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, *this->A);
39 } else {
40 bFactors.clear();
41 orderedMatrix = helper::createReorderedMatrix(*this->A, *rowGroupOrdering, bFactors);
42 this->multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, *orderedMatrix);
43 }
44 auxiliaryRowVector = std::vector<ValueType>(this->A->getRowCount());
45 auxiliaryRowGroupVector = std::vector<ValueType>(this->A->getRowGroupCount());
46 }
47
48 std::vector<ValueType>* xPtr = &x;
49 std::vector<ValueType> const* bPtr = &b;
50 if (rowGroupOrdering) {
51 STORM_LOG_ASSERT(rowGroupOrdering->size() == x.size(), "x-vector has unexpected size.");
52 STORM_LOG_ASSERT(auxiliaryRowGroupVector->size() == x.size(), "x-vector has unexpected size.");
53 STORM_LOG_ASSERT(auxiliaryRowVector->size() == b.size(), "b-vector has unexpected size.");
54 for (uint64_t newGroupIndex = 0; newGroupIndex < x.size(); ++newGroupIndex) {
55 uint64_t newRow = orderedMatrix->getRowGroupIndices()[newGroupIndex];
56 uint64_t newRowGroupEnd = orderedMatrix->getRowGroupIndices()[newGroupIndex + 1];
57 uint64_t oldRow = this->A->getRowGroupIndices()[(*rowGroupOrdering)[newGroupIndex]];
58 for (; newRow < newRowGroupEnd; ++newRow, ++oldRow) {
59 (*auxiliaryRowVector)[newRow] = b[oldRow];
60 }
61 }
62 for (auto const& bFactor : bFactors) {
63 (*auxiliaryRowVector)[bFactor.first] *= bFactor.second;
64 }
65 xPtr = &auxiliaryRowGroupVector.get();
66 bPtr = &auxiliaryRowVector.get();
67 }
68
69 // Allocate memory for the scheduler (if required)
70 std::vector<uint64_t>* choicesPtr = nullptr;
71 if (this->isTrackSchedulerSet()) {
72 if (this->schedulerChoices) {
73 this->schedulerChoices->resize(this->A->getRowGroupCount());
74 } else {
75 this->schedulerChoices = std::vector<uint64_t>(this->A->getRowGroupCount());
76 }
77 if (rowGroupOrdering) {
78 if (auxiliaryRowGroupIndexVector) {
79 auxiliaryRowGroupIndexVector->resize(this->A->getRowGroupCount());
80 } else {
81 auxiliaryRowGroupIndexVector = std::vector<uint64_t>(this->A->getRowGroupCount());
82 }
83 choicesPtr = &(auxiliaryRowGroupIndexVector.get());
84 } else {
85 choicesPtr = &(this->schedulerChoices.get());
86 }
87 }
88
89 // Since a topological ordering is guaranteed, we can solve the equations with a single matrix-vector Multiplication step.
90 this->multiplier->multiplyAndReduceGaussSeidel(env, dir, *xPtr, bPtr, choicesPtr, true);
91
92 if (rowGroupOrdering) {
93 // Restore the correct input-order for the output vector
94 for (uint64_t newGroupIndex = 0; newGroupIndex < x.size(); ++newGroupIndex) {
95 x[(*rowGroupOrdering)[newGroupIndex]] = (*xPtr)[newGroupIndex];
96 }
97 if (this->isTrackSchedulerSet()) {
98 // Do the same for the scheduler choices
99 for (uint64_t newGroupIndex = 0; newGroupIndex < x.size(); ++newGroupIndex) {
100 this->schedulerChoices.get()[(*rowGroupOrdering)[newGroupIndex]] = (*choicesPtr)[newGroupIndex];
101 }
102 }
103 }
104
105 if (!this->isCachingEnabled()) {
106 this->clearCache();
107 }
108 return true;
109}
110
111template<typename ValueType>
113 Environment const&, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
114 // Return the requirements of the underlying solver
116 requirements.requireAcyclic();
117 return requirements;
118}
119
120template<typename ValueType>
122 multiplier.reset();
123 orderedMatrix = boost::none;
124 rowGroupOrdering = boost::none;
125 auxiliaryRowVector = boost::none;
126 auxiliaryRowGroupVector = boost::none;
127 auxiliaryRowGroupIndexVector = boost::none;
128 bFactors.clear();
129}
130
131// Explicitly instantiate the min max linear equation solver.
134} // namespace solver
135} // namespace storm
This solver can be used on equation systems that are known to be acyclic.
virtual bool internalSolveEquations(storm::Environment const &env, OptimizationDirection d, std::vector< ValueType > &x, std::vector< ValueType > const &b) const override
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none, bool const &hasInitialScheduler=false) const override
Retrieves the requirements of this solver for solving equations with the current settings.
virtual void clearCache() const override
Clears the currently cached data that has been stored during previous calls of the solver.
MinMaxLinearEquationSolverRequirements & 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...
LabParser.cpp.
Definition cli.cpp:18