#include // To detect whether the usage of TBB is possible, this include is neccessary #include "storm-config.h" #ifdef STORM_HAVE_INTELTBB #include "tbb/tbb.h" #endif #include "storm/storage/sparse/StateType.h" #include "storm/storage/SparseMatrix.h" #include "storm/adapters/CarlAdapter.h" #include "storm/storage/BitVector.h" #include "storm/utility/constants.h" #include "storm/utility/ConstantsComparator.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/utility/macros.h" #include namespace storm { namespace storage { template MatrixEntry::MatrixEntry(IndexType column, ValueType value) : entry(column, value) { // Intentionally left empty. } template MatrixEntry::MatrixEntry(std::pair&& pair) : entry(std::move(pair)) { // Intentionally left empty. } template IndexType const& MatrixEntry::getColumn() const { return this->entry.first; } template void MatrixEntry::setColumn(IndexType const& column) { this->entry.first = column; } template ValueType const& MatrixEntry::getValue() const { return this->entry.second; } template void MatrixEntry::setValue(ValueType const& value) { this->entry.second = value; } template std::pair const& MatrixEntry::getColumnValuePair() const { return this->entry; } template MatrixEntry MatrixEntry::operator*(value_type factor) const { return MatrixEntry(this->getColumn(), this->getValue() * factor); } template bool MatrixEntry::operator==(MatrixEntry const& other) const { return this->entry.first == other.entry.first && this->entry.second == other.entry.second; } template bool MatrixEntry::operator!=(MatrixEntry const& other) const { return !(*this == other); } template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry) { out << "(" << entry.getColumn() << ", " << entry.getValue() << ")"; return out; } template SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) { // Prepare the internal storage. if (initialRowCountSet) { rowIndications.reserve(initialRowCount + 1); } if (initialEntryCountSet) { columnsAndValues.reserve(initialEntryCount); } if (hasCustomRowGrouping) { rowGroupIndices = std::vector(); } if (initialRowGroupCountSet && hasCustomRowGrouping) { rowGroupIndices.get().reserve(initialRowGroupCount + 1); } rowIndications.push_back(0); } template SparseMatrixBuilder::SparseMatrixBuilder(SparseMatrix&& matrix) : initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), lastRow(matrix.rowCount - 1), lastColumn(columnsAndValues.back().getColumn()), highestColumn(matrix.getColumnCount() - 1), currentRowGroup() { // If the matrix has a custom row grouping, we move it and remove the last element to make it 'open' again. if (hasCustomRowGrouping) { rowGroupIndices = std::move(matrix.rowGroupIndices); rowGroupIndices.get().pop_back(); currentRowGroup = rowGroupIndices.get().size() - 1; } // Likewise, we need to 'open' the row indications again. rowIndications.pop_back(); } template void SparseMatrixBuilder::addNextValue(index_type row, index_type column, ValueType const& value) { // Check that we did not move backwards wrt. the row. STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException, "Adding an element in row " << row << ", but an element in row " << lastRow << " has already been added."); // If the element is in the same row, but was not inserted in the correct order, we need to fix the row after // the insertion. bool fixCurrentRow = row == lastRow && column < lastColumn; // If we switched to another row, we have to adjust the missing entries in the row indices vector. if (row != lastRow) { // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations. for (index_type i = lastRow + 1; i <= row; ++i) { rowIndications.push_back(currentEntryCount); } lastRow = row; } lastColumn = column; // Finally, set the element and increase the current size. columnsAndValues.emplace_back(column, value); highestColumn = std::max(highestColumn, column); ++currentEntryCount; // If we need to fix the row, do so now. if (fixCurrentRow) { // First, we sort according to columns. std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry const& a, storm::storage::MatrixEntry const& b) { return a.getColumn() < b.getColumn(); }); // Then, we eliminate possible duplicate entries. auto it = std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry const& a, storm::storage::MatrixEntry const& b) { return a.getColumn() == b.getColumn(); }); // Finally, remove the superfluous elements. std::size_t elementsToRemove = std::distance(it, columnsAndValues.end()); if (elementsToRemove > 0) { STORM_LOG_WARN("Unordered insertion into matrix builder caused duplicate entries."); currentEntryCount -= elementsToRemove; columnsAndValues.resize(columnsAndValues.size() - elementsToRemove); } } // In case we did not expect this value, we throw an exception. if (forceInitialDimensions) { STORM_LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << "."); STORM_LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal column " << lastColumn << "."); STORM_LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << "."); } } template void SparseMatrixBuilder::newRowGroup(index_type startingRow) { STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping."); STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size."); rowGroupIndices.get().push_back(startingRow); ++currentRowGroup; // Close all rows from the most recent one to the starting row. for (index_type i = lastRow + 1; i <= startingRow; ++i) { rowIndications.push_back(currentEntryCount); } // Reset the most recently seen row/column to allow for proper insertion of the following elements. lastRow = startingRow; lastColumn = 0; } template SparseMatrix SparseMatrixBuilder::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) { uint_fast64_t rowCount = lastRow + 1; if (initialRowCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << "."); rowCount = std::max(rowCount, initialRowCount); } rowCount = std::max(rowCount, overriddenRowCount); // If the current row count was overridden, we may need to add empty rows. for (index_type i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); } // We put a sentinel element at the last position of the row indices array. This eases iteration work, // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for // the first and last row. rowIndications.push_back(currentEntryCount); uint_fast64_t columnCount = highestColumn + 1; if (initialColumnCountSet && forceInitialDimensions) { STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << "."); columnCount = std::max(columnCount, initialColumnCount); } columnCount = std::max(columnCount, overriddenColumnCount); uint_fast64_t entryCount = currentEntryCount; if (initialEntryCountSet && forceInitialDimensions) { STORM_LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << "."); } // Check whether row groups are missing some entries. if (hasCustomRowGrouping) { uint_fast64_t rowGroupCount = currentRowGroup; if (initialRowGroupCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << "."); rowGroupCount = std::max(rowGroupCount, initialRowGroupCount); } rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount); for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) { rowGroupIndices.get().push_back(rowCount); } } return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } template typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastRow() const { return lastRow; } template typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastColumn() const { return lastColumn; } // Debug method for printing the current matrix template void print(std::vector::index_type> const& rowGroupIndices, std::vector::index_type, typename SparseMatrix::value_type>> const& columnsAndValues, std::vector::index_type> const& rowIndications) { typename SparseMatrix::index_type endGroups; typename SparseMatrix::index_type endRows; // Iterate over all row groups. for (typename SparseMatrix::index_type group = 0; group < rowGroupIndices.size(); ++group) { std::cout << "\t---- group " << group << "/" << (rowGroupIndices.size() - 1) << " ---- " << std::endl; endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size(); // Iterate over all rows in a row group for (typename SparseMatrix::index_type i = rowGroupIndices[group]; i < endGroups; ++i) { endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); // Print the actual row. std::cout << "Row " << i << " (" << rowIndications[i] << " - " << endRows << ")" << ": "; for (typename SparseMatrix::index_type pos = rowIndications[i]; pos < endRows; ++pos) { std::cout << "(" << columnsAndValues[pos].getColumn() << ": " << columnsAndValues[pos].getValue() << ") "; } std::cout << std::endl; } } } template void SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { index_type maxColumn = 0; for (index_type row = 0; row < rowIndications.size(); ++row) { bool changed = false; auto startRow = std::next(columnsAndValues.begin(), rowIndications[row]); auto endRow = row < rowIndications.size()-1 ? std::next(columnsAndValues.begin(), rowIndications[row+1]) : columnsAndValues.end(); for (auto entry = startRow; entry != endRow; ++entry) { if (entry->getColumn() >= offset) { // Change column entry->setColumn(replacements[entry->getColumn() - offset]); changed = true; } maxColumn = std::max(maxColumn, entry->getColumn()); } if (changed) { // Sort columns in row std::sort(startRow, endRow, [](MatrixEntry const& a, MatrixEntry const& b) { return a.getColumn() < b.getColumn(); }); // Assert no equal elements STORM_LOG_ASSERT(std::is_sorted(startRow, endRow, [](MatrixEntry const& a, MatrixEntry const& b) { return a.getColumn() < b.getColumn(); }), "Columns not sorted."); } } highestColumn = maxColumn; lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn(); } template SparseMatrix::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } template typename SparseMatrix::iterator SparseMatrix::rows::begin() { return beginIterator; } template typename SparseMatrix::iterator SparseMatrix::rows::end() { return beginIterator + entryCount; } template typename SparseMatrix::index_type SparseMatrix::rows::getNumberOfEntries() const { return this->entryCount; } template SparseMatrix::const_rows::const_rows(const_iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. } template typename SparseMatrix::const_iterator SparseMatrix::const_rows::begin() const { return beginIterator; } template typename SparseMatrix::const_iterator SparseMatrix::const_rows::end() const { return beginIterator + entryCount; } template typename SparseMatrix::index_type 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), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(other.rowGroupIndices) { // Intentionally left empty. } template SparseMatrix::SparseMatrix(SparseMatrix const& other, bool insertDiagonalElements) { storm::storage::BitVector rowConstraint(other.getRowCount(), true); storm::storage::BitVector columnConstraint(other.getColumnCount(), true); *this = other.getSubmatrix(false, rowConstraint, columnConstraint, insertDiagonalElements); } 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)), trivialRowGrouping(other.trivialRowGrouping), rowGroupIndices(std::move(other.rowGroupIndices)) { // Now update the source matrix other.rowCount = 0; other.columnCount = 0; other.entryCount = 0; } template SparseMatrix::SparseMatrix(index_type columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues, boost::optional> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(rowGroupIndices) { this->updateNonzeroEntryCount(); } template SparseMatrix::SparseMatrix(index_type columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues, boost::optional>&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), trivialRowGrouping(!rowGroupIndices), rowGroupIndices(std::move(rowGroupIndices)) { this->updateNonzeroEntryCount(); } template SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { // Only perform assignment if source and target are not the same. if (this != &other) { rowCount = other.rowCount; columnCount = other.columnCount; entryCount = other.entryCount; nonzeroEntryCount = other.nonzeroEntryCount; columnsAndValues = other.columnsAndValues; rowIndications = other.rowIndications; rowGroupIndices = other.rowGroupIndices; trivialRowGrouping = other.trivialRowGrouping; } return *this; } template SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { // Only perform assignment if source and target are not the same. if (this != &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); trivialRowGrouping = other.trivialRowGrouping; } return *this; } template bool SparseMatrix::operator==(SparseMatrix const& other) const { if (this == &other) { return true; } bool equalityResult = true; equalityResult &= this->getRowCount() == other.getRowCount(); if (!equalityResult) { return false; } equalityResult &= this->getColumnCount() == other.getColumnCount(); if (!equalityResult) { return false; } if (!this->hasTrivialRowGrouping() && !other.hasTrivialRowGrouping()) { equalityResult &= this->getRowGroupIndices() == other.getRowGroupIndices(); } else { equalityResult &= this->hasTrivialRowGrouping() && other.hasTrivialRowGrouping(); } if (!equalityResult) { return false; } // 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 (index_type 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 && storm::utility::isZero(it1->getValue())) { ++it1; } while (it2 != ite2 && storm::utility::isZero(it2->getValue())) { ++it2; } if ((it1 == ite1) || (it2 == ite2)) { equalityResult = (it1 == ite1) ^ (it2 == ite2); break; } else { if (it1->getColumn() != it2->getColumn() || it1->getValue() != it2->getValue()) { equalityResult = false; break; } } } if (!equalityResult) { return false; } } return equalityResult; } template typename SparseMatrix::index_type SparseMatrix::getRowCount() const { return rowCount; } template typename SparseMatrix::index_type SparseMatrix::getColumnCount() const { return columnCount; } template typename SparseMatrix::index_type SparseMatrix::getEntryCount() const { return entryCount; } template uint_fast64_t SparseMatrix::getRowGroupEntryCount(uint_fast64_t const group) const { uint_fast64_t result = 0; if (!this->hasTrivialRowGrouping()) { for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group + 1]; ++row) { result += (this->rowIndications[row + 1] - this->rowIndications[row]); } } else { result += (this->rowIndications[group + 1] - this->rowIndications[group]); } return result; } template typename SparseMatrix::index_type SparseMatrix::getNonzeroEntryCount() const { return nonzeroEntryCount; } template void SparseMatrix::updateNonzeroEntryCount() const { this->nonzeroEntryCount = 0; for (auto const& element : *this) { if (element.getValue() != storm::utility::zero()) { ++this->nonzeroEntryCount; } } } template void SparseMatrix::updateNonzeroEntryCount(std::make_signed::type difference) { this->nonzeroEntryCount += difference; } template void SparseMatrix::updateDimensions() const { this->nonzeroEntryCount = 0; this->columnCount = 0; for (auto const& element : *this) { if (element.getValue() != storm::utility::zero()) { ++this->nonzeroEntryCount; this->columnCount = std::max(element.getColumn() + 1, this->columnCount); } } } template typename SparseMatrix::index_type SparseMatrix::getRowGroupCount() const { if (!this->hasTrivialRowGrouping()) { return rowGroupIndices.get().size() - 1; } else { return rowCount; } } template typename SparseMatrix::index_type SparseMatrix::getRowGroupSize(index_type group) const { return this->getRowGroupIndices()[group + 1] - this->getRowGroupIndices()[group]; } template std::vector::index_type> const& SparseMatrix::getRowGroupIndices() const { // If there is no current row grouping, we need to create it. if (!this->rowGroupIndices) { STORM_LOG_ASSERT(trivialRowGrouping, "Only trivial row-groupings can be constructed on-the-fly."); this->rowGroupIndices = std::vector(this->getRowCount() + 1); for (uint_fast64_t group = 0; group <= this->getRowCount(); ++group) { this->rowGroupIndices.get()[group] = group; } } return rowGroupIndices.get(); } template storm::storage::BitVector SparseMatrix::getRowIndicesOfRowGroups(storm::storage::BitVector const& groups) const { storm::storage::BitVector res(this->getRowCount(), false); for(auto group : groups) { for(uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group+1]; ++row) { res.set(row, true); } } return res; } 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) { if (!this->hasTrivialRowGrouping()) { for (auto rowGroup : rowGroupConstraint) { for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) { makeRowDirac(row, rowGroup); } } } else { for (auto rowGroup : rowGroupConstraint) { makeRowDirac(rowGroup, rowGroup); } } } template void SparseMatrix::makeRowDirac(index_type row, index_type column) { iterator columnValuePtr = this->begin(row); iterator columnValuePtrEnd = this->end(row); // If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements // in the vector of nonzeros otherwise. if (columnValuePtr >= columnValuePtrEnd) { throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, but there is no entry in this row."; } // 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->setColumn(column); columnValuePtr->setValue(storm::utility::one()); ++columnValuePtr; for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { ++this->nonzeroEntryCount; columnValuePtr->setColumn(0); columnValuePtr->setValue(storm::utility::zero()); } } template bool SparseMatrix::compareRows(index_type i1, index_type i2) const { const_iterator end1 = this->end(i1); const_iterator end2 = this->end(i2); const_iterator it1 = this->begin(i1); const_iterator it2 = this->begin(i2); for(;it1 != end1 && it2 != end2; ++it1, ++it2 ) { if(*it1 != *it2) { return false; } } if(it1 == end1 && it2 == end2) { return true; } return false; } template BitVector SparseMatrix::duplicateRowsInRowgroups() const { BitVector bv(this->getRowCount()); for(size_t rowgroup = 0; rowgroup < this->getRowGroupCount(); ++rowgroup) { for(size_t row1 = this->getRowGroupIndices().at(rowgroup); row1 < this->getRowGroupIndices().at(rowgroup+1); ++row1) { for(size_t row2 = row1; row2 < this->getRowGroupIndices().at(rowgroup+1); ++row2) { if(compareRows(row1, row2)) { bv.set(row2); } } } } return bv; } template void SparseMatrix::swapRows(index_type const& row1, index_type const& row2) { if (row1 == row2) { return; } // Get the index of the row that has more / less entries than the other. index_type largerRow = getRow(row1).getNumberOfEntries() > getRow(row2).getNumberOfEntries() ? row1 : row2; index_type smallerRow = largerRow == row1 ? row2 : row1; index_type rowSizeDifference = getRow(largerRow).getNumberOfEntries() - getRow(smallerRow).getNumberOfEntries(); // Save contents of larger row. auto copyRow = getRow(largerRow); std::vector> largerRowContents(copyRow.begin(), copyRow.end()); if (largerRow < smallerRow) { auto writeIt = getRows(largerRow, smallerRow + 1).begin(); // Write smaller row to its new position. for (auto& smallerRowEntry : getRow(smallerRow)) { *writeIt = std::move(smallerRowEntry); ++writeIt; } // Write the intermediate rows into their correct position. if (!storm::utility::isZero(rowSizeDifference)) { for (auto& intermediateRowEntry : getRows(largerRow + 1, smallerRow)) { *writeIt = std::move(intermediateRowEntry); ++writeIt; } } else { // skip the intermediate rows writeIt = getRow(smallerRow).begin(); } // Write the larger row to its new position. for (auto& largerRowEntry : largerRowContents) { *writeIt = std::move(largerRowEntry); ++writeIt; } STORM_LOG_ASSERT(writeIt == getRow(smallerRow).end(), "Unexpected position of write iterator."); // Update the row indications to account for the shift of indices at where the rows now start. if (!storm::utility::isZero(rowSizeDifference)) { for (index_type row = largerRow + 1; row <= smallerRow; ++row) { rowIndications[row] -= rowSizeDifference; } } } else { auto writeIt = getRows(smallerRow, largerRow + 1).end() - 1; // Write smaller row to its new position auto copyRow = getRow(smallerRow); for (auto smallerRowEntryIt = copyRow.end() - 1; smallerRowEntryIt != copyRow.begin() - 1; --smallerRowEntryIt) { *writeIt = std::move(*smallerRowEntryIt); --writeIt; } // Write the intermediate rows into their correct position. if (!storm::utility::isZero(rowSizeDifference)) { for (auto intermediateRowEntryIt = getRows(smallerRow + 1, largerRow).end() - 1; intermediateRowEntryIt != getRows(smallerRow + 1, largerRow).begin() - 1; --intermediateRowEntryIt) { *writeIt = std::move(*intermediateRowEntryIt); --writeIt; } } else { // skip the intermediate rows writeIt = getRow(smallerRow).end() - 1; } // Write the larger row to its new position. for (auto largerRowEntryIt = largerRowContents.rbegin(); largerRowEntryIt != largerRowContents.rend(); ++largerRowEntryIt) { *writeIt = std::move(*largerRowEntryIt); --writeIt; } STORM_LOG_ASSERT(writeIt == getRow(smallerRow).begin() - 1, "Unexpected position of write iterator."); // Update row indications. // Update the row indications to account for the shift of indices at where the rows now start. if (!storm::utility::isZero(rowSizeDifference)) { for (index_type row = smallerRow + 1; row <= largerRow; ++row) { rowIndications[row] += rowSizeDifference; } } } } template ValueType SparseMatrix::getConstrainedRowSum(index_type row, storm::storage::BitVector const& constraint) const { ValueType result = storm::utility::zero(); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { if (constraint.get(it->getColumn())) { result += it->getValue(); } } return result; } template std::vector SparseMatrix::getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const { std::vector result(rowConstraint.getNumberOfSetBits()); index_type 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; result.reserve(rowGroupConstraint.getNumberOfSetBits()); if (!this->hasTrivialRowGrouping()) { for (auto rowGroup : rowGroupConstraint) { for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) { result.push_back(getConstrainedRowSum(row, columnConstraint)); } } } else { for (auto rowGroup : rowGroupConstraint) { result.push_back(getConstrainedRowSum(rowGroup, columnConstraint)); } } return result; } 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); index_type i = 0; for (std::vector::iterator it = fakeRowGroupIndices.begin(); it != fakeRowGroupIndices.end(); ++it, ++i) { *it = i; } auto res = getSubmatrix(rowConstraint, columnConstraint, fakeRowGroupIndices, insertDiagonalElements); // Create a new row grouping that reflects the new sizes of the row groups if the current matrix has a // non trivial row-grouping. if (!this->hasTrivialRowGrouping()) { std::vector newRowGroupIndices; newRowGroupIndices.push_back(0); auto selectedRowIt = rowConstraint.begin(); // For this, we need to count how many rows were preserved in every group. for (uint_fast64_t group = 0; group < this->getRowGroupCount(); ++group) { uint_fast64_t newRowCount = 0; while (*selectedRowIt < this->getRowGroupIndices()[group + 1]) { ++selectedRowIt; ++newRowCount; } if (newRowCount > 0) { newRowGroupIndices.push_back(newRowGroupIndices.back() + newRowCount); } } res.trivialRowGrouping = false; res.rowGroupIndices = newRowGroupIndices; } return res; } } template SparseMatrix SparseMatrix::getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries) const { uint_fast64_t submatrixColumnCount = columnConstraint.getNumberOfSetBits(); // Start by creating 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 columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices(); std::vector* rowBitsSetBeforeIndex; if (&rowGroupConstraint == &columnConstraint) { rowBitsSetBeforeIndex = &columnBitsSetBeforeIndex; } else { rowBitsSetBeforeIndex = new std::vector(rowGroupConstraint.getNumberOfSetBitsBeforeIndices()); } // Then, we need to determine the number of entries and the number of rows of the submatrix. index_type subEntries = 0; index_type subRows = 0; index_type rowGroupCount = 0; for (auto index : rowGroupConstraint) { subRows += rowGroupIndices[index + 1] - rowGroupIndices[index]; for (index_type 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) { if (columnConstraint.get(it->getColumn())) { ++subEntries; if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) { foundDiagonalElement = true; } } } // If requested, we need to reserve one entry more for inserting the diagonal zero entry. if (insertDiagonalEntries && !foundDiagonalElement && rowGroupCount < submatrixColumnCount) { ++subEntries; } } ++rowGroupCount; } // Create and initialize resulting matrix. SparseMatrixBuilder matrixBuilder(subRows, submatrixColumnCount, subEntries, true, !this->hasTrivialRowGrouping()); // Copy over selected entries. rowGroupCount = 0; index_type rowCount = 0; for (auto index : rowGroupConstraint) { if (!this->hasTrivialRowGrouping()) { matrixBuilder.newRowGroup(rowCount); } for (index_type 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) { if (columnConstraint.get(it->getColumn())) { if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > (*rowBitsSetBeforeIndex)[index]) { matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero()); insertedDiagonalElement = true; } matrixBuilder.addNextValue(rowCount, columnBitsSetBeforeIndex[it->getColumn()], it->getValue()); } } if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) { matrixBuilder.addNextValue(rowGroupCount, rowGroupCount, storm::utility::zero()); } ++rowCount; } ++rowGroupCount; } // If the constraints were not the same, we have allocated some additional memory we need to free now. if (&rowGroupConstraint != &columnConstraint) { delete rowBitsSetBeforeIndex; } return matrixBuilder.build(); } template SparseMatrix SparseMatrix::restrictRows(storm::storage::BitVector const& rowsToKeep) const { // For now, we use the expensive call to submatrix. STORM_LOG_ASSERT(rowsToKeep.size() == this->getRowCount(), "Dimensions mismatch."); STORM_LOG_ASSERT(rowsToKeep.getNumberOfSetBits() >= this->getRowGroupCount(), "Invalid dimensions."); SparseMatrix res(getSubmatrix(false, rowsToKeep, storm::storage::BitVector(getColumnCount(), true), false)); STORM_LOG_ASSERT(res.getRowCount() == rowsToKeep.getNumberOfSetBits(), "Invalid dimensions"); STORM_LOG_ASSERT(res.getColumnCount() == this->getColumnCount(), "Invalid dimensions"); STORM_LOG_ASSERT(this->getRowGroupCount() == res.getRowGroupCount(), "Invalid dimensions"); return res; } 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. index_type subEntries = 0; for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { // Determine which row we need to select from the current row group. index_type rowToCopy = this->getRowGroupIndices()[rowGroupIndex] + rowGroupToRowIndexMapping[rowGroupIndex]; // Iterate through that row and count the number of slots we have to reserve for copying. bool foundDiagonalElement = false; for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) { if (it->getColumn() == rowGroupIndex) { foundDiagonalElement = true; } ++subEntries; } if (insertDiagonalEntries && !foundDiagonalElement) { ++subEntries; } } // Now create the matrix to be returned with the appropriate size. SparseMatrixBuilder matrixBuilder(rowGroupIndices.get().size() - 1, columnCount, subEntries); // Copy over the selected lines from the source matrix. for (index_type rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { // Determine which row we need to select from the current row group. index_type rowToCopy = this->getRowGroupIndices()[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. bool insertedDiagonalElement = false; for (const_iterator it = this->begin(rowToCopy), ite = this->end(rowToCopy); it != ite; ++it) { if (it->getColumn() == rowGroupIndex) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > rowGroupIndex) { matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::zero()); insertedDiagonalElement = true; } matrixBuilder.addNextValue(rowGroupIndex, it->getColumn(), it->getValue()); } if (insertDiagonalEntries && !insertedDiagonalElement) { matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::zero()); } } // Finalize created matrix and return result. return matrixBuilder.build(); } template SparseMatrix SparseMatrix::selectRowsFromRowIndexSequence(std::vector const& rowIndexSequence, 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. index_type newEntries = 0; for(index_type row = 0, rowEnd = rowIndexSequence.size(); row < rowEnd; ++row) { bool foundDiagonalElement = false; for (const_iterator it = this->begin(rowIndexSequence[row]), ite = this->end(rowIndexSequence[row]); it != ite; ++it) { if (it->getColumn() == row) { foundDiagonalElement = true; } ++newEntries; } if (insertDiagonalEntries && !foundDiagonalElement) { ++newEntries; } } // Now create the matrix to be returned with the appropriate size. SparseMatrixBuilder matrixBuilder(rowIndexSequence.size(), columnCount, newEntries); // Copy over the selected rows from the source matrix. for(index_type row = 0, rowEnd = rowIndexSequence.size(); row < rowEnd; ++row) { bool insertedDiagonalElement = false; for (const_iterator it = this->begin(rowIndexSequence[row]), ite = this->end(rowIndexSequence[row]); it != ite; ++it) { if (it->getColumn() == row) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && it->getColumn() > row) { matrixBuilder.addNextValue(row, row, storm::utility::zero()); insertedDiagonalElement = true; } matrixBuilder.addNextValue(row, it->getColumn(), it->getValue()); } if (insertDiagonalEntries && !insertedDiagonalElement) { matrixBuilder.addNextValue(row, row, storm::utility::zero()); } } // Finally create matrix and return result. return matrixBuilder.build(); } template SparseMatrix SparseMatrix::transpose(bool joinGroups, bool keepZeros) const { index_type rowCount = this->getColumnCount(); index_type columnCount = joinGroups ? this->getRowGroupCount() : this->getRowCount(); index_type entryCount; if (keepZeros) { entryCount = this->getEntryCount(); } else { this->updateNonzeroEntryCount(); entryCount = this->getNonzeroEntryCount(); } std::vector rowIndications(rowCount + 1); std::vector> columnsAndValues(entryCount); // First, we need to count how many entries each column has. for (index_type group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { if (transition.getValue() != storm::utility::zero() || keepZeros) { ++rowIndications[transition.getColumn() + 1]; } } } // Now compute the accumulated offsets. for (index_type 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; // Now we are ready to actually fill in the values of the transposed matrix. for (index_type group = 0; group < columnCount; ++group) { for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) { if (transition.getValue() != storm::utility::zero() || keepZeros) { columnsAndValues[nextIndices[transition.getColumn()]] = std::make_pair(group, transition.getValue()); nextIndices[transition.getColumn()]++; } } } storm::storage::SparseMatrix transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), boost::none); return transposedMatrix; } template void SparseMatrix::convertToEquationSystem() { invertDiagonal(); negateAllNonDiagonalEntries(); } 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. ValueType one = storm::utility::one(); ValueType zero = storm::utility::zero(); bool foundDiagonalElement = false; for (index_type group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() == group) { if (entry.getValue() == one) { --this->nonzeroEntryCount; entry.setValue(zero); } else if (entry.getValue() == zero) { ++this->nonzeroEntryCount; entry.setValue(one); } else { entry.setValue(one - entry.getValue()); } foundDiagonalElement = true; } } // Throw an exception if a row did not have an element on the diagonal. if (!foundDiagonalElement) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is missing diagonal entries."; } } } template void SparseMatrix::negateAllNonDiagonalEntries() { // Iterate over all row groups and negate all the elements that are not on the diagonal. for (index_type group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() != group) { entry.setValue(-entry.getValue()); } } } } template void SparseMatrix::deleteDiagonalEntries() { // Iterate over all rows and negate all the elements that are not on the diagonal. for (index_type group = 0; group < this->getRowGroupCount(); ++group) { for (auto& entry : this->getRowGroup(group)) { if (entry.getColumn() == group) { --this->nonzeroEntryCount; entry.setValue(storm::utility::zero()); } } } } template typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(this->getRowCount() == this->getColumnCount(), storm::exceptions::InvalidArgumentException, "Canno compute Jacobi decomposition of non-square matrix."); // Prepare the resulting data structures. SparseMatrixBuilder luBuilder(this->getRowCount(), this->getColumnCount()); std::vector invertedDiagonal(rowCount); // Copy entries to the appropriate matrices. for (index_type rowNumber = 0; rowNumber < rowCount; ++rowNumber) { for (const_iterator it = this->begin(rowNumber), ite = this->end(rowNumber); it != ite; ++it) { if (it->getColumn() == rowNumber) { invertedDiagonal[rowNumber] = storm::utility::one() / it->getValue(); } else { luBuilder.addNextValue(rowNumber, it->getColumn(), it->getValue()); } } } return std::make_pair(luBuilder.build(), std::move(invertedDiagonal)); } #ifdef STORM_HAVE_CARL template<> typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } template<> typename std::pair, std::vector> SparseMatrix::getJacobiDecomposition() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } #endif template template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { std::vector result(rowCount, storm::utility::zero()); // 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 (index_type row = 0; row < rowCount && row < otherMatrix.getRowCount(); ++row) { typename storm::storage::SparseMatrix::const_iterator it2 = otherMatrix.begin(row); typename storm::storage::SparseMatrix::const_iterator ite2 = otherMatrix.end(row); for (const_iterator it1 = this->begin(row), ite1 = this->end(row); it1 != ite1 && it2 != ite2; ++it1) { if (it1->getColumn() < it2->getColumn()) { continue; } else { // If the precondition of this method (i.e. that the given matrix is a submatrix // of the current one) was fulfilled, we know now that the two elements are in // the same column, so we can multiply and add them to the row sum vector. result[row] += it2->getValue() * OtherValueType(it1->getValue()); ++it2; } } } return result; } 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); } else { return this->multiplyWithVectorSequential(vector, result); } #else return multiplyWithVectorSequential(vector, result); #endif } template void SparseMatrix::multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const { if (&vector == &result) { STORM_LOG_WARN("Matrix-vector-multiplication invoked but the target vector uses the same memory as the input vector. This requires to allocate auxiliary memory."); std::vector tmpVector(this->getRowCount()); multiplyWithVectorSequential(vector, tmpVector); result = std::move(tmpVector); } else { const_iterator it = this->begin(); const_iterator ite; 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::zero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { *resultIterator += it->getValue() * vector[it->getColumn()]; } } } } #ifdef STORM_HAVE_INTELTBB template void SparseMatrix::multiplyWithVectorParallel(std::vector const& vector, std::vector& result) const { if (&vector == &result) { STORM_LOG_WARN("Matrix-vector-multiplication invoked but the target vector uses the same memory as the input vector. This requires to allocate auxiliary memory."); std::vector tmpVector(this->getRowCount()); multiplyWithVectorParallel(vector, tmpVector); result = std::move(tmpVector); } else { tbb::parallel_for(tbb::blocked_range(0, result.size(), 10), [&] (tbb::blocked_range const& range) { index_type startRow = range.begin(); index_type 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; for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::zero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { *resultIterator += it->getValue() * vector[it->getColumn()]; } } }); } } #endif template ValueType SparseMatrix::multiplyRowWithVector(index_type row, std::vector const& vector) const { ValueType result = storm::utility::zero(); for(auto const& entry : this->getRow(row)){ result += entry.getValue() * vector[entry.getColumn()]; } return result; } template void SparseMatrix::performSuccessiveOverRelaxationStep(ValueType omega, std::vector& x, std::vector const& b) const { const_iterator it = this->begin(); const_iterator ite; std::vector::const_iterator rowIterator = rowIndications.begin(); typename std::vector::const_iterator bIt = b.begin(); typename std::vector::iterator resultIterator = x.begin(); typename std::vector::iterator resultIteratorEnd = x.end(); // If the vector to multiply with and the target vector are actually the same, we need an auxiliary variable // to store the intermediate result. index_type currentRow = 0; for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator, ++bIt) { ValueType tmpValue = storm::utility::zero(); ValueType diagonalElement = storm::utility::zero(); for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { if (it->getColumn() != currentRow) { tmpValue += it->getValue() * x[it->getColumn()]; } else { diagonalElement += it->getValue(); } } *resultIterator = ((storm::utility::one() - omega) * *resultIterator) + (omega / diagonalElement) * (*bIt - tmpValue); ++currentRow; } } #ifdef STORM_HAVE_CARL template<> void SparseMatrix::performSuccessiveOverRelaxationStep(Interval, std::vector&, std::vector const&) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported."); } #endif template void SparseMatrix::multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const { const_iterator it = this->begin(); const_iterator ite; std::vector::const_iterator rowIterator = rowIndications.begin(); std::vector::const_iterator rowIteratorEnd = rowIndications.end(); uint_fast64_t currentRow = 0; for (; rowIterator != rowIteratorEnd - 1; ++rowIterator) { for (ite = this->begin() + *(rowIterator + 1); it != ite; ++it) { result[it->getColumn()] += it->getValue() * vector[currentRow]; } ++currentRow; } } template typename SparseMatrix::const_rows SparseMatrix::getRows(index_type startRow, index_type endRow) const { return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]); } template typename SparseMatrix::rows SparseMatrix::getRows(index_type startRow, index_type endRow) { return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]); } template typename SparseMatrix::const_rows SparseMatrix::getRow(index_type row) const { return getRows(row, row + 1); } template typename SparseMatrix::rows SparseMatrix::getRow(index_type row) { return getRows(row, row + 1); } template typename SparseMatrix::const_rows SparseMatrix::getRow(index_type rowGroup, index_type offset) const { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); STORM_LOG_ASSERT(offset < this->getRowGroupEntryCount(rowGroup), "Row offset in row-group is out-of-bounds."); if (!this->hasTrivialRowGrouping()) { return getRow(this->getRowGroupIndices()[rowGroup] + offset); } else { return getRow(this->getRowGroupIndices()[rowGroup] + offset); } } template typename SparseMatrix::rows SparseMatrix::getRow(index_type rowGroup, index_type offset) { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); STORM_LOG_ASSERT(offset < this->getRowGroupEntryCount(rowGroup), "Row offset in row-group is out-of-bounds."); if (!this->hasTrivialRowGrouping()) { return getRow(this->getRowGroupIndices()[rowGroup] + offset); } else { STORM_LOG_ASSERT(offset == 0, "Invalid offset."); return getRow(rowGroup + offset); } } template typename SparseMatrix::const_rows SparseMatrix::getRowGroup(index_type rowGroup) const { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); if (!this->hasTrivialRowGrouping()) { return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]); } else { return getRows(rowGroup, rowGroup + 1); } } template typename SparseMatrix::rows SparseMatrix::getRowGroup(index_type rowGroup) { STORM_LOG_ASSERT(rowGroup < this->getRowGroupCount(), "Row group is out-of-bounds."); if (!this->hasTrivialRowGrouping()) { return getRows(this->getRowGroupIndices()[rowGroup], this->getRowGroupIndices()[rowGroup + 1]); } else { return getRows(rowGroup, rowGroup + 1); } } template typename SparseMatrix::const_iterator SparseMatrix::begin(index_type row) const { return this->columnsAndValues.begin() + this->rowIndications[row]; } template typename SparseMatrix::iterator SparseMatrix::begin(index_type row) { return this->columnsAndValues.begin() + this->rowIndications[row]; } template typename SparseMatrix::const_iterator SparseMatrix::end(index_type row) const { return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } template typename SparseMatrix::iterator SparseMatrix::end(index_type row) { return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } template typename SparseMatrix::const_iterator SparseMatrix::end() const { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } template typename SparseMatrix::iterator SparseMatrix::end() { return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } template bool SparseMatrix::hasTrivialRowGrouping() const { return trivialRowGrouping; } template ValueType SparseMatrix::getRowSum(index_type row) const { ValueType sum = storm::utility::zero(); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { sum += it->getValue(); } return sum; } template typename SparseMatrix::index_type SparseMatrix::getNonconstantEntryCount() const { index_type nonConstEntries = 0; for( auto const& entry : *this){ if(!storm::utility::isConstant(entry.getValue())){ ++nonConstEntries; } } return nonConstEntries; } template typename SparseMatrix::index_type SparseMatrix::getNonconstantRowGroupCount() const { index_type nonConstRowGroups = 0; for (index_type rowGroup=0; rowGroup < this->getRowGroupCount(); ++rowGroup) { for( auto const& entry : this->getRowGroup(rowGroup)){ if(!storm::utility::isConstant(entry.getValue())){ ++nonConstRowGroups; break; } } } return nonConstRowGroups; } template bool SparseMatrix::isProbabilistic() const { storm::utility::ConstantsComparator comparator; for(index_type row = 0; row < this->rowCount; ++row) { if(!comparator.isOne(getRowSum(row))) { return false; } } return true; } template 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->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping()) return false; if (!this->hasTrivialRowGrouping() && matrix.hasTrivialRowGrouping()) return false; if (!this->hasTrivialRowGrouping() && !matrix.hasTrivialRowGrouping() && this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false; if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false; // Check the subset property for all rows individually. for (index_type row = 0; row < this->getRowCount(); ++row) { auto it2 = matrix.begin(row); auto ite2 = matrix.end(row); for (const_iterator it1 = this->begin(row), ite1 = this->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()) { ++it2; } if (it2 == ite2 || it1->getColumn() != it2->getColumn()) { return false; } } } return true; } template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { // Print column numbers in header. out << "\t\t"; for (typename SparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; // Iterate over all row groups. for (typename SparseMatrix::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { out << "\t---- group " << group << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl; typename SparseMatrix::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; typename SparseMatrix::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; for (typename SparseMatrix::index_type i = start; i < end; ++i) { typename SparseMatrix::index_type nextIndex = matrix.rowIndications[i]; // Print the actual row. out << i << "\t(\t"; typename SparseMatrix::index_type currentRealIndex = 0; while (currentRealIndex < matrix.columnCount) { if (nextIndex < matrix.rowIndications[i + 1] && currentRealIndex == matrix.columnsAndValues[nextIndex].getColumn()) { out << matrix.columnsAndValues[nextIndex].getValue() << "\t"; ++nextIndex; } else { out << "0\t"; } ++currentRealIndex; } out << "\t)\t" << i << std::endl; } } // Print column numbers in footer. out << "\t\t"; for (typename SparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { out << i << "\t"; } out << std::endl; return out; } template void SparseMatrix::printAsMatlabMatrix(std::ostream& out) const { // Iterate over all row groups. for (typename SparseMatrix::index_type group = 0; group < this->getRowGroupCount(); ++group) { STORM_LOG_ASSERT(this->getRowGroupSize(group) == 1, "Incorrect row group size."); for (typename SparseMatrix::index_type i = this->getRowGroupIndices()[group]; i < this->getRowGroupIndices()[group + 1]; ++i) { typename SparseMatrix::index_type nextIndex = this->rowIndications[i]; // Print the actual row. out << i << "\t("; typename SparseMatrix::index_type currentRealIndex = 0; while (currentRealIndex < this->columnCount) { if (nextIndex < this->rowIndications[i + 1] && currentRealIndex == this->columnsAndValues[nextIndex].getColumn()) { out << this->columnsAndValues[nextIndex].getValue() << " "; ++nextIndex; } else { out << "0 "; } ++currentRealIndex; } out << ";" << std::endl; } } } template std::size_t SparseMatrix::hash() const { std::size_t result = 0; boost::hash_combine(result, this->getRowCount()); boost::hash_combine(result, this->getColumnCount()); boost::hash_combine(result, this->getEntryCount()); boost::hash_combine(result, boost::hash_range(columnsAndValues.begin(), columnsAndValues.end())); boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end())); if (!this->hasTrivialRowGrouping()) { boost::hash_combine(result, boost::hash_range(rowGroupIndices.get().begin(), rowGroupIndices.get().end())); } return result; } #ifdef STORM_HAVE_CARL std::set getVariables(SparseMatrix const& matrix) { std::set result; for(auto const& entry : matrix) { entry.getValue().gatherVariables(result); } return result; } #endif // Explicitly instantiate the entry, builder and the matrix. // double template class MatrixEntry::index_type, double>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, double> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; template class MatrixEntry; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); // float template class MatrixEntry::index_type, float>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, float> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; // int template class MatrixEntry::index_type, int>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, int> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; // state_type template class MatrixEntry::index_type, storm::storage::sparse::state_type>; template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, storm::storage::sparse::state_type> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #ifdef STORM_HAVE_CARL // Rat Number template class MatrixEntry::index_type, RationalNumber>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; // Rat Function template class MatrixEntry::index_type, RationalFunction>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; // Intervals template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template class MatrixEntry::index_type, Interval>; template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; #endif } // namespace storage } // namespace storm