From ab5810355578f83e92c6863c512c58a7ab4115eb Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 4 Sep 2014 21:20:42 +0200 Subject: [PATCH] Started to pimp matrix. First step: added proper methods setColumn/setValue that operate on a matrix entry and removed the non-const versions of getColumn/getValue. Added a typedef for the index type in the matrix so that it becomes possible to have matrices with a different index type (e.g. 32-bit values). Former-commit-id: 3cc0fdf9ee6fb5889c5f92bebb91e906374cd714 --- .../SparseMarkovAutomatonCslModelChecker.h | 6 +- src/models/MarkovAutomaton.h | 2 +- src/storage/SparseMatrix.cpp | 492 +++++++++--------- src/storage/SparseMatrix.h | 185 ++++--- src/storage/dd/CuddDd.cpp | 8 +- src/storage/dd/CuddDd.h | 2 +- test/functional/storage/SparseMatrixTest.cpp | 2 +- 7 files changed, 362 insertions(+), 335 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index fc1138b21..56b36ac37 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -149,9 +149,9 @@ namespace storm { for (auto& element : aMarkovian.getRow(rowIndex)) { ValueType eTerm = std::exp(-exitRates[state] * delta); if (element.getColumn() == rowIndex) { - element.getValue() = (storm::utility::constantOne() - eTerm) * element.getValue() + eTerm; + element.setValue((storm::utility::constantOne() - eTerm) * element.getValue() + eTerm); } else { - element.getValue() = (storm::utility::constantOne() - eTerm) * element.getValue(); + element.setValue((storm::utility::constantOne() - eTerm) * element.getValue()); } } ++rowIndex; @@ -161,7 +161,7 @@ namespace storm { rowIndex = 0; for (auto state : markovianNonGoalStates) { for (auto& element : aMarkovianToProbabilistic.getRow(rowIndex)) { - element.getValue() = (1 - std::exp(-exitRates[state] * delta)) * element.getValue(); + element.setValue((1 - std::exp(-exitRates[state] * delta)) * element.getValue()); } ++rowIndex; } diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 387590df6..8f5825d6d 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -259,7 +259,7 @@ namespace storm { void turnRatesToProbabilities() { for (auto state : this->markovianStates) { for (auto& transition : this->transitionMatrix.getRowGroup(state)) { - transition.getValue() /= this->exitRates[state]; + transition.setValue(transition.getValue() / this->exitRates[state]); } } } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index e03909703..c4ac671df 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -17,48 +17,48 @@ extern log4cplus::Logger logger; namespace storm { namespace storage { - template - MatrixEntry::MatrixEntry(uint_fast64_t column, T value) : entry(column, value) { + template + MatrixEntry::MatrixEntry(IndexType column, ValueType value) : entry(column, value) { // Intentionally left empty. } - template - MatrixEntry::MatrixEntry(std::pair&& pair) : entry(std::move(pair)) { + template + MatrixEntry::MatrixEntry(std::pair&& pair) : entry(std::move(pair)) { // Intentionally left empty. } - template - uint_fast64_t const& MatrixEntry::getColumn() const { + template + IndexType const& MatrixEntry::getColumn() const { return this->entry.first; } - template - uint_fast64_t& MatrixEntry::getColumn() { - return this->entry.first; + template + void MatrixEntry::setColumn(IndexType const& column) { + this->entry.first = column; } - template - T const& MatrixEntry::getValue() const { + template + ValueType const& MatrixEntry::getValue() const { return this->entry.second; } - template - T& MatrixEntry::getValue() { - return this->entry.second; + template + void MatrixEntry::setValue(ValueType const& value) { + this->entry.second = value; } - - template - std::pair const& MatrixEntry::getColumnValuePair() const { + + template + std::pair const& MatrixEntry::getColumnValuePair() const { return this->entry; } - template - SparseMatrixBuilder::SparseMatrixBuilder(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries, bool hasCustomRowGrouping, uint_fast64_t rowGroups) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), hasCustomRowGrouping(hasCustomRowGrouping), rowGroupCountSet(rowGroups != 0), rowGroupCount(rowGroups), rowGroupIndices(), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), currentRowGroup(0) { + template + SparseMatrixBuilder::SparseMatrixBuilder(IndexType rows, IndexType columns, IndexType entries, bool hasCustomRowGrouping, IndexType rowGroups) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), hasCustomRowGrouping(hasCustomRowGrouping), rowGroupCountSet(rowGroups != 0), rowGroupCount(rowGroups), rowGroupIndices(), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), currentRowGroup(0) { this->prepareInternalStorage(); } - template - void SparseMatrixBuilder::addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value) { + template + void SparseMatrixBuilder::addNextValue(IndexType row, IndexType column, ValueType const& value) { // Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat // differently. if (storagePreallocated) { @@ -94,18 +94,18 @@ namespace storm { if (storagePreallocated) { // If the storage was preallocated, we can access the elements in the vectors with the subscript // operator. - for (uint_fast64_t i = lastRow + 1; i <= row; ++i) { + for (IndexType i = lastRow + 1; i <= row; ++i) { rowIndications[i] = currentEntryCount; } } else { // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations. - for (uint_fast64_t i = lastRow + 1; i <= row; ++i) { + for (IndexType i = lastRow + 1; i <= row; ++i) { rowIndications.push_back(currentEntryCount); } } if (!hasCustomRowGrouping) { - for (uint_fast64_t i = lastRow + 1; i <= row; ++i) { + for (IndexType i = lastRow + 1; i <= row; ++i) { rowGroupIndices.push_back(i); ++currentRowGroup; } @@ -131,8 +131,8 @@ namespace storm { ++currentEntryCount; } - template - void SparseMatrixBuilder::newRowGroup(uint_fast64_t startingRow) { + template + void SparseMatrixBuilder::newRowGroup(IndexType startingRow) { if (!hasCustomRowGrouping) { throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: matrix was not created to have a custom row grouping."; } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) { @@ -146,22 +146,22 @@ namespace storm { } } - template - SparseMatrix SparseMatrixBuilder::build(uint_fast64_t overriddenRowCount, uint_fast64_t overriddenColumnCount, uint_fast64_t overriddenRowGroupCount) { + template + SparseMatrix SparseMatrixBuilder::build(IndexType overriddenRowCount, IndexType overriddenColumnCount, IndexType overriddenRowGroupCount) { // Check whether it's safe to finalize the matrix and throw error otherwise. if (storagePreallocated && currentEntryCount != entryCount) { throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::build: expected " << entryCount << " entries, but got " << currentEntryCount << " instead."; } else { // Fill in the missing entries in the row indices array, as there may be empty rows at the end. if (storagePreallocated) { - for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { + for (IndexType i = lastRow + 1; i < rowCount; ++i) { rowIndications[i] = currentEntryCount; } } else { if (!rowCountSet) { rowCount = std::max(overriddenRowCount, rowCount); } - for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { + for (IndexType i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); } } @@ -184,27 +184,27 @@ namespace storm { rowGroupIndices[rowGroupCount] = rowCount; } else { if (!hasCustomRowGrouping) { - for (uint_fast64_t i = currentRowGroup; i < rowCount; ++i) { + for (IndexType i = currentRowGroup; i < rowCount; ++i) { rowGroupIndices.push_back(i + 1); } } else { overriddenRowGroupCount = std::max(overriddenRowGroupCount, currentRowGroup + 1); - for (uint_fast64_t i = currentRowGroup; i < overriddenRowGroupCount; ++i) { + for (IndexType i = currentRowGroup; i < overriddenRowGroupCount; ++i) { rowGroupIndices.push_back(rowCount); } } } } - return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } - template - void SparseMatrixBuilder::prepareInternalStorage() { + template + void SparseMatrixBuilder::prepareInternalStorage() { // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known. if (storagePreallocated) { - columnsAndValues = std::vector>(entryCount, MatrixEntry(0, storm::utility::constantZero())); - rowIndications = std::vector(rowCount + 1, 0); + columnsAndValues = std::vector>(entryCount, MatrixEntry(0, storm::utility::constantZero())); + rowIndications = std::vector(rowCount + 1, 0); } else { rowIndications.push_back(0); } @@ -212,7 +212,7 @@ namespace storm { // Only allocate the memory for the row grouping of the matrix contents if the number of groups is already // known. if (hasCustomRowGrouping && rowGroupCountSet) { - rowGroupIndices = std::vector(rowGroupCount + 1, 0); + rowGroupIndices = std::vector(rowGroupCount + 1, 0); } else { if (hasCustomRowGrouping) { // Nothing to do in this case @@ -222,74 +222,84 @@ namespace storm { } } - template - SparseMatrix::rows::rows(iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) { + template + SparseMatrix::rows::rows(iterator begin, IndexType entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } - template - typename SparseMatrix::iterator SparseMatrix::rows::begin() { + template + typename SparseMatrix::iterator SparseMatrix::rows::begin() { return beginIterator; } - template - typename SparseMatrix::iterator SparseMatrix::rows::end() { + template + typename SparseMatrix::iterator SparseMatrix::rows::end() { return beginIterator + entryCount; } - template - SparseMatrix::const_rows::const_rows(const_iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) { + template + typename SparseMatrix::IndexType SparseMatrix::rows::getNumberOfEntries() const { + return this->entryCount; + } + + template + SparseMatrix::const_rows::const_rows(const_iterator begin, IndexType entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } - template - typename SparseMatrix::const_iterator SparseMatrix::const_rows::begin() const { + template + typename SparseMatrix::const_iterator SparseMatrix::const_rows::begin() const { return beginIterator; } - template - typename SparseMatrix::const_iterator SparseMatrix::const_rows::end() const { + template + typename SparseMatrix::const_iterator SparseMatrix::const_rows::end() const { return beginIterator + entryCount; } - template - SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { + template + typename SparseMatrix::IndexType SparseMatrix::const_rows::getNumberOfEntries() const { + return this->entryCount; + } + + template + SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), nonzeroEntryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() { // Intentionally left empty. } - template - SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) { + template + SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. } - template - SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), rowGroupIndices(std::move(other.rowGroupIndices)) { + template + SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), rowGroupIndices(std::move(other.rowGroupIndices)) { // Now update the source matrix other.rowCount = 0; other.columnCount = 0; other.entryCount = 0; } - template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { + template + SparseMatrix::SparseMatrix(IndexType columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) { for (auto const& element : *this) { - if (element.getValue() != storm::utility::constantZero()) { + if (element.getValue() != storm::utility::constantZero()) { ++this->nonzeroEntryCount; } } } - template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { + template + SparseMatrix::SparseMatrix(IndexType columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) { for (auto const& element : *this) { - if (element.getValue() != storm::utility::constantZero()) { + if (element.getValue() != storm::utility::constantZero()) { ++this->nonzeroEntryCount; } } } - template - SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { + template + SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { // Only perform assignment if source and target are not the same. if (this != &other) { rowCount = other.rowCount; @@ -305,8 +315,8 @@ namespace storm { return *this; } - template - SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { + template + SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { // Only perform assignment if source and target are not the same. if (this != &other) { rowCount = other.rowCount; @@ -322,8 +332,8 @@ namespace storm { return *this; } - template - bool SparseMatrix::operator==(SparseMatrix const& other) const { + template + bool SparseMatrix::operator==(SparseMatrix const& other) const { if (this == &other) { return true; } @@ -336,13 +346,13 @@ namespace storm { // For the actual contents, we need to do a little bit more work, because we want to ignore elements that // are set to zero, please they may be represented implicitly in the other matrix. - for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { + for (IndexType row = 0; row < this->getRowCount(); ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = other.begin(row), ite2 = other.end(row); it1 != ite1 && it2 != ite2; ++it1, ++it2) { // Skip over all zero entries in both matrices. - while (it1 != ite1 && it1->getValue() == storm::utility::constantZero()) { + while (it1 != ite1 && it1->getValue() == storm::utility::constantZero()) { ++it1; } - while (it2 != ite2 && it2->getValue() == storm::utility::constantZero()) { + while (it2 != ite2 && it2->getValue() == storm::utility::constantZero()) { ++it2; } if ((it1 == ite1) || (it2 == ite2)) { @@ -360,59 +370,59 @@ namespace storm { return equalityResult; } - template - uint_fast64_t SparseMatrix::getRowCount() const { + template + typename SparseMatrix::IndexType SparseMatrix::getRowCount() const { return rowCount; } - template - uint_fast64_t SparseMatrix::getColumnCount() const { + template + typename SparseMatrix::IndexType SparseMatrix::getColumnCount() const { return columnCount; } - template - uint_fast64_t SparseMatrix::getEntryCount() const { + template + typename SparseMatrix::IndexType SparseMatrix::getEntryCount() const { return entryCount; } - template - uint_fast64_t SparseMatrix::getNonzeroEntryCount() const { + template + typename SparseMatrix::IndexType SparseMatrix::getNonzeroEntryCount() const { return nonzeroEntryCount; } - template - uint_fast64_t SparseMatrix::getRowGroupCount() const { + template + typename SparseMatrix::IndexType SparseMatrix::getRowGroupCount() const { return rowGroupIndices.size() - 1; } - template - uint_fast64_t SparseMatrix::getRowGroupSize(uint_fast64_t group) const { + template + typename SparseMatrix::IndexType SparseMatrix::getRowGroupSize(IndexType group) const { return this->getRowGroupIndices()[group + 1] - this->getRowGroupIndices()[group]; } - template - std::vector const& SparseMatrix::getRowGroupIndices() const { + template + std::vector::IndexType> const& SparseMatrix::getRowGroupIndices() const { return rowGroupIndices; } - template - void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { + template + void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { for (auto row : rows) { makeRowDirac(row, row); } } - template - void SparseMatrix::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint) { + template + void SparseMatrix::makeRowGroupsAbsorbing(storm::storage::BitVector const& rowGroupConstraint) { for (auto rowGroup : rowGroupConstraint) { - for (uint_fast64_t row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) { + for (IndexType row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) { makeRowDirac(row, rowGroup); } } } - template - void SparseMatrix::makeRowDirac(uint_fast64_t row, uint_fast64_t column) { + template + void SparseMatrix::makeRowDirac(IndexType row, IndexType column) { iterator columnValuePtr = this->begin(row); iterator columnValuePtrEnd = this->end(row); @@ -424,18 +434,18 @@ namespace storm { // If there is at least one entry in this row, we can just set it to one, modify its column value to the // one given by the parameter and set all subsequent elements of this row to zero. - columnValuePtr->getColumn() = column; - columnValuePtr->getValue() = storm::utility::constantOne(); + columnValuePtr->setColumn(column); + columnValuePtr->setValue(storm::utility::constantOne()); ++columnValuePtr; for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { - columnValuePtr->getColumn() = 0; - columnValuePtr->getValue() = storm::utility::constantZero(); + columnValuePtr->setColumn(0); + columnValuePtr->setValue(storm::utility::constantZero()); } } - template - T SparseMatrix::getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& constraint) const { - T result(0); + template + ValueType SparseMatrix::getConstrainedRowSum(IndexType row, storm::storage::BitVector const& constraint) const { + ValueType result = storm::utility::constantZero(); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { if (constraint.get(it->getColumn())) { result += it->getValue(); @@ -444,51 +454,51 @@ namespace storm { return result; } - template - std::vector SparseMatrix::getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const { - std::vector result(rowConstraint.getNumberOfSetBits()); - uint_fast64_t currentRowCount = 0; + template + std::vector SparseMatrix::getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const { + std::vector result(rowConstraint.getNumberOfSetBits()); + IndexType currentRowCount = 0; for (auto row : rowConstraint) { result[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); } return result; } - template - std::vector SparseMatrix::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const { - std::vector result; + template + std::vector SparseMatrix::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const { + std::vector result; result.reserve(rowGroupConstraint.getNumberOfSetBits()); for (auto rowGroup : rowGroupConstraint) { - for (uint_fast64_t row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) { + for (IndexType row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) { result.push_back(getConstrainedRowSum(row, columnConstraint)); } } return result; } - template - SparseMatrix SparseMatrix::getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalElements) const { + template + SparseMatrix SparseMatrix::getSubmatrix(bool useGroups, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalElements) const { if (useGroups) { return getSubmatrix(rowConstraint, columnConstraint, this->getRowGroupIndices(), insertDiagonalElements); } else { // Create a fake row grouping to reduce this to a call to a more general method. - std::vector fakeRowGroupIndices(rowCount + 1); - uint_fast64_t i = 0; - for (std::vector::iterator it = fakeRowGroupIndices.begin(); it != fakeRowGroupIndices.end(); ++it, ++i) { + std::vector fakeRowGroupIndices(rowCount + 1); + IndexType i = 0; + for (std::vector::iterator it = fakeRowGroupIndices.begin(); it != fakeRowGroupIndices.end(); ++it, ++i) { *it = i; } return getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements); } } - template - SparseMatrix SparseMatrix::getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries) const { + template + SparseMatrix SparseMatrix::getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries) const { // First, we need to determine the number of entries and the number of rows of the submatrix. - uint_fast64_t subEntries = 0; - uint_fast64_t subRows = 0; + IndexType subEntries = 0; + IndexType subRows = 0; for (auto index : rowGroupConstraint) { subRows += rowGroupIndices[index + 1] - rowGroupIndices[index]; - for (uint_fast64_t i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { + for (IndexType i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { bool foundDiagonalElement = false; for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { @@ -509,16 +519,16 @@ namespace storm { } // Create and initialize resulting matrix. - SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true); + SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true); // Create a temporary vector that stores for each index whose bit is set to true the number of bits that // were set before that particular index. - std::vector bitsSetBeforeIndex; + std::vector bitsSetBeforeIndex; bitsSetBeforeIndex.reserve(columnCount); // Compute the information to fill this vector. - uint_fast64_t lastIndex = 0; - uint_fast64_t currentNumberOfSetBits = 0; + IndexType lastIndex = 0; + IndexType currentNumberOfSetBits = 0; // If we are requested to add missing diagonal entries, we need to make sure the corresponding rows are also // taken. @@ -535,10 +545,10 @@ namespace storm { } // Copy over selected entries. - uint_fast64_t rowCount = 0; + IndexType rowCount = 0; for (auto index : rowGroupConstraint) { matrixBuilder.newRowGroup(rowCount); - for (uint_fast64_t i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { + for (IndexType i = rowGroupIndices[index]; i < rowGroupIndices[index + 1]; ++i) { bool insertedDiagonalElement = false; for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) { @@ -546,14 +556,14 @@ namespace storm { if (index == it->getColumn()) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > index) { - matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); + matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); insertedDiagonalElement = true; } matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[it->getColumn()], it->getValue()); } } if (insertDiagonalEntries && !insertedDiagonalElement) { - matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); + matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); } ++rowCount; @@ -563,14 +573,14 @@ namespace storm { return matrixBuilder.build(); } - template - SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { + template + SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for // diagonal entries if requested. - uint_fast64_t subEntries = 0; - for (uint_fast64_t rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { + IndexType subEntries = 0; + for (IndexType rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { // Determine which row we need to select from the current row group. - uint_fast64_t rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; + IndexType rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; // Iterate through that row and count the number of slots we have to reserve for copying. bool foundDiagonalElement = false; @@ -586,12 +596,12 @@ namespace storm { } // Now create the matrix to be returned with the appropriate size. - SparseMatrixBuilder matrixBuilder(rowGroupIndices.size() - 1, columnCount, subEntries); + SparseMatrixBuilder matrixBuilder(rowGroupIndices.size() - 1, columnCount, subEntries); // Copy over the selected lines from the source matrix. - for (uint_fast64_t rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { + for (IndexType rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { // Determine which row we need to select from the current row group. - uint_fast64_t rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; + IndexType rowToCopy = rowGroupIndices[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; // Iterate through that row and copy the entries. This also inserts a zero element on the diagonal if // there is no entry yet. @@ -600,13 +610,13 @@ namespace storm { if (it->getColumn() == rowGroupIndex) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > rowGroupIndex) { - matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); + matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); insertedDiagonalElement = true; } matrixBuilder.addNextValue(rowGroupIndex, it->getColumn(), it->getValue()); } if (insertDiagonalEntries && !insertedDiagonalElement) { - matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); + matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); } } @@ -614,70 +624,70 @@ namespace storm { return matrixBuilder.build(); } - template - SparseMatrix SparseMatrix::transpose(bool joinGroups) const { - uint_fast64_t rowCount = this->getColumnCount(); - uint_fast64_t columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount(); - uint_fast64_t entryCount = this->getEntryCount(); + template + SparseMatrix SparseMatrix::transpose(bool joinGroups) const { + IndexType rowCount = this->getColumnCount(); + IndexType columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount(); + IndexType entryCount = this->getEntryCount(); - std::vector rowIndications(rowCount + 1); - std::vector> columnsAndValues(entryCount); + std::vector rowIndications(rowCount + 1); + std::vector> columnsAndValues(entryCount); // First, we need to count how many entries each column has. - for (uint_fast64_t group = 0; group < columnCount; ++group) { + for (IndexType group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { - if (transition.getValue() != storm::utility::constantZero()) { + if (transition.getValue() != storm::utility::constantZero()) { ++rowIndications[transition.getColumn() + 1]; } } } // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < rowCount + 1; ++i) { + for (IndexType i = 1; i < rowCount + 1; ++i) { rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; } // Create an array that stores the index for the next value to be added for // each row in the transposed matrix. Initially this corresponds to the previously // computed accumulated offsets. - std::vector nextIndices = rowIndications; + std::vector nextIndices = rowIndications; // Now we are ready to actually fill in the values of the transposed matrix. - for (uint_fast64_t group = 0; group < columnCount; ++group) { + for (IndexType group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { - if (transition.getValue() != storm::utility::constantZero()) { + if (transition.getValue() != storm::utility::constantZero()) { columnsAndValues[nextIndices[transition.getColumn()]] = std::make_pair(group, transition.getValue()); nextIndices[transition.getColumn()]++; } } } - std::vector rowGroupIndices(rowCount + 1); - for (uint_fast64_t i = 0; i <= rowCount; ++i) { + std::vector rowGroupIndices(rowCount + 1); + for (IndexType i = 0; i <= rowCount; ++i) { rowGroupIndices[i] = i; } - storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); return transposedMatrix; } - template - void SparseMatrix::convertToEquationSystem() { + template + void SparseMatrix::convertToEquationSystem() { invertDiagonal(); negateAllNonDiagonalEntries(); } - template - void SparseMatrix::invertDiagonal() { + template + void SparseMatrix::invertDiagonal() { // Now iterate over all row groups and set the diagonal elements to the inverted value. // If there is a row without the diagonal element, an exception is thrown. - T one = storm::utility::constantOne(); + ValueType one = storm::utility::constantOne(); bool foundDiagonalElement = false; - for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { + for (IndexType group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() == group) { - entry.getValue() = one - entry.getValue(); + entry.setValue(one - entry.getValue()); foundDiagonalElement = true; } } @@ -689,46 +699,46 @@ namespace storm { } } - template - void SparseMatrix::negateAllNonDiagonalEntries() { + template + void SparseMatrix::negateAllNonDiagonalEntries() { // Iterate over all row groups and negate all the elements that are not on the diagonal. - for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { + for (IndexType group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() != group) { - entry.getValue() = -entry.getValue(); + entry.setValue(-entry.getValue()); } } } } - template - void SparseMatrix::deleteDiagonalEntries() { + template + void SparseMatrix::deleteDiagonalEntries() { // Iterate over all rows and negate all the elements that are not on the diagonal. - for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { + for (IndexType group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() == group) { - entry.getValue() = storm::utility::constantZero(); + entry.setValue(storm::utility::constantZero()); } } } } - template - typename std::pair, storm::storage::SparseMatrix> SparseMatrix::getJacobiDecomposition() const { + template + typename std::pair, storm::storage::SparseMatrix> SparseMatrix::getJacobiDecomposition() const { if (rowCount != columnCount) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; } - storm::storage::SparseMatrix resultLU(*this); + storm::storage::SparseMatrix resultLU(*this); resultLU.deleteDiagonalEntries(); - SparseMatrixBuilder dInvBuilder(rowCount, columnCount, rowCount); + SparseMatrixBuilder dInvBuilder(rowCount, columnCount, rowCount); // Copy entries to the appropriate matrices. - for (uint_fast64_t rowNumber = 0; rowNumber < rowCount; ++rowNumber) { + for (IndexType rowNumber = 0; rowNumber < rowCount; ++rowNumber) { // Because the matrix may have several entries on the diagonal, we need to sum them before we are able // to invert the entry. - T diagonalValue = storm::utility::constantZero(); + ValueType diagonalValue = storm::utility::constantZero(); for (const_iterator it = this->begin(rowNumber), ite = this->end(rowNumber); it != ite; ++it) { if (it->getColumn() == rowNumber) { diagonalValue += it->getValue(); @@ -736,20 +746,20 @@ namespace storm { break; } } - dInvBuilder.addNextValue(rowNumber, rowNumber, storm::utility::constantOne() / diagonalValue); + dInvBuilder.addNextValue(rowNumber, rowNumber, storm::utility::constantOne() / diagonalValue); } return std::make_pair(std::move(resultLU), dInvBuilder.build()); } - template - std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { - std::vector result(rowCount, storm::utility::constantZero()); + template + std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { + std::vector result(rowCount, storm::utility::constantZero()); // Iterate over all elements of the current matrix and either continue with the next element in case the // given matrix does not have a non-zero element at this column position, or multiply the two entries and // add the result to the corresponding position in the vector. - for (uint_fast64_t row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) { + for (IndexType row = 0; row < rowCount && row < otherMatrix.rowCount; ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = otherMatrix.begin(row), ite2 = otherMatrix.end(row); it1 != ite1 && it2 != ite2; ++it1) { if (it1->getColumn() < it2->getColumn()) { continue; @@ -767,8 +777,8 @@ namespace storm { } - template - void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { + template + void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB if (this->getNonzeroEntryCount() > 10000) { return this->multiplyWithVectorParallel(vector, result); @@ -780,16 +790,16 @@ namespace storm { #endif } - template - void SparseMatrix::multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const { + template + void SparseMatrix::multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const { const_iterator it = this->begin(); const_iterator ite; - typename std::vector::const_iterator rowIterator = rowIndications.begin(); - typename std::vector::iterator resultIterator = result.begin(); - typename std::vector::iterator resultIteratorEnd = result.end(); + typename std::vector::const_iterator rowIterator = rowIndications.begin(); + typename std::vector::iterator resultIterator = result.begin(); + typename std::vector::iterator resultIteratorEnd = result.end(); for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { - *resultIterator = storm::utility::constantZero(); + *resultIterator = storm::utility::constantZero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { *resultIterator += it->getValue() * vector[it->getColumn()]; @@ -798,21 +808,21 @@ namespace storm { } #ifdef STORM_HAVE_INTELTBB - template - void SparseMatrix::multiplyWithVectorParallel(std::vector const& vector, std::vector& result) const { - tbb::parallel_for(tbb::blocked_range(0, result.size(), 10), - [&] (tbb::blocked_range const& range) { - uint_fast64_t startRow = range.begin(); - uint_fast64_t endRow = range.end(); + template + void SparseMatrix::multiplyWithVectorParallel(std::vector const& vector, std::vector& result) const { + tbb::parallel_for(tbb::blocked_range(0, result.size(), 10), + [&] (tbb::blocked_range const& range) { + IndexType startRow = range.begin(); + IndexType endRow = range.end(); const_iterator it = this->begin(startRow); const_iterator ite; - std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; - std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; - typename std::vector::iterator resultIterator = result.begin() + startRow; - typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; + std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; + std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; + typename std::vector::iterator resultIterator = result.begin() + startRow; + typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { - *resultIterator = storm::utility::constantZero(); + *resultIterator = storm::utility::constantZero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { *resultIterator += it->getValue() * vector[it->getColumn()]; @@ -822,12 +832,12 @@ namespace storm { } #endif - template - uint_fast64_t SparseMatrix::getSizeInMemory() const { + template + uint_fast64_t SparseMatrix::getSizeInMemory() const { uint_fast64_t size = sizeof(*this); // Add size of columns and values. - size += sizeof(MatrixEntry) * columnsAndValues.capacity(); + size += sizeof(MatrixEntry) * columnsAndValues.capacity(); // Add row_indications size. size += sizeof(uint_fast64_t) * rowIndications.capacity(); @@ -835,84 +845,84 @@ namespace storm { return size; } - template - typename SparseMatrix::const_rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { + template + typename SparseMatrix::const_rows SparseMatrix::getRows(IndexType startRow, IndexType endRow) const { return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } - template - typename SparseMatrix::rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) { + template + typename SparseMatrix::rows SparseMatrix::getRows(IndexType startRow, IndexType endRow) { return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } - template - typename SparseMatrix::const_rows SparseMatrix::getRow(uint_fast64_t row) const { + template + typename SparseMatrix::const_rows SparseMatrix::getRow(IndexType row) const { return getRows(row, row); } - template - typename SparseMatrix::rows SparseMatrix::getRow(uint_fast64_t row) { + template + typename SparseMatrix::rows SparseMatrix::getRow(IndexType row) { return getRows(row, row); } - template - typename SparseMatrix::const_rows SparseMatrix::getRowGroup(uint_fast64_t rowGroup) const { + template + typename SparseMatrix::const_rows SparseMatrix::getRowGroup(IndexType rowGroup) const { return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1); } - template - typename SparseMatrix::rows SparseMatrix::getRowGroup(uint_fast64_t rowGroup) { + template + typename SparseMatrix::rows SparseMatrix::getRowGroup(IndexType rowGroup) { return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1); } - template - typename SparseMatrix::const_iterator SparseMatrix::begin(uint_fast64_t row) const { + template + typename SparseMatrix::const_iterator SparseMatrix::begin(IndexType row) const { return this->columnsAndValues.begin() + this->rowIndications[row]; } - template - typename SparseMatrix::iterator SparseMatrix::begin(uint_fast64_t row) { + template + typename SparseMatrix::iterator SparseMatrix::begin(IndexType row) { return this->columnsAndValues.begin() + this->rowIndications[row]; } - template - typename SparseMatrix::const_iterator SparseMatrix::end(uint_fast64_t row) const { + template + typename SparseMatrix::const_iterator SparseMatrix::end(IndexType row) const { return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } - template - typename SparseMatrix::iterator SparseMatrix::end(uint_fast64_t row) { + template + typename SparseMatrix::iterator SparseMatrix::end(IndexType row) { return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } - template - typename SparseMatrix::const_iterator SparseMatrix::end() const { + template + typename SparseMatrix::const_iterator SparseMatrix::end() const { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } - template - typename SparseMatrix::iterator SparseMatrix::end() { + template + typename SparseMatrix::iterator SparseMatrix::end() { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } - template - T SparseMatrix::getRowSum(uint_fast64_t row) const { - T sum = storm::utility::constantZero(); + template + ValueType SparseMatrix::getRowSum(IndexType row) const { + ValueType sum = storm::utility::constantZero(); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { sum += it->getValue(); } return sum; } - template - bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { + template + bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { // Check for matching sizes. if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false; // Check the subset property for all rows individually. - for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { + for (IndexType row = 0; row < this->getRowCount(); ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) { // Skip over all entries of the other matrix that are before the current entry in the current matrix. while (it2 != ite2 && it2->getColumn() < it1->getColumn()) { @@ -926,24 +936,24 @@ namespace storm { return true; } - template - std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { + template + std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { // Print column numbers in header. out << "\t\t"; - for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { + for (typename SparseMatrix::IndexType i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; // Iterate over all row groups. - for (uint_fast64_t group = 0; group < matrix.getRowGroupCount(); ++group) { + for (typename SparseMatrix::IndexType group = 0; group < matrix.getRowGroupCount(); ++group) { out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl; - for (uint_fast64_t i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) { - uint_fast64_t nextIndex = matrix.rowIndications[i]; + for (typename SparseMatrix::IndexType i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) { + typename SparseMatrix::IndexType nextIndex = matrix.rowIndications[i]; // Print the actual row. out << i << "\t(\t"; - uint_fast64_t currentRealIndex = 0; + typename SparseMatrix::IndexType currentRealIndex = 0; while (currentRealIndex < matrix.columnCount) { if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].getColumn()) { out << matrix.columnsAndValues[nextIndex].getValue() << "\t"; @@ -959,7 +969,7 @@ namespace storm { // Print column numbers in footer. out << "\t\t"; - for (uint_fast64_t i = 0; i < matrix.getColumnCount(); ++i) { + for (typename SparseMatrix::IndexType i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; @@ -967,8 +977,8 @@ namespace storm { return out; } - template - std::size_t SparseMatrix::hash() const { + template + std::size_t SparseMatrix::hash() const { std::size_t result = 0; boost::hash_combine(result, this->getRowCount()); @@ -982,11 +992,11 @@ namespace storm { } // Explicitly instantiate the entry, builder and the matrix. - template class MatrixEntry; + template class MatrixEntry::IndexType, double>; template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); - template class MatrixEntry; + template class MatrixEntry::IndexType, int>; template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 38b1cec9e..73c4260a8 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -30,7 +30,7 @@ namespace storm { // Forward declare matrix class. template class SparseMatrix; - template + template class MatrixEntry { public: /*! @@ -39,14 +39,14 @@ namespace storm { * @param column The column of the matrix entry. * @param value The value of the matrix entry. */ - MatrixEntry(uint_fast64_t column, T value); + MatrixEntry(IndexType column, ValueType value); /*! * Move-constructs the matrix entry fro the given column-value pair. * * @param pair The column-value pair from which to move-construct the matrix entry. */ - MatrixEntry(std::pair&& pair); + MatrixEntry(std::pair&& pair); MatrixEntry() = default; MatrixEntry(MatrixEntry const& other) = default; @@ -61,46 +61,46 @@ namespace storm { * * @return The column of the matrix entry. */ - uint_fast64_t const& getColumn() const; + IndexType const& getColumn() const; /*! - * Retrieves the column of the matrix entry. + * Sets the column of the current entry. * - * @return The column of the matrix entry. + * @param column The column to set for this entry. */ - uint_fast64_t& getColumn(); + void setColumn(IndexType const& column); /*! * Retrieves the value of the matrix entry. * * @return The value of the matrix entry. */ - T const& getValue() const; - + ValueType const& getValue() const; + /*! - * Retrieves the value of the matrix entry. + * Sets the value of the entry in the matrix. * - * @return The value of the matrix entry. + * @param value The value that is to be set for this entry. */ - T& getValue(); + void setValue(ValueType const& value); /*! * Retrieves a pair of column and value that characterizes this entry. * * @return A column-value pair that characterizes this entry. */ - std::pair const& getColumnValuePair() const; + std::pair const& getColumnValuePair() const; private: // The actual matrix entry. - std::pair entry; + std::pair entry; }; /*! * Computes the hash value of a matrix entry. */ - template - std::size_t hash_value(MatrixEntry const& matrixEntry) { + template + std::size_t hash_value(MatrixEntry const& matrixEntry) { std::size_t seed = 0; boost::hash_combine(seed, matrixEntry.getColumn()); boost::hash_combine(seed, matrixEntry.getValue()); @@ -110,9 +110,11 @@ namespace storm { /*! * A class that can be used to build a sparse matrix by adding value by value. */ - template + template class SparseMatrixBuilder { public: + typedef uint_fast64_t IndexType; + /*! * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. * @@ -124,7 +126,7 @@ namespace storm { * @param rowGroups The number of row groups of the resulting matrix. This is only relevant if the matrix * has a custom row grouping. */ - SparseMatrixBuilder(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0, bool hasCustomRowGrouping = false, uint_fast64_t rowGroups = 0); + SparseMatrixBuilder(IndexType rows = 0, IndexType columns = 0, IndexType entries = 0, bool hasCustomRowGrouping = false, IndexType rowGroups = 0); /*! * Sets the matrix entry at the given row and column to the given value. After all entries have been added, @@ -139,7 +141,7 @@ namespace storm { * @param column The column in which the matrix entry is to be set. * @param value The value that is to be set at the specified row and column. */ - void addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value); + void addNextValue(IndexType row, IndexType column, ValueType const& value); /*! * Starts a new row group in the matrix. Note that this needs to be called before any entries in the new row @@ -147,7 +149,7 @@ namespace storm { * * @param startingRow The starting row of the new row group. */ - void newRowGroup(uint_fast64_t startingRow); + void newRowGroup(IndexType startingRow); /* * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix @@ -168,7 +170,7 @@ namespace storm { * effect if the matrix has been created without the number of row groups given. By construction, the row * groups added this way will be empty. */ - SparseMatrix build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0, uint_fast64_t overriddenRowGroupCount = 0); + SparseMatrix build(IndexType overriddenRowCount = 0, IndexType overriddenColumnCount = 0, IndexType overriddenRowGroupCount = 0); private: /*! @@ -182,16 +184,16 @@ namespace storm { bool rowCountSet; // The number of rows of the matrix. - uint_fast64_t rowCount; + IndexType rowCount; // A flag indicating whether the number of columns was set upon construction. bool columnCountSet; // The number of columns of the matrix. - uint_fast64_t columnCount; + IndexType columnCount; // The number of entries in the matrix. - uint_fast64_t entryCount; + IndexType entryCount; // A flag indicating whether the builder is to construct a custom row grouping for the matrix. bool hasCustomRowGrouping; @@ -200,37 +202,37 @@ namespace storm { bool rowGroupCountSet; // The number of row groups in the matrix. - uint_fast64_t rowGroupCount; + IndexType rowGroupCount; - std::vector rowGroupIndices; + std::vector rowGroupIndices; // Stores whether the storage of the matrix was preallocated or not. bool storagePreallocated; // The storage for the columns and values of all entries in the matrix. - std::vector> columnsAndValues; + std::vector> columnsAndValues; // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. - std::vector rowIndications; + std::vector rowIndications; // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix // with preallocated storage. - uint_fast64_t currentEntryCount; + IndexType currentEntryCount; // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a // matrix. - uint_fast64_t lastRow; + IndexType lastRow; // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an // entry into a matrix. - uint_fast64_t lastColumn; + IndexType lastColumn; // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. - uint_fast64_t currentRowGroup; + IndexType currentRowGroup; }; /*! @@ -247,7 +249,7 @@ namespace storm { * It should be observed that due to the nature of the sparse matrix format, entries can only be inserted in * order, i.e. row by row and column by column. */ - template + template class SparseMatrix { public: // Declare adapter classes as friends to use internal data. @@ -255,8 +257,9 @@ namespace storm { friend class storm::adapters::EigenAdapter; friend class storm::adapters::StormAdapter; - typedef typename std::vector>::iterator iterator; - typedef typename std::vector>::const_iterator const_iterator; + typedef uint_fast64_t IndexType; + typedef typename std::vector>::iterator iterator; + typedef typename std::vector>::const_iterator const_iterator; /*! * This class represents a number of consecutive rows of the matrix. @@ -270,7 +273,7 @@ namespace storm { * @param begin An iterator that points to the beginning of the row. * @param entryCount The number of entrys in the rows. */ - rows(iterator begin, uint_fast64_t entryCount); + rows(iterator begin, IndexType entryCount); /*! * Retrieves an iterator that points to the beginning of the rows. @@ -286,12 +289,19 @@ namespace storm { */ iterator end(); + /*! + * Retrieves the number of entries in the rows. + * + * @return The number of entries in the rows. + */ + IndexType getNumberOfEntries() const; + private: // The pointer to the columnd and value of the first entry. iterator beginIterator; // The number of non-zero entries in the rows. - uint_fast64_t entryCount; + IndexType entryCount; }; /*! @@ -306,7 +316,7 @@ namespace storm { * @param begin An iterator that points to the beginning of the row. * @param entryCount The number of entrys in the rows. */ - const_rows(const_iterator begin, uint_fast64_t entryCount); + const_rows(const_iterator begin, IndexType entryCount); /*! * Retrieves an iterator that points to the beginning of the rows. @@ -322,12 +332,19 @@ namespace storm { */ const_iterator end() const; + /*! + * Retrieves the number of entries in the rows. + * + * @return The number of entries in the rows. + */ + IndexType getNumberOfEntries() const; + private: // The pointer to the columnd and value of the first entry. const_iterator beginIterator; // The number of non-zero entries in the rows. - uint_fast64_t entryCount; + IndexType entryCount; }; /*! @@ -347,14 +364,14 @@ namespace storm { * * @param other The matrix from which to copy the content. */ - SparseMatrix(SparseMatrix const& other); + SparseMatrix(SparseMatrix const& other); /*! * Constructs a sparse matrix by moving the contents of the given matrix to the newly created one. * * @param other The matrix from which to move the content. */ - SparseMatrix(SparseMatrix&& other); + SparseMatrix(SparseMatrix&& other); /*! * Constructs a sparse matrix by copying the given contents. @@ -364,7 +381,7 @@ namespace storm { * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. * @param rowGroupIndices The vector representing the row groups in the matrix. */ - SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices); + SparseMatrix(IndexType columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, std::vector const& rowGroupIndices); /*! * Constructs a sparse matrix by moving the given contents. @@ -374,21 +391,21 @@ namespace storm { * @param columnsAndValues The vector containing the columns and values of the entries in the matrix. * @param rowGroupIndices The vector representing the row groups in the matrix. */ - SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices); + SparseMatrix(IndexType columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, std::vector&& rowGroupIndices); /*! * Assigns the contents of the given matrix to the current one by deep-copying its contents. * * @param other The matrix from which to copy-assign. */ - SparseMatrix& operator=(SparseMatrix const& other); + SparseMatrix& operator=(SparseMatrix const& other); /*! * Assigns the contents of the given matrix to the current one by moving its contents. * * @param other The matrix from which to move to contents. */ - SparseMatrix& operator=(SparseMatrix&& other); + SparseMatrix& operator=(SparseMatrix&& other); /*! * Determines whether the current and the given matrix are semantically equal. @@ -396,42 +413,42 @@ namespace storm { * @param other The matrix with which to compare the current matrix. * @return True iff the given matrix is semantically equal to the current one. */ - bool operator==(SparseMatrix const& other) const; + bool operator==(SparseMatrix const& other) const; /*! * Returns the number of rows of the matrix. * * @return The number of rows of the matrix. */ - uint_fast64_t getRowCount() const; + IndexType getRowCount() const; /*! * Returns the number of columns of the matrix. * * @return The number of columns of the matrix. */ - uint_fast64_t getColumnCount() const; + IndexType getColumnCount() const; /*! * Returns the number of entries in the matrix. * * @return The number of entries in the matrix. */ - uint_fast64_t getEntryCount() const; + IndexType getEntryCount() const; /*! * Returns the number of nonzero entries in the matrix. * * @return The number of nonzero entries in the matrix. */ - uint_fast64_t getNonzeroEntryCount() const; + IndexType getNonzeroEntryCount() const; /*! * Returns the number of row groups in the matrix. * * @return The number of row groups in the matrix. */ - uint_fast64_t getRowGroupCount() const; + IndexType getRowGroupCount() const; /*! * Returns the size of the given row group. @@ -439,14 +456,14 @@ namespace storm { * @param group The group whose size to retrieve. * @return The number of rows that belong to the given row group. */ - uint_fast64_t getRowGroupSize(uint_fast64_t group) const; + IndexType getRowGroupSize(IndexType group) const; /*! * Returns the grouping of rows of this matrix. * * @return The grouping of rows of this matrix. */ - std::vector const& getRowGroupIndices() const; + std::vector const& getRowGroupIndices() const; /*! * This function makes the given rows absorbing. @@ -469,7 +486,7 @@ namespace storm { * @param row The row to be made Dirac. * @param column The index of the column whose value is to be set to 1. */ - void makeRowDirac(const uint_fast64_t row, const uint_fast64_t column); + void makeRowDirac(const IndexType row, const IndexType column); /* * Sums the entries in the given row and columns. @@ -478,7 +495,7 @@ namespace storm { * @param columns A bit vector that indicates which columns to add. * @return The sum of the entries in the given row and columns. */ - T getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& columns) const; + ValueType getConstrainedRowSum(IndexType row, storm::storage::BitVector const& columns) const; /*! * Computes a vector whose i-th entry is the sum of the entries in the i-th selected row where only those @@ -489,7 +506,7 @@ namespace storm { * * @return A vector whose elements are the sums of the selected columns in each row. */ - std::vector getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const; + std::vector getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const; /*! * Computes a vector whose entries represent the sums of selected columns for all rows in selected row @@ -500,7 +517,7 @@ namespace storm { * @return A vector whose entries represent the sums of selected columns for all rows in selected row * groups. */ - std::vector getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const; + std::vector getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const; /*! * Creates a submatrix of the current matrix by dropping all rows and columns whose bits are not @@ -524,7 +541,7 @@ namespace storm { * each row in row group i. This can then be used for inserting other values later. * @return A submatrix of the current matrix by selecting one row out of each row group. */ - SparseMatrix selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; + SparseMatrix selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries = true) const; /*! * Transposes the matrix. @@ -533,7 +550,7 @@ namespace storm { * * @return A sparse matrix that represents the transpose of this matrix. */ - storm::storage::SparseMatrix transpose(bool joinGroups = false) const; + storm::storage::SparseMatrix transpose(bool joinGroups = false) const; /*! * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A). @@ -561,7 +578,7 @@ namespace storm { * * @return A pair (L+U, D^-1) containing the matrix L+U and the inverted diagonal matrix D^-1. */ - std::pair, storm::storage::SparseMatrix> getJacobiDecomposition() const; + std::pair, storm::storage::SparseMatrix> getJacobiDecomposition() const; /*! * Performs a pointwise matrix multiplication of the matrix with the given matrix and returns a vector @@ -573,7 +590,7 @@ namespace storm { * @return A vector containing the sum of the entries in each row of the matrix resulting from pointwise * multiplication of the current matrix with the given matrix. */ - std::vector getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; + std::vector getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; /*! * Multiplies the matrix with the given vector and writes the result to the given result vector. If a @@ -584,7 +601,7 @@ namespace storm { * @param result The vector that is supposed to hold the result of the multiplication after the operation. * @return The product of the matrix and the given vector as the content of the given result vector. */ - void multiplyWithVector(std::vector const& vector, std::vector& result) const; + void multiplyWithVector(std::vector const& vector, std::vector& result) const; /*! * Multiplies the matrix with the given vector in a sequential way and writes the result to the given result @@ -594,7 +611,7 @@ namespace storm { * @param result The vector that is supposed to hold the result of the multiplication after the operation. * @return The product of the matrix and the given vector as the content of the given result vector. */ - void multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const; + void multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const; #ifdef STORM_HAVE_INTELTBB /*! @@ -605,7 +622,7 @@ namespace storm { * @param result The vector that is supposed to hold the result of the multiplication after the operation. * @return The product of the matrix and the given vector as the content of the given result vector. */ - void multiplyWithVectorParallel(std::vector const& vector, std::vector& result) const; + void multiplyWithVectorParallel(std::vector const& vector, std::vector& result) const; #endif /*! @@ -614,7 +631,7 @@ namespace storm { * @param row The row that is to be summed. * @return The sum of the selected row. */ - T getRowSum(uint_fast64_t row) const; + ValueType getRowSum(IndexType row) const; /*! * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix @@ -623,7 +640,7 @@ namespace storm { * @param matrix The matrix that possibly is a supermatrix of the current matrix. * @return True iff the current matrix is a submatrix of the given matrix. */ - bool isSubmatrixOf(SparseMatrix const& matrix) const; + bool isSubmatrixOf(SparseMatrix const& matrix) const; template friend std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); @@ -649,7 +666,7 @@ namespace storm { * @param endRow The ending row (which is included in the result). * @return An object representing the consecutive rows given by the parameters. */ - const_rows getRows(uint_fast64_t startRow, uint_fast64_t endRow) const; + const_rows getRows(IndexType startRow, IndexType endRow) const; /*! * Returns an object representing the consecutive rows given by the parameters. @@ -658,7 +675,7 @@ namespace storm { * @param endRow The ending row (which is included in the result). * @return An object representing the consecutive rows given by the parameters. */ - rows getRows(uint_fast64_t startRow, uint_fast64_t endRow); + rows getRows(IndexType startRow, IndexType endRow); /*! * Returns an object representing the given row. @@ -666,7 +683,7 @@ namespace storm { * @param row The row to get. * @return An object representing the given row. */ - const_rows getRow(uint_fast64_t row) const; + const_rows getRow(IndexType row) const; /*! * Returns an object representing the given row. @@ -674,7 +691,7 @@ namespace storm { * @param row The row to get. * @return An object representing the given row. */ - rows getRow(uint_fast64_t row); + rows getRow(IndexType row); /*! * Returns an object representing the given row group. @@ -682,7 +699,7 @@ namespace storm { * @param rowGroup The row group to get. * @return An object representing the given row group. */ - const_rows getRowGroup(uint_fast64_t rowGroup) const; + const_rows getRowGroup(IndexType rowGroup) const; /*! * Returns an object representing the given row group. @@ -690,7 +707,7 @@ namespace storm { * @param rowGroup The row group to get. * @return An object representing the given row group. */ - rows getRowGroup(uint_fast64_t rowGroup); + rows getRowGroup(IndexType rowGroup); /*! * Retrieves an iterator that points to the beginning of the given row. @@ -698,7 +715,7 @@ namespace storm { * @param row The row to the beginning of which the iterator has to point. * @return An iterator that points to the beginning of the given row. */ - const_iterator begin(uint_fast64_t row = 0) const; + const_iterator begin(IndexType row = 0) const; /*! * Retrieves an iterator that points to the beginning of the given row. @@ -706,7 +723,7 @@ namespace storm { * @param row The row to the beginning of which the iterator has to point. * @return An iterator that points to the beginning of the given row. */ - iterator begin(uint_fast64_t row = 0); + iterator begin(IndexType row = 0); /*! * Retrieves an iterator that points past the end of the given row. @@ -714,7 +731,7 @@ namespace storm { * @param row The row past the end of which the iterator has to point. * @return An iterator that points past the end of the given row. */ - const_iterator end(uint_fast64_t row) const; + const_iterator end(IndexType row) const; /*! * Retrieves an iterator that points past the end of the given row. @@ -722,7 +739,7 @@ namespace storm { * @param row The row past the end of which the iterator has to point. * @return An iterator that points past the end of the given row. */ - iterator end(uint_fast64_t row); + iterator end(IndexType row); /*! * Retrieves an iterator that points past the end of the last row of the matrix. @@ -751,31 +768,31 @@ namespace storm { * @return A matrix corresponding to a submatrix of the current matrix in which only row groups and columns * given by the row group constraint are kept and all others are dropped. */ - SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries = false) const; + SparseMatrix getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries = false) const; // The number of rows of the matrix. - uint_fast64_t rowCount; + IndexType rowCount; // The number of columns of the matrix. - uint_fast64_t columnCount; + IndexType columnCount; // The number of entries in the matrix. - uint_fast64_t entryCount; + IndexType entryCount; // The number of nonzero entries in the matrix. - uint_fast64_t nonzeroEntryCount; + IndexType nonzeroEntryCount; // The storage for the columns and values of all entries in the matrix. - std::vector> columnsAndValues; + std::vector> columnsAndValues; // A vector containing the indices at which each given row begins. This index is to be interpreted as an // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. - std::vector rowIndications; + std::vector rowIndications; // A vector indicating the row groups of the matrix. - std::vector rowGroupIndices; + std::vector rowGroupIndices; }; } // namespace storage diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 57cda7018..724b20018 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -496,7 +496,7 @@ namespace storm { // Prepare the vectors that represent the matrix. std::vector rowIndications(rowOdd.getTotalOffset() + 1); - std::vector> columnsAndValues(this->getNonZeroCount()); + std::vector> columnsAndValues(this->getNonZeroCount()); // Create a trivial row grouping. std::vector trivialRowGroupIndices(rowIndications.size()); @@ -584,7 +584,7 @@ namespace storm { splitGroupsRec(this->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables); // Create the actual storage for the non-zero entries. - std::vector> columnsAndValues(this->getNonZeroCount()); + std::vector> columnsAndValues(this->getNonZeroCount()); // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); @@ -638,7 +638,7 @@ namespace storm { return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } - void Dd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { + void Dd::toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues) const { // For the empty DD, we do not need to add any entries. if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) { return; @@ -647,7 +647,7 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentRowLevel + currentColumnLevel == maxLevel) { if (generateValues) { - columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); + columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] = storm::storage::MatrixEntry(currentColumnOffset, Cudd_V(dd)); } ++rowIndications[rowGroupOffsets[currentRowOffset]]; } else { diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 316e30c89..adcb2e490 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -685,7 +685,7 @@ namespace storm { * only works if the offsets given in rowIndications are already correct. If they need to be computed first, * this flag needs to be false. */ - void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; + void toMatrixRec(DdNode const* dd, std::vector& rowIndications, std::vector>& columnsAndValues, std::vector const& rowGroupOffsets, Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector const& ddRowVariableIndices, std::vector const& ddColumnVariableIndices, bool generateValues = true) const; /*! * Splits the given matrix DD into the groups using the given group variables. diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index de89f4950..52746ef97 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -147,7 +147,7 @@ TEST(SparseMatrix, Build) { } TEST(SparseMatrix, CreationWithMovingContents) { - std::vector> columnsAndValues; + std::vector> columnsAndValues; columnsAndValues.emplace_back(1, 1.0); columnsAndValues.emplace_back(2, 1.2); columnsAndValues.emplace_back(0, 0.5);