Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ValueIterationOperator.cpp
Go to the documentation of this file.
2
3#include <optional>
4
8
9namespace storm::solver::helper {
10
11template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
12template<bool Backward>
14 std::vector<IndexType> const* rowGroupIndices) {
15 if constexpr (TrivialRowGrouping) {
16 STORM_LOG_ASSERT(matrix.hasTrivialRowGrouping(), "Expected a matrix with trivial row grouping");
17 STORM_LOG_ASSERT(rowGroupIndices == nullptr, "Row groups given, but grouping is supposed to be trivial.");
18 this->rowGroupIndices = nullptr;
19 } else {
20 if (rowGroupIndices) {
21 this->rowGroupIndices = rowGroupIndices;
22 } else {
23 this->rowGroupIndices = &matrix.getRowGroupIndices();
24 }
25 }
26 this->backwards = Backward;
27 this->hasSkippedRows = false;
28 auto const numRows = matrix.getRowCount();
29 matrixValues.clear();
30 matrixColumns.clear();
31 matrixValues.reserve(matrix.getNonzeroEntryCount());
32 matrixColumns.reserve(matrix.getNonzeroEntryCount() + numRows + 1); // matrixColumns also contain indications for when a row(group) starts
33
34 // hasOnlyConstants is only used for Interval matrices, currently only populated for iMCs
35 if constexpr (std::is_same<ValueType, storm::Interval>::value) {
36 applyCache.hasOnlyConstants.clear();
37 applyCache.hasOnlyConstants.grow(matrix.getRowCount());
38 }
39
40 if constexpr (!TrivialRowGrouping) {
41 matrixColumns.push_back(StartOfRowGroupIndicator); // indicate start of first row(group)
42 for (auto groupIndex : indexRange<Backward>(0, this->rowGroupIndices->size() - 1)) {
43 STORM_LOG_ASSERT(this->rowGroupIndices->at(groupIndex) != this->rowGroupIndices->at(groupIndex + 1),
44 "There is an empty row group. This is not expected.");
45 for (auto rowIndex : indexRange<false>((*this->rowGroupIndices)[groupIndex], (*this->rowGroupIndices)[groupIndex + 1])) {
46 for (auto const& entry : matrix.getRow(rowIndex)) {
47 matrixValues.push_back(entry.getValue());
48 matrixColumns.push_back(entry.getColumn());
49 }
50 matrixColumns.push_back(StartOfRowIndicator); // Indicate start of next row
51 }
52 matrixColumns.back() = StartOfRowGroupIndicator; // This is the start of the next row group
53 }
54 } else {
55 if constexpr (std::is_same<ValueType, storm::Interval>::value) {
56 matrixColumns.push_back(StartOfRowIndicator); // Indicate start of first row
57 for (auto rowIndex : indexRange<Backward>(0, numRows)) {
58 bool hasOnlyConstants = true;
59 for (auto const& entry : matrix.getRow(rowIndex)) {
60 ValueType value = entry.getValue();
61 hasOnlyConstants &= value.upper() == value.lower();
62 matrixValues.push_back(value);
63 matrixColumns.push_back(entry.getColumn());
64 }
65 applyCache.hasOnlyConstants.set(rowIndex, hasOnlyConstants);
66 matrixColumns.push_back(StartOfRowIndicator); // Indicate start of next row
67 }
68 } else {
69 matrixColumns.push_back(StartOfRowIndicator); // Indicate start of first row
70 for (auto rowIndex : indexRange<Backward>(0, numRows)) {
71 for (auto const& entry : matrix.getRow(rowIndex)) {
72 matrixValues.push_back(entry.getValue());
73 matrixColumns.push_back(entry.getColumn());
74 }
75 matrixColumns.push_back(StartOfRowIndicator); // Indicate start of next row
76 }
77 }
78 }
79}
80
81template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
83 std::vector<IndexType> const* rowGroupIndices) {
84 setMatrix<false>(matrix, rowGroupIndices);
85}
86
87template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
89 std::vector<IndexType> const* rowGroupIndices) {
90 setMatrix<true>(matrix, rowGroupIndices);
91}
92
93template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
95 for (auto& c : matrixColumns) {
96 if (c >= StartOfRowIndicator) {
97 c &= StartOfRowGroupIndicator;
98 }
99 }
100 hasSkippedRows = false;
101}
102
103template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
104template<bool Backward>
106 std::function<bool(IndexType, IndexType)> const& ignore) {
107 STORM_LOG_ASSERT(!TrivialRowGrouping, "Tried to ignroe rows but the row grouping is trivial.");
108 auto colIt = matrixColumns.begin();
109 for (auto groupIndex : indexRange<Backward>(0, this->rowGroupIndices->size() - 1)) {
110 STORM_LOG_ASSERT(colIt != matrixColumns.end(), "VI Operator in invalid state.");
111 STORM_LOG_ASSERT(*colIt >= StartOfRowGroupIndicator, "VI Operator in invalid state.");
112 auto const rowIndexRange = useLocalRowIndices ? indexRange<false>(0ull, (*this->rowGroupIndices)[groupIndex + 1] - (*this->rowGroupIndices)[groupIndex])
113 : indexRange<false>((*this->rowGroupIndices)[groupIndex], (*this->rowGroupIndices)[groupIndex + 1]);
114 for (auto const rowIndex : rowIndexRange) {
115 if (!ignore(groupIndex, rowIndex)) {
116 *colIt &= StartOfRowGroupIndicator; // Clear number of skipped entries
117 moveToEndOfRow(colIt);
118 } else if ((*colIt & SkipNumEntriesMask) == 0) { // i.e. should ignore but is not already ignored
119 auto currColIt = colIt;
120 moveToEndOfRow(colIt);
121 *currColIt += std::distance(currColIt, colIt); // set number of skipped entries
122 }
124 !std::all_of(rowIndexRange.begin(), rowIndexRange.end(), [&ignore, &groupIndex](IndexType rowIndex) { return ignore(groupIndex, rowIndex); }),
125 "All rows in row group " << groupIndex << " are ignored.");
126 STORM_LOG_ASSERT(colIt != matrixColumns.end(), "VI Operator in invalid state.");
127 STORM_LOG_ASSERT(*colIt >= StartOfRowIndicator, "VI Operator in invalid state.");
128 }
129 STORM_LOG_ASSERT(*colIt == StartOfRowGroupIndicator, "VI Operator in invalid state.");
130 }
131 hasSkippedRows = true;
132}
133
134template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
136 std::function<bool(IndexType, IndexType)> const& ignore) {
137 if (backwards) {
138 setIgnoredRows<true>(useLocalRowIndices, ignore);
139 } else {
140 setIgnoredRows<false>(useLocalRowIndices, ignore);
141 }
142}
143
144template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
145std::vector<typename ValueIterationOperator<ValueType, TrivialRowGrouping, SolutionType>::IndexType> const&
147 STORM_LOG_ASSERT(!TrivialRowGrouping, "Tried to get row group indices for trivial row grouping");
148 return *rowGroupIndices;
149}
150
151template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
153 uint64_t size, std::optional<SolutionType> const& initialValue) {
154 STORM_LOG_ASSERT(!auxiliaryVectorUsedExternally, "Auxiliary vector already in use.");
155 if (initialValue) {
156 auxiliaryVector.assign(size, *initialValue);
157 } else {
158 auxiliaryVector.resize(size);
159 }
160 auxiliaryVectorUsedExternally = true;
161 return auxiliaryVector;
162}
163
164template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
168
169template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
170void ValueIterationOperator<ValueType, TrivialRowGrouping, SolutionType>::moveToEndOfRow(std::vector<IndexType>::iterator& matrixColumnIt) const {
171 do {
172 ++matrixColumnIt;
173 } while (*matrixColumnIt < StartOfRowIndicator);
174}
175
176template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
177bool ValueIterationOperator<ValueType, TrivialRowGrouping, SolutionType>::skipIgnoredRow(std::vector<IndexType>::const_iterator& matrixColumnIt,
178 typename std::vector<ValueType>::const_iterator& matrixValueIt) const {
179 if (IndexType entriesToSkip = (*matrixColumnIt & SkipNumEntriesMask)) {
180 matrixColumnIt += entriesToSkip;
181 matrixValueIt += entriesToSkip - 1;
182 return true;
183 }
184 return false;
185}
186
187template<typename ValueType, bool TrivialRowGrouping, typename SolutionType>
188uint64_t ValueIterationOperator<ValueType, TrivialRowGrouping, SolutionType>::skipMultipleIgnoredRows(
189 std::vector<IndexType>::const_iterator& matrixColumnIt, typename std::vector<ValueType>::const_iterator& matrixValueIt) const {
190 IndexType result{0ull};
191 while (skipIgnoredRow(matrixColumnIt, matrixValueIt)) {
192 ++result;
193 STORM_LOG_ASSERT(*matrixColumnIt >= StartOfRowIndicator, "Undexpected state of VI operator");
194 // We (currently) don't use this past the end of a row group, so we may have this additional sanity check:
195 STORM_LOG_ASSERT(*matrixColumnIt < StartOfRowGroupIndicator, "Undexpected state of VI operator");
196 }
197 return result;
198}
199
200template class ValueIterationOperator<double, true>;
201template class ValueIterationOperator<double, false>;
202template class ValueIterationOperator<storm::RationalNumber, true>;
203template class ValueIterationOperator<storm::RationalNumber, false>;
204template class ValueIterationOperator<storm::Interval, true, double>;
205template class ValueIterationOperator<storm::Interval, false, double>;
206
207} // namespace storm::solver::helper
This class represents the Value Iteration Operator (also known as Bellman operator).
std::vector< SolutionType > & allocateAuxiliaryVector(uint64_t size, std::optional< SolutionType > const &initialValue={})
Allocates additional storage that can be used e.g.
void setIgnoredRows(bool useLocalRowIndices, std::function< bool(IndexType, IndexType)> const &ignore)
Sets rows that will be skipped when applying the operator.
std::vector< IndexType > const & getRowGroupIndices() const
void setMatrix(storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< IndexType > const *rowGroupIndices=nullptr)
Initializes this operator with the given data.
void freeAuxiliaryVector()
Clears the auxiliary vector, invalidating any references to it.
void setMatrixForwards(storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< IndexType > const *rowGroupIndices=nullptr)
Initializes this operator with the given data for forward iterations (starting with the smallest row ...
void setMatrixBackwards(storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< IndexType > const *rowGroupIndices=nullptr)
Initializes this operator with the given data for backward iterations (starting with the largest row ...
A class that holds a possibly non-square matrix in the compressed row storage format.
const_rows getRow(index_type row) const
Returns an object representing the given row.
bool hasTrivialRowGrouping() const
Retrieves whether the matrix has a trivial row grouping.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
index_type getRowCount() const
Returns the number of rows of the matrix.
index_type getNonzeroEntryCount() const
Returns the cached number of nonzero entries in the matrix.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11