diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 81e87ce20..99ed68337 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -16,9 +16,6 @@ namespace storm { FlexibleSparseMatrix::FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) : data(matrix.getRowCount()), columnCount(matrix.getColumnCount()), nonzeroEntryCount(matrix.getNonzeroEntryCount()), nontrivialRowGrouping(matrix.hasNontrivialRowGrouping()) { if (nontrivialRowGrouping) { rowGroupIndices = matrix.getRowGroupIndices(); - rowIndications = matrix.getRowIndications(); - // Not fully implemented yet - assert(false); } for (index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { typename storm::storage::SparseMatrix::const_rows row = matrix.getRow(rowIndex); @@ -52,6 +49,20 @@ namespace storm { return this->data[index]; } + template + typename FlexibleSparseMatrix::row_type& FlexibleSparseMatrix::getRow(index_type rowGroup, index_type offset) { + assert(rowGroup < this->getRowGroupCount()); + assert(offset < this->getRowGroupSize(rowGroup)); + return getRow(rowGroupIndices[rowGroup] + offset); + } + + template + typename FlexibleSparseMatrix::row_type const& FlexibleSparseMatrix::getRow(index_type rowGroup, index_type offset) const { + assert(rowGroup < this->getRowGroupCount()); + assert(offset < this->getRowGroupSize(rowGroup)); + return getRow(rowGroupIndices[rowGroup] + offset); + } + template typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getRowCount() const { return this->data.size(); @@ -66,6 +77,20 @@ namespace storm { typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getNonzeroEntryCount() const { return nonzeroEntryCount; } + + template + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getRowGroupCount() const { + return rowGroupIndices.size(); + } + + template + typename FlexibleSparseMatrix::index_type FlexibleSparseMatrix::getRowGroupSize(index_type group) const { + if (group == getRowGroupCount() - 1) { + return getRowCount() - rowGroupIndices[group]; + } else { + return rowGroupIndices[group + 1] - rowGroupIndices[group]; + } + } template void FlexibleSparseMatrix::updateDimensions() { @@ -91,7 +116,7 @@ namespace storm { } template - bool SparseMatrix::hasNontrivialRowGrouping() const { + bool FlexibleSparseMatrix::hasNontrivialRowGrouping() const { return nontrivialRowGrouping; } @@ -142,13 +167,50 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix const& matrix) { - for (uint_fast64_t index = 0; index < matrix->data.size(); ++index) { - out << index << " - "; - for (auto const& element : matrix->getRow(index)) { - out << "(" << element.getColumn() << ", " << element.getValue() << ") "; + // Print column numbers in header. + out << "\t\t"; + for (typename FlexibleSparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { + out << i << "\t"; + } + out << std::endl; + + typename FlexibleSparseMatrix::index_type endIndex = matrix.hasNontrivialRowGrouping() ? matrix.getRowGroupCount() : matrix.getRowCount(); + // Iterate over all rows. + for (typename SparseMatrix::index_type i = 0; i < endIndex; ++i) { + if (matrix.hasNontrivialRowGrouping()) { + out << "\t---- group " << i << "/" << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl; } - return out; + typename FlexibleSparseMatrix::index_type startRow = matrix.hasNontrivialRowGrouping() ? matrix.rowGroupIndices[i] : i; + typename FlexibleSparseMatrix::index_type endRow = matrix.hasNontrivialRowGrouping() ? matrix.rowGroupIndices[i + 1] : i+1; + for (typename FlexibleSparseMatrix::index_type rowIndex = startRow; rowIndex < endRow; ++rowIndex) { + // Print the actual row. + out << i << "\t(\t"; + typename FlexibleSparseMatrix::row_type row = matrix.getRow(rowIndex); + typename FlexibleSparseMatrix::index_type columnIndex = 0; + for (auto const& entry : row) { + //Insert zero between entries. + while (columnIndex < entry.getColumn()) { + out << "0\t"; + ++columnIndex; + } + ++columnIndex; + out << entry.getValue() << "\t"; + } + //Insert remaining zeros. + while (columnIndex++ <= matrix.getColumnCount()) { + out << "0\t"; + } + out << "\t)\t" << i << std::endl; + } + } + + // Print column numbers in footer. + out << "\t\t"; + for (typename FlexibleSparseMatrix::index_type i = 0; i < matrix.getColumnCount(); ++i) { + out << i << "\t"; } + out << std::endl; + return out; } // Explicitly instantiate the matrix. diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index 295b0337b..5ab573057 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -71,6 +71,22 @@ namespace storm { * @return An object representing the given row. */ row_type const& getRow(index_type) const; + + /*! + * Returns an object representing the offset'th row in the rowgroup + * @param rowGroup the row group + * @param offset which row in the group + * @return An object representing the given row. + */ + row_type& getRow(index_type rowGroup, index_type offset); + + /*! + * Returns an object representing the offset'th row in the rowgroup + * @param rowGroup the row group + * @param offset which row in the group + * @return An object representing the given row. + */ + row_type const& getRow(index_type rowGroup, index_type entryInGroup) const; /*! * Returns the number of rows of the matrix. @@ -92,6 +108,21 @@ namespace storm { * @return The number of nonzero entries in the matrix. */ index_type getNonzeroEntryCount() const; + + /*! + * Returns the number of row groups in the matrix. + * + * @return The number of row groups in the matrix. + */ + index_type getRowGroupCount() const; + + /*! + * Returns the size of the given row group. + * + * @param group The group whose size to retrieve. + * @return The number of rows that belong to the given row group. + */ + index_type getRowGroupSize(index_type group) const; /*! * Recomputes the number of columns and the number of non-zero entries. @@ -146,10 +177,6 @@ namespace storm { // The number of entries in the matrix. index_type nonzeroEntryCount; - // A vector containing the indices at which each given row begins. The values of the entries in row i are - // data[rowIndications[i]] to data[rowIndications[i + 1]] where the last entry is not included anymore. - std::vector rowIndications; - // A flag that indicates whether the matrix has a non-trivial row-grouping, i.e. (possibly) more than one // row per row group. bool nontrivialRowGrouping; diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 04e941561..65f74d874 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -452,11 +452,6 @@ namespace storm { return rowGroupIndices; } - template - std::vector::index_type> const& SparseMatrix::getRowIndications() const { - return rowIndications; - } - template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { for (auto row : rows) { diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 94defdfa5..f9d9916c4 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -549,13 +549,6 @@ namespace storm { */ std::vector const& getRowGroupIndices() const; - /*! - * Returns the indices where new row groups start. - * - * @return The indices where new row groups start. - */ - std::vector const& getRowIndications() const; - /*! * This function makes the given rows absorbing. *