From efd430a33f94adcd6dedf310860d04538fb9bec6 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 13 Mar 2017 17:00:25 +0100
Subject: [PATCH] fixes regarding state elimination on mdps

---
 src/storm/modelchecker/parametric/ParameterLifting.cpp | 2 +-
 src/storm/solver/stateelimination/EliminatorBase.cpp   | 6 +++---
 src/storm/storage/FlexibleSparseMatrix.cpp             | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp
index 74240043b..e5d21d941 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@@ -143,7 +143,7 @@ namespace storm {
                 
                 while (fractionOfUndiscoveredArea > threshold) {
                     STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
-                    STORM_LOG_INFO("Analyzing region #" << regions.size() -1 << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
+                    STORM_LOG_INFO("Analyzing region #" << indexOfCurrentRegion << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
                     auto const& currentRegion = regions[indexOfCurrentRegion].first;
                     auto& res = regions[indexOfCurrentRegion].second;
                     res = analyzeRegion(currentRegion, res, false);
diff --git a/src/storm/solver/stateelimination/EliminatorBase.cpp b/src/storm/solver/stateelimination/EliminatorBase.cpp
index 7eeb4eb27..041b610bf 100644
--- a/src/storm/solver/stateelimination/EliminatorBase.cpp
+++ b/src/storm/solver/stateelimination/EliminatorBase.cpp
@@ -207,7 +207,7 @@ namespace storm {
                             break;
                         }
                         if (first2->getColumn() < first1->getColumn()) {
-                            if (first2->getColumn() != column) {
+                            if (first2->getColumn() != row) {
                                 *result = *first2;
                             }
                             ++first2;
@@ -225,9 +225,9 @@ namespace storm {
                         }
                     }
                     if (isFilterPredecessor()) {
-                        std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != column && filterPredecessor(a.getColumn()); });
+                        std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != row && filterPredecessor(a.getColumn()); });
                     } else {
-                        std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != column; });
+                        std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename storm::storage::FlexibleSparseMatrix<ValueType>::index_type, typename storm::storage::FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != row; });
                     }
                     // Now move the new predecessors in place.
                     successorBackwardTransitions = std::move(newPredecessors);
diff --git a/src/storm/storage/FlexibleSparseMatrix.cpp b/src/storm/storage/FlexibleSparseMatrix.cpp
index 29308f410..1b3534eee 100644
--- a/src/storm/storage/FlexibleSparseMatrix.cpp
+++ b/src/storm/storage/FlexibleSparseMatrix.cpp
@@ -234,7 +234,7 @@ namespace storm {
                 oldToNewColumnIndexMapping[oldColumnIndex] = newColumnIndex++;
             }
             
-            storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, hasTrivialRowGrouping(), numRowGroups);
+            storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder(rowConstraint.getNumberOfSetBits(), newColumnIndex, numEntries, true, hasTrivialRowGrouping(), numRowGroups);
             uint_fast64_t currRowIndex = 0;
             auto rowGroupIndexIt = getRowGroupIndices().begin();
             for (auto const& oldRowIndex : rowConstraint) {
@@ -243,7 +243,7 @@ namespace storm {
                     // Skip empty row groups
                     do {
                         ++rowGroupIndexIt;
-                    } while (currRowIndex >= *rowGroupIndexIt);
+                    } while (oldRowIndex >= *rowGroupIndexIt);
                 }
                 auto const& row = data[oldRowIndex];
                 for (auto const& entry : row) {