From a95ff3056a29abe6bf52c82d832bdd5546f8e380 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 1 Jul 2021 12:34:07 +0200
Subject: [PATCH] Fixed incorrect results for PcaaWeightVectorChecker.

---
 .../multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp  | 5 +++--
 .../multiobjective/pcaa/StandardPcaaWeightVectorChecker.h    | 3 ++-
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 7447eaf4e..cbc140354 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -585,6 +585,7 @@ namespace storm {
                     }
                     ecQuotient->ecqStayInEcChoices = std::move(ecElimResult.sinkRows);
                     ecQuotient->origReward0Choices = std::move(newReward0Choices);
+                    ecQuotient->origTotalReward0Choices = std::move(newTotalReward0Choices);
                     ecQuotient->rowsWithSumLessOne = std::move(rowsWithSumLessOne);
                     ecQuotient->auxStateValues.resize(ecQuotient->matrix.getRowGroupCount());
                     ecQuotient->auxChoiceValues.resize(ecQuotient->matrix.getRowCount());
@@ -741,7 +742,7 @@ namespace storm {
                                     unprocessedStates.set(state, false);
                                     originalSolution[state] = ecqSolution[ecqState];
                                 }
-                                computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices);
+                                computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices, &ecQuotient->origTotalReward0Choices);
                                 // Clear bitvectors for next ecqState.
                                 ecStatesToProcess.clear();
                                 ecStatesToReach.clear();
@@ -801,7 +802,7 @@ namespace storm {
                                 unprocessedStates.set(state, false);
                                 originalSolution[state] = ecqSolution[ecqState];
                             }
-                            computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices);
+                            computeSchedulerProb1(transitionMatrix, backwardsTransitions, ecStatesToProcess, ecStatesToReach, originalOptimalChoices, &ecQuotient->origTotalReward0Choices);
                             // Clear bitvectors for next ecqState.
                             ecStatesToProcess.clear();
                             ecStatesToReach.clear();
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
index b59cd1336..d6a73f8e7 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
@@ -159,7 +159,8 @@ namespace storm {
                     std::vector<uint_fast64_t> originalToEcqStateMapping;
                     std::vector<storm::storage::FlatSetStateContainer> ecqToOriginalStateMapping;
                     storm::storage::BitVector ecqStayInEcChoices;
-                    storm::storage::BitVector origReward0Choices;
+                    storm::storage::BitVector origReward0Choices; // includes total and LRA rewards
+                    storm::storage::BitVector origTotalReward0Choices; // considers just total rewards
                     storm::storage::BitVector rowsWithSumLessOne;
                     
                     std::vector<ValueType> auxStateValues;