From 8e3e99c4cebbf4ff6f7b1cb4b5363648018f75c4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 6 Nov 2017 21:32:06 +0100
Subject: [PATCH] fixed bug in submatrix computation pointed out by Timo Gros

---
 src/storm/storage/SparseMatrix.cpp | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index bf1b15d14..d4c9ba5ad 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -897,12 +897,11 @@ namespace storm {
             // Start by creating a temporary vector that stores for each index whose bit is set to true the number of
             // bits that were set before that particular index.
             std::vector<index_type> columnBitsSetBeforeIndex = columnConstraint.getNumberOfSetBitsBeforeIndices();
-            std::vector<index_type>* rowBitsSetBeforeIndex;
-            if (&rowGroupConstraint == &columnConstraint) {
-                rowBitsSetBeforeIndex = &columnBitsSetBeforeIndex;
-            } else {
-                rowBitsSetBeforeIndex = new std::vector<index_type>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices());
+            std::unique_ptr<std::vector<index_type>> tmp;
+            if (rowGroupConstraint != columnConstraint) {
+                tmp = std::make_unique<std::vector<index_type>>(rowGroupConstraint.getNumberOfSetBitsBeforeIndices());
             }
+            std::vector<index_type> const& rowBitsSetBeforeIndex = tmp ? *tmp : columnBitsSetBeforeIndex;
             
             // Then, we need to determine the number of entries and the number of rows of the submatrix.
             index_type subEntries = 0;
@@ -917,7 +916,7 @@ namespace storm {
                         if (columnConstraint.get(it->getColumn())) {
                             ++subEntries;
                             
-                            if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) {
+                            if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
                                 foundDiagonalElement = true;
                             }
                         }
@@ -946,9 +945,9 @@ namespace storm {
                     
                     for (const_iterator it = this->begin(i), ite = this->end(i); it != ite; ++it) {
                         if (columnConstraint.get(it->getColumn())) {
-                            if (columnBitsSetBeforeIndex[it->getColumn()] == (*rowBitsSetBeforeIndex)[index]) {
+                            if (columnBitsSetBeforeIndex[it->getColumn()] == rowBitsSetBeforeIndex[index]) {
                                 insertedDiagonalElement = true;
-                            } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > (*rowBitsSetBeforeIndex)[index]) {
+                            } else if (insertDiagonalEntries && !insertedDiagonalElement && columnBitsSetBeforeIndex[it->getColumn()] > rowBitsSetBeforeIndex[index]) {
                                 matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
                                 insertedDiagonalElement = true;
                             }
@@ -956,18 +955,13 @@ namespace storm {
                         }
                     }
                     if (insertDiagonalEntries && !insertedDiagonalElement && rowGroupCount < submatrixColumnCount) {
-                        matrixBuilder.addNextValue(rowGroupCount, rowGroupCount, storm::utility::zero<ValueType>());
+                        matrixBuilder.addNextValue(rowCount, rowGroupCount, storm::utility::zero<ValueType>());
                     }
                     ++rowCount;
                 }
                 ++rowGroupCount;
             }
             
-            // If the constraints were not the same, we have allocated some additional memory we need to free now.
-            if (&rowGroupConstraint != &columnConstraint) {
-                delete rowBitsSetBeforeIndex;
-            }
-            
             return matrixBuilder.build();
         }