Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FlexibleSparseMatrix.cpp
Go to the documentation of this file.
2
6
10
11namespace storm {
12namespace storage {
13template<typename ValueType>
14FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows), columnCount(0), nonzeroEntryCount(0) {
15 // Intentionally left empty.
16}
17
18template<typename ValueType>
19FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne, bool revertEquationSystem)
20 : data(matrix.getRowCount()),
21 columnCount(matrix.getColumnCount()),
22 nonzeroEntryCount(matrix.getNonzeroEntryCount()),
23 trivialRowGrouping(matrix.hasTrivialRowGrouping()) {
24 STORM_LOG_THROW(!revertEquationSystem || trivialRowGrouping, storm::exceptions::InvalidArgumentException, "Illegal option for creating flexible matrix.");
25
26 if (!trivialRowGrouping) {
27 rowGroupIndices = matrix.getRowGroupIndices();
28 }
29 for (index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) {
30 typename storm::storage::SparseMatrix<ValueType>::const_rows row = matrix.getRow(rowIndex);
31 reserveInRow(rowIndex, row.getNumberOfEntries());
32 for (auto const& element : row) {
33 // If the probability is zero, we skip this entry.
34 if (storm::utility::isZero(element.getValue())) {
35 if (revertEquationSystem && rowIndex == element.getColumn()) {
36 getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one<ValueType>());
37 } else {
38 continue;
39 }
40 }
41 if (setAllValuesToOne) {
42 if (revertEquationSystem && element.getColumn() == rowIndex && storm::utility::isOne(element.getValue())) {
43 continue;
44 } else {
45 getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one<ValueType>());
46 }
47 } else {
48 if (revertEquationSystem) {
49 if (element.getColumn() == rowIndex) {
50 if (storm::utility::isOne(element.getValue())) {
51 continue;
52 }
53 getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one<ValueType>() - element.getValue());
54 } else {
55 getRow(rowIndex).emplace_back(element.getColumn(), -element.getValue());
56 }
57 } else {
58 getRow(rowIndex).emplace_back(element);
59 }
60 }
61 }
62 }
63}
64
65template<typename ValueType>
67 this->data[row].reserve(numberOfElements);
68}
69
70template<typename ValueType>
74
75template<typename ValueType>
77 return this->data[index];
78}
79
80template<typename ValueType>
82 STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Invalid rowGroup.");
83 STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Invalid offset.");
84 return getRow(rowGroupIndices[rowGroup] + offset);
85}
86
87template<typename ValueType>
89 STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Invalid rowGroup.");
90 STORM_LOG_ASSERT(offset < this->getRowGroupSize(rowGroup), "Invalid offset.");
91 return getRow(rowGroupIndices[rowGroup] + offset);
92}
93
94template<typename ValueType>
95std::vector<typename FlexibleSparseMatrix<ValueType>::index_type> const& FlexibleSparseMatrix<ValueType>::getRowGroupIndices() const {
96 return rowGroupIndices;
97}
98
99template<typename ValueType>
103
104template<typename ValueType>
108
109template<typename ValueType>
113
114template<typename ValueType>
116 return rowGroupIndices.size() - 1;
117}
118
119template<typename ValueType>
121 return rowGroupIndices[group + 1] - rowGroupIndices[group];
122}
123
124template<typename ValueType>
126 ValueType sum = storm::utility::zero<ValueType>();
127 for (auto const& element : getRow(row)) {
128 sum += element.getValue();
129 }
130 return sum;
131}
132
133template<typename ValueType>
135 this->nonzeroEntryCount = 0;
136 this->columnCount = 0;
137 for (auto const& row : this->data) {
138 for (auto const& element : row) {
139 STORM_LOG_ASSERT(!storm::utility::isZero(element.getValue()), "Entry is 0.");
140 ++this->nonzeroEntryCount;
141 this->columnCount = std::max(element.getColumn() + 1, this->columnCount);
142 }
143 }
144}
145
146template<typename ValueType>
148 for (auto const& row : this->data) {
149 if (!row.empty()) {
150 return false;
151 }
152 }
153 return true;
154}
155
156template<typename ValueType>
158 return trivialRowGrouping;
159}
160
161template<typename ValueType>
163 for (uint_fast64_t rowIndex = 0; rowIndex < this->data.size(); ++rowIndex) {
164 auto& row = this->data[rowIndex];
165 if (!rowConstraint.get(rowIndex)) {
166 row.clear();
167 row.shrink_to_fit();
168 continue;
169 }
170 row_type newRow;
171 for (auto const& element : row) {
172 if (columnConstraint.get(element.getColumn())) {
173 newRow.push_back(element);
174 }
175 }
176 row = std::move(newRow);
177 }
178}
179
180template<typename ValueType>
183 STORM_LOG_ERROR_COND(this->columnCount == this->getRowCount(), "insertNewRowsAtEnd only works when the FlexibleMatrix is square but column count is "
184 << columnCount << " and row count is " << this->getRowCount());
185 // ... because otherwise assumptions break when creating the SparseMatrix and we get weird entries for some reason
186 index_type newRowsIndex = data.size();
187 for (index_type i = 0; i < numRows; i++) {
188 row_type newRow;
189 this->data.push_back(newRow);
190 }
191 this->columnCount = getRowCount();
192 return newRowsIndex;
193}
194
195template<typename ValueType>
197 uint_fast64_t numEntries = 0;
198 for (auto const& row : this->data) {
199 numEntries += row.size();
200 }
201
202 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(getRowCount(), getColumnCount(), numEntries, hasTrivialRowGrouping(),
203 hasTrivialRowGrouping() ? 0 : getRowGroupCount());
204 uint_fast64_t currRowIndex = 0;
205 auto rowGroupIndexIt = getRowGroupIndices().begin();
206 for (auto const& row : this->data) {
207 if (!hasTrivialRowGrouping()) {
208 while (currRowIndex >= *rowGroupIndexIt) {
209 matrixBuilder.newRowGroup(currRowIndex);
210 ++rowGroupIndexIt;
211 }
212 }
213 for (auto const& entry : row) {
214 matrixBuilder.addNextValue(currRowIndex, entry.getColumn(), entry.getValue());
215 }
216 ++currRowIndex;
217 }
218 // The matrix might end with one or more empty row groups
219 if (!hasTrivialRowGrouping()) {
220 while (currRowIndex >= *rowGroupIndexIt) {
221 matrixBuilder.newRowGroup(currRowIndex);
222 ++rowGroupIndexIt;
223 }
224 }
225 return matrixBuilder.build();
226}
227
228template<typename ValueType>
230 storm::storage::BitVector const& columnConstraint) {
231 uint_fast64_t numEntries = 0;
232 for (auto rowIndex : rowConstraint) {
233 auto const& row = data[rowIndex];
234 for (auto const& entry : row) {
235 if (columnConstraint.get(entry.getColumn())) {
236 ++numEntries;
237 }
238 }
239 }
240 uint_fast64_t numRowGroups = 0;
241 if (!hasTrivialRowGrouping()) {
242 auto lastRowGroupIndexIt = getRowGroupIndices().end() - 1;
243 auto rowGroupIndexIt = getRowGroupIndices().begin();
244 while (rowGroupIndexIt != lastRowGroupIndexIt) {
245 // Check whether the rowGroup will be nonempty
246 if (rowConstraint.getNextSetIndex(*rowGroupIndexIt) < *(++rowGroupIndexIt)) {
247 ++numRowGroups;
248 }
249 }
250 }
251
252 std::vector<uint_fast64_t> oldToNewColumnIndexMapping(getColumnCount(), getColumnCount());
253 uint_fast64_t newColumnIndex = 0;
254 for (auto oldColumnIndex : columnConstraint) {
255 oldToNewColumnIndexMapping[oldColumnIndex] = newColumnIndex++;
256 }
257
258 storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, !hasTrivialRowGrouping(),
259 numRowGroups);
260 uint_fast64_t currRowIndex = 0;
261 auto rowGroupIndexIt = getRowGroupIndices().begin();
262 for (auto oldRowIndex : rowConstraint) {
263 if (!hasTrivialRowGrouping() && oldRowIndex >= *rowGroupIndexIt) {
264 matrixBuilder.newRowGroup(currRowIndex);
265 // Skip empty row groups
266 do {
267 ++rowGroupIndexIt;
268 } while (oldRowIndex >= *rowGroupIndexIt);
269 }
270 auto const& row = data[oldRowIndex];
271 for (auto const& entry : row) {
272 if (columnConstraint.get(entry.getColumn())) {
273 matrixBuilder.addNextValue(currRowIndex, oldToNewColumnIndexMapping[entry.getColumn()], entry.getValue());
274 }
275 }
276 ++currRowIndex;
277 }
278 return matrixBuilder.build();
279}
280
281template<typename ValueType>
283 for (auto const& entry : this->getRow(state)) {
284 if (entry.getColumn() < state) {
285 continue;
286 } else if (entry.getColumn() > state) {
287 return false;
288 } else if (entry.getColumn() == state) {
289 return true;
290 }
291 }
292 return false;
293}
294
295template<typename ValueType>
296std::ostream& FlexibleSparseMatrix<ValueType>::printRow(std::ostream& out, index_type const& rowIndex) const {
297 index_type columnIndex = 0;
298 row_type row = this->getRow(rowIndex);
299 for (index_type column = 0; column < this->getColumnCount(); ++column) {
300 if (columnIndex < row.size() && row[columnIndex].getColumn() == column) {
301 // Insert entry
302 out << row[columnIndex].getValue() << "\t";
303 ++columnIndex;
304 } else {
305 // Insert zero
306 out << "0\t";
307 }
308 }
309 return out;
310}
311
312template<typename ValueType>
313std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<ValueType> const& matrix) {
314 typedef typename FlexibleSparseMatrix<ValueType>::index_type FlexibleIndex;
315
316 // Print column numbers in header.
317 out << "\t\t";
318 for (FlexibleIndex i = 0; i < matrix.getColumnCount(); ++i) {
319 out << i << "\t";
320 }
321 out << '\n';
322
323 if (!matrix.hasTrivialRowGrouping()) {
324 // Iterate over all row groups
325 FlexibleIndex rowGroupCount = matrix.getRowGroupCount();
326 for (FlexibleIndex rowGroup = 0; rowGroup < rowGroupCount; ++rowGroup) {
327 out << "\t---- group " << rowGroup << "/" << (rowGroupCount - 1) << " ---- \n";
328 FlexibleIndex endRow = matrix.rowGroupIndices[rowGroup + 1];
329 // Iterate over all rows.
330 for (FlexibleIndex row = matrix.rowGroupIndices[rowGroup]; row < endRow; ++row) {
331 // Print the actual row.
332 out << rowGroup << "\t(\t";
333 matrix.printRow(out, row);
334 out << "\t)\t" << rowGroup << '\n';
335 }
336 }
337
338 } else {
339 // Iterate over all rows
340 for (FlexibleIndex row = 0; row < matrix.getRowCount(); ++row) {
341 // Print the actual row.
342 out << row << "\t(\t";
343 matrix.printRow(out, row);
344 out << "\t)\t" << row << '\n';
345 }
346 }
347
348 // Print column numbers in footer.
349 out << "\t\t";
350 for (FlexibleIndex i = 0; i < matrix.getColumnCount(); ++i) {
351 out << i << "\t";
352 }
353 out << '\n';
354 return out;
355}
356
357// Explicitly instantiate the matrix.
358template class FlexibleSparseMatrix<double>;
359template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<double> const& matrix);
360
361#ifdef STORM_HAVE_CARL
363template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<storm::RationalNumber> const& matrix);
364
366template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<storm::RationalFunction> const& matrix);
367#endif
368
369} // namespace storage
370} // namespace storm
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
bool get(uint_fast64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
The flexible sparse matrix is used during state elimination.
void reserveInRow(index_type row, index_type numberOfElements)
Reserves space for elements in row.
index_type getRowGroupSize(index_type group) const
Returns the size of the given row group.
index_type getColumnCount() const
Returns the number of columns of the matrix.
value_type getRowSum(index_type row) const
Computes the sum of the entries in a given row.
void updateDimensions()
Recomputes the number of columns and the number of non-zero entries.
index_type getNonzeroEntryCount() const
Returns the cached number of nonzero entries in the matrix.
std::ostream & printRow(std::ostream &out, index_type const &rowIndex) const
Print row.
std::vector< index_type > const & getRowGroupIndices() const
Returns the grouping of rows of this matrix.
storm::storage::SparseMatrix< ValueType > createSparseMatrix()
Creates a sparse matrix from the flexible sparse matrix.
row_type & getRow(index_type)
Returns an object representing the given row.
bool empty() const
Checks if the matrix has no elements.
void filterEntries(storm::storage::BitVector const &rowConstraint, storm::storage::BitVector const &columnConstraint)
Erases all entries whose row and column does not satisfy the given rowConstraint and the given column...
index_type getRowCount() const
Returns the number of rows of the matrix.
FlexibleSparseMatrix()=default
Constructs an empty flexible sparse matrix.
bool hasTrivialRowGrouping() const
Retrieves whether the matrix has a (possibly) trivial row grouping.
index_type insertNewRowsAtEnd(index_type numRows)
Inserts new, empty rows at the end of the FlexibleSparseMatrix.
bool rowHasDiagonalElement(storm::storage::sparse::state_type state)
Checks whether the given state has a self-loop with an arbitrary probability in the probability matri...
index_type getRowGroupCount() const
Returns the number of row groups in the matrix.
std::vector< storm::storage::MatrixEntry< index_type, value_type > > row_type
This class represents a number of consecutive rows of the matrix.
index_type getNumberOfEntries() const
Retrieves the number of entries in the rows.
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
void newRowGroup(index_type startingRow)
Starts a new row group in the matrix.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
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.
const_iterator end(index_type row) const
Retrieves an iterator that points past the end of the given row.
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.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
#define STORM_LOG_ERROR_COND(cond, message)
Definition macros.h:52
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::ostream & operator<<(std::ostream &out, ParameterRegion< ParametricType > const &region)
bool isOne(ValueType const &a)
Definition constants.cpp:36
bool isZero(ValueType const &a)
Definition constants.cpp:41
LabParser.cpp.
Definition cli.cpp:18