Started to add row-grouping to sparse matrix class.

Former-commit-id: 39e3703095

src/adapters/ExplicitModelAdapter.h

@@ -542,6 +542,7 @@ namespace storm {
                         } else {
                             // If the model is nondeterministic, we add all choices individually.
                             nondeterministicChoiceIndices.push_back(currentRow);
+                            transitionMatrixBuilder.addRowGroup();
                             
                             // First, process all unlabeled choices.
                             for (auto const& choice : allUnlabeledChoices) {
@@ -631,8 +632,8 @@ namespace storm {
                 bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC;
 
                 // Build the transition and reward matrices.
-                storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder;
-                storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder;
+                storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
+                storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0);
                 std::pair<std::vector<uint_fast64_t>, std::vector<boost::container::flat_set<uint_fast64_t>>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
                 modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first);
                 modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second);

src/modelchecker/prctl/AbstractModelChecker.h

@@ -177,7 +177,7 @@ public:
 			result = this->checkNoBoundOperator(noBoundFormula);
 			LOG4CPLUS_INFO(logger, "Result for initial states:");
 			std::cout << "Result for initial states:" << std::endl;
-			for (auto initialState : model.getInitialStates()) {
+            for (auto initialState : model.getInitialStates()) {
 				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
 				std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
 			}

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -284,23 +284,23 @@ namespace storm {
                  */
                 static std::pair<std::vector<Type>, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, std::vector<uint_fast64_t> nondeterministicChoiceIndices, storm::storage::SparseMatrix<Type> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver, bool qualitative) {
                     size_t numberOfStates = phiStates.size();
-                    
+
                     // We need to identify the states which have to be taken out of the matrix, i.e.
                     // all states that have probability 0 and 1 of satisfying the until-formula.
                     std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
                     if (minimize) {
                         statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
+
                     } else {
                         statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, phiStates, psiStates);
                     }
                     storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
                     storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
-                    
                     storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
                     LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
                     LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
                     LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-                    
+
                     // Create resulting vector.
                     std::vector<Type> result(numberOfStates);
                     
@@ -317,7 +317,7 @@ namespace storm {
                         storm::utility::vector::setVectorValues<Type>(result, maybeStates, Type(0.5));
                     } else {
                         // In this case we have have to compute the probabilities.
-                        
+
                         // First, we can eliminate the rows and columns from the original transition probability matrix for states
                         // whose probabilities are already known.
                         storm::storage::SparseMatrix<Type> submatrix = transitionMatrix.getSubmatrix(maybeStates, nondeterministicChoiceIndices);

src/models/AbstractModel.h

@@ -194,7 +194,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
          * @return A sparse matrix that represents the backward transitions of this model.
          */
         storm::storage::SparseMatrix<T> getBackwardTransitions() const {
-            return this->transitionMatrix.transpose();
+            return this->transitionMatrix.transpose(true);
         }
 
         /*!

src/models/AbstractNondeterministicModel.h

@@ -123,46 +123,7 @@ namespace storm {
              * @return A sparse matrix that represents the backward transitions of this model.
              */
             storm::storage::SparseMatrix<T> getBackwardTransitions() const {
-                uint_fast64_t numberOfStates = this->getNumberOfStates();
-                uint_fast64_t numberOfTransitions = this->getTransitionMatrix().getEntryCount();
-
-                std::vector<uint_fast64_t> rowIndications(numberOfStates + 1);
-                std::vector<std::pair<uint_fast64_t, T>> columnsAndValues(numberOfTransitions, std::make_pair(0, storm::utility::constantZero<T>()));
-
-                // First, we need to count how many backward transitions each state has.
-                for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
-                    typename storm::storage::SparseMatrix<T>::const_rows rows = this->getRows(i);
-                    for (auto const& transition : rows) {
-                        if (transition.second > 0) {
-                            ++rowIndications[transition.first + 1];
-                        }
-                    }
-                }
-
-                // Now compute the accumulated offsets.
-                for (uint_fast64_t i = 1; i < numberOfStates + 1; ++i) {
-                    rowIndications[i] = rowIndications[i - 1] + rowIndications[i];
-                }
-
-                // Create an array that stores the next index for each state. Initially
-                // this corresponds to the previously computed accumulated offsets.
-                std::vector<uint_fast64_t> nextIndices = rowIndications;
-
-                // Now we are ready to actually fill in the list of predecessors for
-                // every state. Again, we start by considering all but the last row.
-                for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
-                    typename storm::storage::SparseMatrix<T>::const_rows rows = this->getRows(i);
-                    for (auto const& transition : rows) {
-                        if (transition.second > 0) {
-                            columnsAndValues[nextIndices[transition.first]] = std::make_pair(i, transition.second);
-                            ++nextIndices[transition.first];
-                        }
-                    }
-                }
-
-                storm::storage::SparseMatrix<T> backwardTransitionMatrix(numberOfStates, std::move(rowIndications), std::move(columnsAndValues));
-
-                return backwardTransitionMatrix;
+                return this->getTransitionMatrix().transpose(true);
             }
 
             /*!

src/storage/SparseMatrix.cpp

@@ -18,7 +18,7 @@ namespace storm {
     namespace storage {
         
         template<typename T>
-        SparseMatrixBuilder<T>::SparseMatrixBuilder(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0) {
+        SparseMatrixBuilder<T>::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) {
             this->prepareInternalStorage();
         }
         
@@ -68,6 +68,14 @@ namespace storm {
                         rowIndications.push_back(currentEntryCount);
                     }
                 }
+                
+                if (!hasCustomRowGrouping) {
+                    for (uint_fast64_t i = lastRow + 1; i <= row; ++i) {
+                        rowGroupIndices.push_back(row);
+                        ++currentRowGroup;
+                    }
+                }
+                
                 lastRow = row;
             }
             
@@ -86,14 +94,26 @@ namespace storm {
                 }
             }
             ++currentEntryCount;
-            
         }
         
         template<typename T>
-        SparseMatrix<T> SparseMatrixBuilder<T>::build(uint_fast64_t overriddenRowCount, uint_fast64_t overriddenColumnCount) {            
+        void SparseMatrixBuilder<T>::addRowGroup() {
+            if (!hasCustomRowGrouping) {
+                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::addRowGroup: matrix was not created to have a custom row grouping.";
+            }
+            if (rowGroupCountSet) {
+                rowGroupIndices[currentRowGroup] = lastRow + 1;
+                ++currentRowGroup;
+            } else {
+                rowGroupIndices.push_back(lastRow + 1);
+            }
+        }
+        
+        template<typename T>
+        SparseMatrix<T> SparseMatrixBuilder<T>::build(uint_fast64_t overriddenRowCount, uint_fast64_t overriddenColumnCount, uint_fast64_t 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::finalize: expected " << entryCount << " entries, but got " << currentEntryCount << " instead.";
+                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) {
@@ -122,20 +142,47 @@ namespace storm {
                 }
                 
                 entryCount = currentEntryCount;
+                
+                if (hasCustomRowGrouping && rowGroupCountSet) {
+                    rowGroupIndices[rowGroupCount] = rowCount;
+                } else {
+                    if (!hasCustomRowGrouping) {
+                        for (uint_fast64_t 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) {
+                            rowGroupIndices.push_back(rowCount);
+                        }
+                    }
+                }
             }
             
-            return SparseMatrix<T>(columnCount, std::move(rowIndications), std::move(columnsAndValues));
+            return SparseMatrix<T>(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
         }
         
         template<typename T>
         void SparseMatrixBuilder<T>::prepareInternalStorage() {
-            // Only allocate the memory if the dimensions of the matrix are already known.
+            // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known.
             if (storagePreallocated) {
                 columnsAndValues = std::vector<std::pair<uint_fast64_t, T>>(entryCount, std::make_pair(0, storm::utility::constantZero<T>()));
                 rowIndications = std::vector<uint_fast64_t>(rowCount + 1, 0);
             } else {
                 rowIndications.push_back(0);
             }
+            
+            // 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<uint_fast64_t>(rowGroupCount + 1, 0);
+            } else {
+                if (hasCustomRowGrouping) {
+                    // Nothing to do in this case
+                } else {
+                    rowGroupIndices.push_back(0);
+                }
+            }
         }
         
         template<typename T>
@@ -169,17 +216,17 @@ namespace storm {
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications() {
+        SparseMatrix<T>::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications(), rowGroupIndices() {
             // Intentionally left empty.
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(SparseMatrix<T> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications) {
+        SparseMatrix<T>::SparseMatrix(SparseMatrix<T> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), rowGroupIndices(other.rowGroupIndices) {
             // Intentionally left empty.
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(SparseMatrix<T>&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)) {
+        SparseMatrix<T>::SparseMatrix(SparseMatrix<T>&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), 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;
@@ -187,12 +234,12 @@ namespace storm {
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications) {
+        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications), rowGroupIndices(rowGroupIndices) {
             // Intentionally left empty.
         }
         
         template<typename T>
-        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)) {
+        SparseMatrix<T>::SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues, std::vector<uint_fast64_t>&& rowGroupIndices) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), rowGroupIndices(std::move(rowGroupIndices)) {
             // Intentionally left empty.
         }
                 
@@ -206,6 +253,7 @@ namespace storm {
                 
                 columnsAndValues = other.columnsAndValues;
                 rowIndications = other.rowIndications;
+                rowGroupIndices = other.rowGroupIndices;
             }
             
             return *this;
@@ -221,6 +269,7 @@ namespace storm {
                 
                 columnsAndValues = std::move(other.columnsAndValues);
                 rowIndications = std::move(other.rowIndications);
+                rowGroupIndices = std::move(other.rowGroupIndices);
             }
             
             return *this;
@@ -236,6 +285,7 @@ namespace storm {
             
             equalityResult &= rowCount == other.rowCount;
             equalityResult &= columnCount == other.columnCount;
+            equalityResult &= rowGroupIndices == other.rowGroupIndices;
             
             // 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.
@@ -278,6 +328,11 @@ namespace storm {
             return entryCount;
         }
         
+        template<typename T>
+        uint_fast64_t SparseMatrix<T>::getRowGroupCount() const {
+            return rowGroupIndices.size() - 1;
+        }
+        
         template<typename T>
         void SparseMatrix<T>::makeRowsAbsorbing(storm::storage::BitVector const& rows) {
             for (auto row : rows) {
@@ -502,19 +557,19 @@ namespace storm {
         }
         
         template <typename T>
-        SparseMatrix<T> SparseMatrix<T>::transpose() const {
-            uint_fast64_t rowCount = this->columnCount;
-            uint_fast64_t columnCount = this->rowCount;
-            uint_fast64_t entryCount = this->entryCount;
+        SparseMatrix<T> SparseMatrix<T>::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();
             
             std::vector<uint_fast64_t> rowIndications(rowCount + 1);
             std::vector<std::pair<uint_fast64_t, T>> columnsAndValues(entryCount);
             
             // First, we need to count how many entries each column has.
-            for (uint_fast64_t row = 0; row < this->rowCount; ++row) {
-                for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
-                    if (it->second > 0) {
-                        ++rowIndications[it->first + 1];
+            for (uint_fast64_t group = 0; group < columnCount; ++group) {
+                for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) {
+                    if (transition.second != storm::utility::constantZero<T>()) {
+                        ++rowIndications[transition.first + 1];
                     }
                 }
             }
@@ -530,20 +585,25 @@ namespace storm {
             std::vector<uint_fast64_t> nextIndices = rowIndications;
             
             // Now we are ready to actually fill in the values of the transposed matrix.
-            for (uint_fast64_t row = 0; row < this->rowCount; ++row) {
-                for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) {
-                    if (it->second > 0) {
-                        columnsAndValues[nextIndices[it->first]] = std::make_pair(row, it->second);
-                        nextIndices[it->first]++;
+            for (uint_fast64_t group = 0; group < columnCount; ++group) {
+                for (auto const& transition : joinGroups ? this->getRowGroup(group) : this->getRow(group)) {
+                    if (transition.second != storm::utility::constantZero<T>()) {
+                        columnsAndValues[nextIndices[transition.first]] = std::make_pair(group, transition.second);
+                        nextIndices[transition.first]++;
                     }
                 }
             }
             
-            storm::storage::SparseMatrix<T> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues));
+            std::vector<uint_fast64_t> rowGroupIndices(rowCount + 1);
+            for (uint_fast64_t i = 0; i <= rowCount; ++i) {
+                rowGroupIndices[i] = i;
+            }
             
+            storm::storage::SparseMatrix<T> transposedMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
+                        
             return transposedMatrix;
         }
-        
+                
         template<typename T>
         void SparseMatrix<T>::convertToEquationSystem() {
             invertDiagonal();
@@ -738,6 +798,16 @@ namespace storm {
             return getRows(row, row);
         }
         
+        template<typename T>
+        typename SparseMatrix<T>::const_rows SparseMatrix<T>::getRowGroup(uint_fast64_t rowGroup) const {
+            return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1);
+        }
+        
+        template<typename T>
+        typename SparseMatrix<T>::rows SparseMatrix<T>::getRowGroup(uint_fast64_t rowGroup) {
+            return getRows(rowGroupIndices[rowGroup], rowGroupIndices[rowGroup + 1] - 1);
+        }
+        
         template<typename T>
         typename SparseMatrix<T>::const_iterator SparseMatrix<T>::begin(uint_fast64_t row) const {
             return this->columnsAndValues.begin() + this->rowIndications[row];

src/storage/SparseMatrix.h

@@ -39,8 +39,12 @@ namespace storm {
              * @param rows The number of rows of the resulting matrix.
              * @param columns The number of columns of the resulting matrix.
              * @param entries The number of entries of the resulting matrix.
+             * @param hasCustomRowGrouping A flag indicating whether the builder is used to create a non-canonical
+             * grouping of rows for this matrix.
+             * @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);
+            SparseMatrixBuilder(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0, bool hasCustomRowGrouping = false, uint_fast64_t rowGroups = 0);
             
             /*!
              * Sets the matrix entry at the given row and column to the given value. After all entries have been added,
@@ -57,6 +61,12 @@ namespace storm {
              */
             void addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value);
             
