11template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
12template<
bool Backward>
14 std::vector<IndexType>
const* rowGroupIndices) {
15 if constexpr (TrivialRowGrouping) {
17 STORM_LOG_ASSERT(rowGroupIndices ==
nullptr,
"Row groups given, but grouping is supposed to be trivial.");
18 this->rowGroupIndices =
nullptr;
20 if (rowGroupIndices) {
21 this->rowGroupIndices = rowGroupIndices;
26 this->backwards = Backward;
27 this->hasSkippedRows =
false;
30 matrixColumns.clear();
35 if constexpr (std::is_same<ValueType, storm::Interval>::value) {
36 applyCache.hasOnlyConstants.clear();
37 applyCache.hasOnlyConstants.grow(matrix.
getRowCount());
40 if constexpr (!TrivialRowGrouping) {
41 matrixColumns.push_back(StartOfRowGroupIndicator);
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());
50 matrixColumns.push_back(StartOfRowIndicator);
52 matrixColumns.back() = StartOfRowGroupIndicator;
55 if constexpr (std::is_same<ValueType, storm::Interval>::value) {
56 matrixColumns.push_back(StartOfRowIndicator);
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());
65 applyCache.hasOnlyConstants.set(rowIndex, hasOnlyConstants);
66 matrixColumns.push_back(StartOfRowIndicator);
69 matrixColumns.push_back(StartOfRowIndicator);
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());
75 matrixColumns.push_back(StartOfRowIndicator);
81template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
83 std::vector<IndexType>
const* rowGroupIndices) {
84 setMatrix<false>(matrix, rowGroupIndices);
87template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
89 std::vector<IndexType>
const* rowGroupIndices) {
90 setMatrix<true>(matrix, rowGroupIndices);
93template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
95 for (
auto& c : matrixColumns) {
96 if (c >= StartOfRowIndicator) {
97 c &= StartOfRowGroupIndicator;
100 hasSkippedRows =
false;
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;
117 moveToEndOfRow(colIt);
118 }
else if ((*colIt & SkipNumEntriesMask) == 0) {
119 auto currColIt = colIt;
120 moveToEndOfRow(colIt);
121 *currColIt += std::distance(currColIt, colIt);
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.");
129 STORM_LOG_ASSERT(*colIt == StartOfRowGroupIndicator,
"VI Operator in invalid state.");
131 hasSkippedRows =
true;
134template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
138 setIgnoredRows<true>(useLocalRowIndices, ignore);
140 setIgnoredRows<false>(useLocalRowIndices, ignore);
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;
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.");
156 auxiliaryVector.assign(size, *initialValue);
158 auxiliaryVector.resize(size);
160 auxiliaryVectorUsedExternally =
true;
161 return auxiliaryVector;
164template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
166 auxiliaryVectorUsedExternally =
false;
169template<
typename ValueType,
bool TrivialRowGrouping,
typename SolutionType>
173 }
while (*matrixColumnIt < StartOfRowIndicator);
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;
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)) {
193 STORM_LOG_ASSERT(*matrixColumnIt >= StartOfRowIndicator,
"Undexpected state of VI operator");
195 STORM_LOG_ASSERT(*matrixColumnIt < StartOfRowGroupIndicator,
"Undexpected state of VI operator");
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>;
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 unsetIgnoredRows()
Clears all ignored rows.
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.
storm::storage::sparse::state_type IndexType
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)