diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index e0307344f..6467793c6 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -309,7 +309,7 @@ namespace storm { buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); // Initialize the model components with the obtained information. - storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getLastRowGroup()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); + storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); // Now finalize all reward models. for (auto& rewardModelBuilder : rewardModelBuilders) { diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 009e5ab0b..36dd5724e 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -87,7 +87,7 @@ namespace storm { } 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) { + 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), currentRowGroupCount(0) { // Prepare the internal storage. if (initialRowCountSet) { rowIndications.reserve(initialRowCount + 1); @@ -105,7 +105,7 @@ namespace storm { } 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), currentRowGroup() { + 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), currentRowGroupCount() { lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1; lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn(); @@ -117,7 +117,7 @@ namespace storm { if (!rowGroupIndices->empty()) { rowGroupIndices.get().pop_back(); } - currentRowGroup = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; + currentRowGroupCount = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1; } // Likewise, we need to 'open' the row indications again. @@ -191,7 +191,7 @@ namespace storm { 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; + ++currentRowGroupCount; // Close all rows from the most recent one to the starting row. for (index_type i = lastRow + 1; i < startingRow; ++i) { @@ -252,14 +252,14 @@ namespace storm { // Check whether row groups are missing some entries. if (hasCustomRowGrouping) { - uint_fast64_t rowGroupCount = currentRowGroup; + uint_fast64_t rowGroupCount = currentRowGroupCount; 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) { + for (index_type i = currentRowGroupCount; i <= rowGroupCount; ++i) { rowGroupIndices.get().push_back(rowCount); } } @@ -273,11 +273,11 @@ namespace storm { } template - typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getLastRowGroup() const { + typename SparseMatrixBuilder::index_type SparseMatrixBuilder::getCurrentRowGroupCount() const { if (this->hasCustomRowGrouping) { - return currentRowGroup; + return currentRowGroupCount; } else { - return getLastRow(); + return getLastRow() + 1; } } diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 98eb959b5..e07389e5a 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -220,11 +220,11 @@ namespace storm { index_type getLastRow() const; /*! - * Retrieves the most recently used row group. + * Retrieves the current row group count. * - * @return The most recently used row group. + * @return The current row group count. */ - index_type getLastRowGroup() const; + index_type getCurrentRowGroupCount() const; /*! * Retrieves the most recently used row. @@ -303,7 +303,7 @@ namespace storm { // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. - index_type currentRowGroup; + index_type currentRowGroupCount; }; /*!