From b56cd07d0e3715c4f589433fc3ee27a444c3cb1c Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Sun, 15 Oct 2017 19:36:30 +0200
Subject: [PATCH] Consider only a submap of all epochsolutions for faster
 search

---
 .../MultiDimensionalRewardUnfolding.cpp       | 26 ++++++++++++++++---
 .../MultiDimensionalRewardUnfolding.h         | 14 +++++-----
 2 files changed, 29 insertions(+), 11 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
index ad680f154..3e6991854 100644
--- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
+++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
@@ -296,7 +296,15 @@ namespace storm {
                         break;
                     }
                 }
-                
+                std::map<Epoch, EpochSolution const*> subSolutions;
+                for (auto const& step : possibleEpochSteps) {
+                    Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, step);
+                    if (successorEpoch != epoch) {
+                        auto successorSolIt = epochSolutions.find(successorEpoch);
+                        STORM_LOG_ASSERT(successorSolIt != epochSolutions.end(), "Solution for successor epoch does not exist (anymore).");
+                        subSolutions.emplace(successorEpoch, &successorSolIt->second);
+                    }
+                }
                 epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
                 auto stepSolIt = epochModel.stepSolutions.begin();
                 for (auto const& reducedChoice : epochModel.stepChoices) {
@@ -328,16 +336,16 @@ namespace storm {
                     if (!containsLowerBoundedObjective && epochManager.compareEpochClass(epoch, successorEpoch)) {
                         for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
                             if (firstSuccessor) {
-                                choiceSolution = getScaledSolution(getStateSolution(successorEpoch, successor.getColumn()), successor.getValue());
+                                choiceSolution = getScaledSolution(getStateSolution(subSolutions, successorEpoch, successor.getColumn()), successor.getValue());
                                 firstSuccessor = false;
                             } else {
-                                addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue());
+                                addScaledSolution(choiceSolution, getStateSolution(subSolutions, successorEpoch, successor.getColumn()), successor.getValue());
                             }
                         }
                     } else {
                         for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
                             uint64_t successorProductState = productModel->transformProductState(successor.getColumn(), successorEpochClass, memoryState);
-                            SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState);
+                            SolutionType const& successorSolution = getStateSolution(subSolutions, successorEpoch, successorProductState);
                             if (firstSuccessor) {
                                 choiceSolution = getScaledSolution(successorSolution, successor.getValue());
                                 firstSuccessor = false;
@@ -573,6 +581,16 @@ namespace storm {
                 return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]];
             }
             
+            template<typename ValueType, bool SingleObjectiveMode>
+            typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(std::map<Epoch, EpochSolution const*> const& solutions, Epoch const& epoch, uint64_t const& productState) {
+                auto epochSolutionIt = solutions.find(epoch);
+                STORM_LOG_ASSERT(epochSolutionIt != solutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
+                auto const& epochSolution = *epochSolutionIt->second;
+                STORM_LOG_ASSERT(productState < epochSolution.productStateToSolutionVectorMap->size(), "Requested solution for epoch " << epochManager.toString(epoch) << " at an unexisting product state.");
+                STORM_LOG_ASSERT((*epochSolution.productStateToSolutionVectorMap)[productState] < epochSolution.solutions.size(), "Requested solution for epoch " << epochManager.toString(epoch) << " at a state for which no solution was stored.");
+                return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]];
+            }
+            
             template<typename ValueType, bool SingleObjectiveMode>
             typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getInitialStateResult(Epoch const& epoch) {
                 STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states.");
diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
index a269ab1e9..782f53b2f 100644
--- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
+++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
@@ -99,6 +99,13 @@ namespace storm {
                 std::string solutionToString(SolutionType const& solution) const;
                 
                 SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState);
+                struct EpochSolution {
+                    uint64_t count;
+                    std::shared_ptr<std::vector<uint64_t> const> productStateToSolutionVectorMap;
+                    std::vector<SolutionType> solutions;
+                };
+                std::map<Epoch, EpochSolution> epochSolutions;
+                SolutionType const& getStateSolution(std::map<Epoch, EpochSolution const*> const& solutions, Epoch const& epoch, uint64_t const& productState);
                 
                 storm::models::sparse::Mdp<ValueType> const& model;
                 std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> objectives;
@@ -117,13 +124,6 @@ namespace storm {
                 std::vector<Dimension<ValueType>> dimensions;
                 std::vector<storm::storage::BitVector> objectiveDimensions;
                 
-                struct EpochSolution {
-                    uint64_t count;
-                    std::shared_ptr<std::vector<uint64_t> const> productStateToSolutionVectorMap;
-                    std::vector<SolutionType> solutions;
-                };
-                std::map<Epoch, EpochSolution> epochSolutions;
-                
                 
                 storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4;
                 std::vector<uint64_t> epochModelSizes;