diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index d41e2ef2c..fa95f3930 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -220,6 +220,73 @@ namespace storm { 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 + bool SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { + bool changed = false; + index_type maxColumn = 0; + for (auto& elem : columnsAndValues) { + if (elem.getColumn() >= offset) { + elem.setColumn(replacements[elem.getColumn() - offset]); + changed = true; + } + maxColumn = std::max(maxColumn, elem.getColumn()); + } + assert(changed || highestColumn == maxColumn); + highestColumn = maxColumn; + assert(changed || lastColumn == columnsAndValues[columnsAndValues.size() - 1].getColumn()); + lastColumn = columnsAndValues[columnsAndValues.size() - 1].getColumn(); + + if (changed) { + fixColumns(); + } + return changed; + } + + template + void SparseMatrixBuilder::fixColumns() { + // Sort columns per row + typename SparseMatrix::index_type endGroups; + typename SparseMatrix::index_type endRows; + for (index_type group = 0; group < rowGroupIndices.size(); ++group) { + endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size(); + for (index_type i = rowGroupIndices[group]; i < endGroups; ++i) { + endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); + // Sort the row + std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + [](MatrixEntry const& a, MatrixEntry const& b) { + return a.getColumn() < b.getColumn(); + }); + // Assert no equal elements + assert(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + [](MatrixEntry const& a, MatrixEntry const& b) { + return a.getColumn() <= b.getColumn(); + })); + } + } + } + template SparseMatrix::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index f9d9916c4..4892dbe32 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -217,6 +217,17 @@ namespace storm { */ index_type getLastColumn() const; + /*! + * Replaces all columns with id > offset according to replacements. + * Every state with id offset+i is replaced by the id in replacements[i]. + * Afterwards the columns are sorted. + * + * @param replacements Mapping indicating the replacements from offset+i -> value of i. + * @param offset Offset to add to each id in vector index. + * @return True if replacement took place, False if nothing changed. + */ + bool replaceColumns(std::vector const& replacements, index_type offset); + private: // A flag indicating whether a row count was set upon construction. bool initialRowCountSet; @@ -277,6 +288,11 @@ namespace storm { // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroup; + + /*! + * Fixes the matrix by sorting the columns to gain increasing order again. + */ + void fixColumns(); }; /*!