+            /*!
+             * Adds a new row group to the matrix. Note that this needs to be called before any entries in the new row
+             * group are added.
+             */
+            void addRowGroup();
+            
             /*
              * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix
              * may now be used. This must be called after all entries have been added to the matrix via addNextValue.
@@ -70,8 +80,13 @@ namespace storm {
              * *not* override the column count that has been given upon construction (if any), but will only take effect
              * if the matrix has been created without the number of columns given. By construction, the matrix will have
              * no entries in the columns that have been added this way.
+             * @param overriddenRowGroupCount If this is set to a value that is greater than the current number of row
+             * groups, this will cause the method to set the number of row groups to the given value. Note that this will
+             * *not* override the row group count that has been given upon construction (if any), but will only take
+             * 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<T> build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0);
+            SparseMatrix<T> build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0, uint_fast64_t overriddenRowGroupCount = 0);
             
         private:
             /*!
@@ -96,6 +111,17 @@ namespace storm {
             // The number of entries in the matrix.
             uint_fast64_t entryCount;
             
+            // A flag indicating whether the builder is to construct a custom row grouping for the matrix.
+            bool hasCustomRowGrouping;
+            
+            // A flag indicating whether the number of row groups was set upon construction.
+            bool rowGroupCountSet;
+            
+            // The number of row groups in the matrix.
+            uint_fast64_t rowGroupCount;
+            
+            std::vector<uint_fast64_t> rowGroupIndices;
+            
             // Stores whether the storage of the matrix was preallocated or not.
             bool storagePreallocated;
             
@@ -119,6 +145,10 @@ namespace storm {
             // 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;
+            
+            // Stores the currently active row group. This is used for correctly constructing the row grouping of the
+            // matrix.
+            uint_fast64_t currentRowGroup;
         };
         
         /*!
@@ -250,8 +280,9 @@ namespace storm {
              * @param columnCount The number of columns of the matrix.
              * @param rowIndications The row indications vector of the matrix to be constructed.
              * @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<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues);
+            SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t> const& rowIndications, std::vector<std::pair<uint_fast64_t, T>> const& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupIndices);
             
             /*!
              * Constructs a sparse matrix by moving the given contents.
@@ -259,8 +290,9 @@ namespace storm {
              * @param columnCount The number of columns of the matrix.
              * @param rowIndications The row indications vector of the matrix to be constructed.
              * @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<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues);
+            SparseMatrix(uint_fast64_t columnCount, std::vector<uint_fast64_t>&& rowIndications, std::vector<std::pair<uint_fast64_t, T>>&& columnsAndValues, std::vector<uint_fast64_t>&& rowGroupIndices);
 
             /*!
              * Assigns the contents of the given matrix to the current one by deep-copying its contents.
@@ -305,6 +337,13 @@ namespace storm {
              */
             uint_fast64_t getEntryCount() const;
             
