From d3b0046fa05661be551b938c36c2c2c104125508 Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Tue, 31 Aug 2021 08:34:45 +0200
Subject: [PATCH] fixed bug in reduce method in Multiplier.cpp for SMGs and
 MDPs

---
 .../SparseNondeterministicStepBoundedHorizonHelper.cpp   | 3 ++-
 .../modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp   | 4 +++-
 src/storm/solver/Multiplier.cpp                          | 9 +++++++--
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
index ea1948d54..8e3da6930 100644
--- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
+++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
@@ -20,10 +20,11 @@ namespace storm {
             template<typename ValueType>
             void SparseNondeterministicStepBoundedHorizonHelper<ValueType>::getMaybeStatesRowGroupSizes(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, std::vector<uint64_t>& maybeStatesRowGroupSizes, uint& choiceValuesCounter) {
                 std::vector<uint64_t> rowGroupIndices = transitionMatrix.getRowGroupIndices();
+                choiceValuesCounter = 0;
                 for(uint counter = 0; counter < maybeStates.size(); counter++) {
                     if(maybeStates.get(counter)) {
-                        maybeStatesRowGroupSizes.push_back(rowGroupIndices.at(counter));
                         choiceValuesCounter += transitionMatrix.getRowGroupSize(counter);
+                        maybeStatesRowGroupSizes.push_back(choiceValuesCounter);
                     }
                 }
             }
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index 2a352c381..139165ee3 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -110,7 +110,9 @@ namespace storm {
                 }
                 // Create a multiplier for reduction.
                 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
-                multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition);
+                auto rowGroupIndices = transitionMatrix.getRowGroupIndices();
+                rowGroupIndices.erase(rowGroupIndices.begin());
+                multiplier->reduce(env, goal.direction(), b, rowGroupIndices, result, &statesOfCoalition);
                 if (goal.isShieldingTask()) {
                     choiceValues = b;
                 }
diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp
index 2324b7833..e5df00b05 100644
--- a/src/storm/solver/Multiplier.cpp
+++ b/src/storm/solver/Multiplier.cpp
@@ -92,8 +92,13 @@ namespace storm {
         template<typename ValueType>
         void Multiplier<ValueType>::reduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& choiceValues, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices, std::vector<ValueType>& result, storm::storage::BitVector const* dirOverride) const {
             auto choice_it = choiceValues.begin();
-            for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
-                uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
+            for(uint state = 0; state < rowGroupIndices.size(); state++) {
+                uint rowGroupSize;
+                if(state == 0) {
+                    rowGroupSize = rowGroupIndices[state];
+                } else {
+                    rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state-1];
+                }
                 if(dirOverride != nullptr) {
                     if((dir == storm::OptimizationDirection::Minimize && !dirOverride->get(state)) || (dir == storm::OptimizationDirection::Maximize && dirOverride->get(state))) {
                         result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize);