From 60670e1fb2c96a86343999991de7275bb95f1267 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 3 Mar 2020 14:38:26 +0100
Subject: [PATCH] SparseMatrix: fixed getConstraintRowSumVector which did not
 allocate enough space before filling the resulting vector.

---
 src/storm/storage/SparseMatrix.cpp | 21 ++++++++++++++++++++-
 src/storm/storage/SparseMatrix.h   |  5 +++++
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index ecf29de4a..59d158d96 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -586,6 +586,25 @@ namespace storm {
             return res;
         }
         
+        template<typename ValueType>
+        typename SparseMatrix<ValueType>::index_type SparseMatrix<ValueType>::getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const {
+            if (this->hasTrivialRowGrouping()) {
+                return groupConstraint.getNumberOfSetBits();
+            }
+            index_type numRows = 0;
+            index_type rowGroupIndex = groupConstraint.getNextSetIndex(0);
+            while (rowGroupIndex < this->getRowGroupCount()) {
+                index_type start = this->getRowGroupIndices()[rowGroupIndex];
+                rowGroupIndex = groupConstraint.getNextUnsetIndex(rowGroupIndex + 1);
+                index_type end = this->getRowGroupIndices()[rowGroupIndex];
+                // All rows with index in [start,end) are selected.
+                numRows += end - start;
+                rowGroupIndex = groupConstraint.getNextSetIndex(rowGroupIndex + 1);
+            }
+            return numRows;
+        }
+
+        
         template<typename ValueType>
         std::vector<typename SparseMatrix<ValueType>::index_type> const& SparseMatrix<ValueType>::getRowGroupIndices() const {
             // If there is no current row grouping, we need to create it.
@@ -874,7 +893,7 @@ namespace storm {
         template<typename ValueType>
         std::vector<ValueType> SparseMatrix<ValueType>::getConstrainedRowGroupSumVector(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint) const {
             std::vector<ValueType> result;
-            result.reserve(rowGroupConstraint.getNumberOfSetBits());
+            result.reserve(this->getNumRowsInRowGroups(rowGroupConstraint));
             if (!this->hasTrivialRowGrouping()) {
                 for (auto rowGroup : rowGroupConstraint) {
                     for (index_type row = this->getRowGroupIndices()[rowGroup]; row < this->getRowGroupIndices()[rowGroup + 1]; ++row) {
diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h
index d3bbb5930..ad9c00ecd 100644
--- a/src/storm/storage/SparseMatrix.h
+++ b/src/storm/storage/SparseMatrix.h
@@ -573,6 +573,11 @@ namespace storm {
              */
             index_type getSizeOfLargestRowGroup() const;
             
+            /*!
+             * Returns the total number of rows that are in one of the specified row groups.
+             */
+            index_type getNumRowsInRowGroups(storm::storage::BitVector const& groupConstraint) const;
+            
             /*!
              * Returns the grouping of rows of this matrix.
              *