+            /*!
+             * Returns the number of row groups in the matrix.
+             *
+             * @return The number of row groups in the matrix.
+             */
+            uint_fast64_t getRowGroupCount() const;
+            
             /*!
              * This function makes the given rows absorbing.
              *
@@ -411,9 +450,11 @@ namespace storm {
             /*!
              * Transposes the matrix.
              *
+             * @param joinGroups A flag indicating whether the row groups are supposed to be treated as single rows.
+             *
              * @return A sparse matrix that represents the transpose of this matrix.
              */
-            storm::storage::SparseMatrix<T> transpose() const;
+            storm::storage::SparseMatrix<T> transpose(bool joinGroups = false) const;
             
             /*!
              * Transforms the matrix into an equation system. That is, it transforms the matrix A into a matrix (1-A).
@@ -498,6 +539,22 @@ namespace storm {
              */
             rows getRow(uint_fast64_t row);
             
+            /*!
+             * Returns an object representing the given row group.
+             *
+             * @param rowGroup The row group to get.
+             * @return An object representing the given row group.
+             */
+            const_rows getRowGroup(uint_fast64_t rowGroup) const;
+            
+            /*!
+             * Returns an object representing the given row group.
+             *
+             * @param rowGroup The row group to get.
+             * @return An object representing the given row group.
+             */
+            rows getRowGroup(uint_fast64_t rowGroup);
+            
             /*!
              * Retrieves an iterator that points to the beginning of the given row.
              *
@@ -596,6 +653,9 @@ namespace storm {
             // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last
             // entry is not included anymore.
             std::vector<uint_fast64_t> rowIndications;
+            
+            // A vector indicating the row groups of the matrix.
+            std::vector<uint_fast64_t> rowGroupIndices;
         };
 
     } // namespace storage

test/functional/solver/GurobiLpSolverTest.cpp

@@ -14,7 +14,7 @@ TEST(GurobiLpSolver, LPOptimizeMax) {
     ASSERT_NO_THROW(yIndex = solver.createContinuousVariable("y", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 2));
     uint_fast64_t zIndex;
     ASSERT_NO_THROW(zIndex = solver.createContinuousVariable("z", storm::solver::LpSolver::VariableType::LOWER_BOUND, 0, 0, 1));
-    
+        
     ASSERT_NO_THROW(solver.addConstraint("", {xIndex, yIndex, zIndex}, {1, 1, 1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 12));
     ASSERT_NO_THROW(solver.addConstraint("", {yIndex, zIndex, xIndex}, {0.5, 1, -1}, storm::solver::LpSolver::BoundType::EQUAL, 5));
     ASSERT_NO_THROW(solver.addConstraint("", {yIndex, xIndex}, {1, -1}, storm::solver::LpSolver::BoundType::LESS_EQUAL, 5.5));

test/functional/storage/SparseMatrixTest.cpp

@@ -154,11 +154,12 @@ TEST(SparseMatrix, CreationWithMovingContents) {
     columnsAndValues.emplace_back(1, 0.7);
     columnsAndValues.emplace_back(3, 0.2);
     
-    ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues));
-    storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues);
+    ASSERT_NO_THROW(storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3}));
+    storm::storage::SparseMatrix<double> matrix(4, {0, 2, 5, 5}, columnsAndValues, {0, 1, 2, 3});
     ASSERT_EQ(3, matrix.getRowCount());
     ASSERT_EQ(4, matrix.getColumnCount());
     ASSERT_EQ(5, matrix.getEntryCount());
+    ASSERT_EQ(3, matrix.getRowGroupCount());
 }
 
 TEST(SparseMatrix, CopyConstruct) {