The solutions are now stored epoch-wise and will be erased as soon as all predecessor epochs are computed

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@@ -56,8 +56,8 @@ namespace storm {
                 ++numCheckedEpochs;
                 swEqBuilding.start();
                 
-                auto& result = cachedData.solutions;
-                result.resize(epochModel.epochInStates.getNumberOfSetBits(), typename MultiDimensionalRewardUnfolding<ValueType, false>::SolutionType());
+                std::vector<typename MultiDimensionalRewardUnfolding<ValueType, false>::SolutionType> result;
+                result.reserve(epochModel.epochInStates.getNumberOfSetBits());
                 uint64_t solutionSize = this->objectives.size() + 1;
                 
                 // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives
@@ -87,12 +87,10 @@ namespace storm {
                 cachedData.minMaxSolver->solveEquations(cachedData.xMinMax, cachedData.bMinMax);
                 swMinMaxSolving.stop();
                 swEqBuilding.start();
-                auto resultIt = result.begin();
                 for (auto const& state : epochModel.epochInStates) {
-                    resultIt->clear();
-                    resultIt->reserve(solutionSize);
-                    resultIt->push_back(cachedData.xMinMax[state]);
-                    ++resultIt;
+                    result.emplace_back();
+                    result.back().reserve(solutionSize);
+                    result.back().push_back(cachedData.xMinMax[state]);
                 }
                 
                 // Check whether the linear equation solver needs to be updated
@@ -144,7 +142,7 @@ namespace storm {
                     cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq);
                     swLinEqSolving.stop();
                     swEqBuilding.start();
-                    resultIt = result.begin();
+                    auto resultIt = result.begin();
                     for (auto const& state : epochModel.epochInStates) {
                         resultIt->push_back(x[state]);
                         ++resultIt;
@@ -152,7 +150,7 @@ namespace storm {
                 }
                 swEqBuilding.stop();
                 swAux3.stop();
-                rewardUnfolding.setSolutionForCurrentEpoch(result);
+                rewardUnfolding.setSolutionForCurrentEpoch(std::move(result));
             }
 
             template <class SparseMdpModelType>

src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp

@@ -29,12 +29,12 @@ namespace storm {
             }
             
             uint64_t const& EpochManager::getDimensionCount() const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 return dimensionCount;
             }
 
             bool EpochManager::compareEpochClass(Epoch const& epoch1, Epoch const& epoch2) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 uint64_t mask = dimensionBitMask;
                 for (uint64_t d = 0; d < dimensionCount; ++d) {
                     if (((epoch1 & mask) == mask) != ((epoch2 & mask) == mask)) {
@@ -48,7 +48,7 @@ namespace storm {
             }
             
             typename EpochManager::EpochClass EpochManager::getEpochClass(Epoch const& epoch) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 EpochClass result = 0;
                 uint64_t mask = dimensionBitMask;
                 for (uint64_t d  = 0; d < dimensionCount; ++d) {
@@ -62,13 +62,13 @@ namespace storm {
             }
 
             typename EpochManager::Epoch EpochManager::getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(!hasBottomDimension(step), "The given step has at least one bottom dimension.");
 
                 // Start with dimension zero
                 uint64_t mask = dimensionBitMask;
                 uint64_t e_d = epoch & mask;
                 uint64_t s_d = step & mask;
-                assert(s_d != mask);
                 uint64_t result = (e_d < s_d || e_d == mask) ? mask : e_d - s_d;
                 
                 // Consider the remaining dimensions
@@ -76,39 +76,72 @@ namespace storm {
                     mask = mask << bitsPerDimension;
                     e_d = epoch & mask;
                     s_d = step & mask;
-                    assert(s_d != mask);
                     result |= ((e_d < s_d || e_d == mask) ? mask : e_d - s_d);
                 }
                 return result;
             }
             
             std::vector<typename EpochManager::Epoch> EpochManager::getPredecessorEpochs(Epoch const& epoch, Epoch const& step) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
-            
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(!hasBottomDimension(step), "The given step has at least one bottom dimension.");
+                std::set<Epoch> resultAsSet;
+                gatherPredecessorEpochs(resultAsSet, epoch, step);
+                return std::vector<Epoch>(resultAsSet.begin(), resultAsSet.end());
             }
             
             void EpochManager::gatherPredecessorEpochs(std::set<Epoch>& gatheredPredecessorEpochs, Epoch const& epoch, Epoch const& step) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(!hasBottomDimension(step), "The given step has at least one bottom dimension.");
+                Epoch currStep = step;
+                uint64_t d = 0;
+                while (d < dimensionCount) {
+                    Epoch predecessor = epoch;
+                    for (uint64_t dPrime = 0; dPrime < dimensionCount; ++dPrime) {
+                        uint64_t step_dPrime = getDimensionOfEpoch(currStep, dPrime);
+                        if (isBottomDimension(predecessor, dPrime)) {
+                            if (step_dPrime != 0) {
+                                setDimensionOfEpoch(predecessor, dPrime, step_dPrime - 1);
+                            }
+                        } else {
+                            setDimensionOfEpoch(predecessor, dPrime, getDimensionOfEpoch(predecessor, dPrime) + step_dPrime);
+                        }
+                    }
+                    assert(epoch == getSuccessorEpoch(predecessor, step));
+                    gatheredPredecessorEpochs.insert(predecessor);
                     
+                    do {
+                        if (isBottomDimension(epoch, d)) {
+                            uint64_t step_d = getDimensionOfEpoch(currStep, d);
+                            if (step_d == 0) {
+                                setDimensionOfEpoch(currStep, d, getDimensionOfEpoch(step, d));
+                            } else {
+                                setDimensionOfEpoch(currStep, d, step_d - 1);
+                                d = 0;
+                                break;
+                            }
+                        }
+                        ++d;
+                    } while(d < dimensionCount);
+                }
             }
             
             bool EpochManager::isValidDimensionValue(uint64_t const& value) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 return ((value & dimensionBitMask) == value) && value != dimensionBitMask;
             }
             
             bool EpochManager::isZeroEpoch(Epoch const& epoch) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 return (epoch & relevantBitsMask) == 0;
             }
             
             bool EpochManager::isBottomEpoch(Epoch const& epoch) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 return (epoch & relevantBitsMask) == relevantBitsMask;
             }
             
             bool EpochManager::hasBottomDimension(Epoch const& epoch) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 uint64_t mask = dimensionBitMask;
                 for (uint64_t d  = 0; d < dimensionCount; ++d) {
                     if ((epoch | mask) == epoch) {
@@ -120,29 +153,29 @@ namespace storm {
             }
 
             void EpochManager::setBottomDimension(Epoch& epoch, uint64_t const& dimension) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 epoch |= (dimensionBitMask << (dimension * bitsPerDimension));
             }
             
             void EpochManager::setDimensionOfEpoch(Epoch& epoch, uint64_t const& dimension, uint64_t const& value) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 STORM_LOG_ASSERT(isValidDimensionValue(value), "The dimension value " << value << " is too high.");
                 epoch &= ~(dimensionBitMask << (dimension * bitsPerDimension));
                 epoch |= (value << (dimension * bitsPerDimension));
             }
             
             bool EpochManager::isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 return (epoch | (dimensionBitMask << (dimension * bitsPerDimension))) == epoch;
             }
             
             uint64_t EpochManager::getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 return (epoch >> (dimension * bitsPerDimension)) & dimensionBitMask;
             }
             
             std::string EpochManager::toString(Epoch const& epoch) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 std::string res = "<" + (isBottomDimension(epoch, 0) ? "_" : std::to_string(getDimensionOfEpoch(epoch, 0)));
                 for (uint64_t d = 1; d < dimensionCount; ++d) {
                     res += ", ";
@@ -153,7 +186,7 @@ namespace storm {
             }
             
             bool EpochManager::epochClassZigZagOrder(Epoch const& epoch1, Epoch const& epoch2) const {
-                STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
                 
                 // Return true iff epoch 1 has to be computed before epoch 2
                 

src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp

@@ -389,7 +389,6 @@ namespace storm {
                 swAux4.start();
                 epochModel.epochMatrix = std::move(ecElimResult.matrix);
                 epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping);
-                productToEpochModelStateMap = std::move(ecElimResult.oldToNewStateMapping);
                 
                 epochModel.stepChoices = storm::storage::BitVector(epochModel.epochMatrix.getRowCount(), false);
                 for (uint64_t choice = 0; choice < epochModel.epochMatrix.getRowCount(); ++choice) {
@@ -410,14 +409,17 @@ namespace storm {
                 
                 epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false);
                 for (auto const& productState : productInStates) {
-                    STORM_LOG_ASSERT(productToEpochModelStateMap[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model.");
-                    epochModel.epochInStates.set(productToEpochModelStateMap[productState], true);
+                    STORM_LOG_ASSERT(ecElimResult.oldToNewStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model.");
+                    epochModel.epochInStates.set(ecElimResult.oldToNewStateMapping[productState], true);
                 }
                 
                 epochModelInStateToProductStatesMap.assign(epochModel.epochInStates.getNumberOfSetBits(), std::vector<uint64_t>());
+                std::vector<uint64_t> toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits<uint64_t>::max());
                 for (auto const& productState : productInStates) {
-                    epochModelInStateToProductStatesMap[epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(productToEpochModelStateMap[productState])].push_back(productState);
+                    toEpochModelInStatesMap[productState] = epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(ecElimResult.oldToNewStateMapping[productState]);
+                    epochModelInStateToProductStatesMap[epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(ecElimResult.oldToNewStateMapping[productState])].push_back(productState);
                 }
+                productStateToEpochModelInStateMap = std::make_shared<std::vector<uint64_t> const>(std::move(toEpochModelInStatesMap));
                 
                 swAux4.stop();
                 swSetEpochClass.stop();
@@ -478,49 +480,47 @@ namespace storm {
             }
             
             template<typename ValueType, bool SingleObjectiveMode>
-            void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch(std::vector<SolutionType>& inStateSolutions) {
+            void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch(std::vector<SolutionType>&& inStateSolutions) {
                 swInsertSol.start();
+                STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before.");
                 STORM_LOG_ASSERT(inStateSolutions.size() == epochModelInStateToProductStatesMap.size(), "Invalid number of solutions.");
-                auto solIt = inStateSolutions.begin();
-                for (auto const& productStates : epochModelInStateToProductStatesMap) {
-                    assert(!productStates.empty());
-                    auto productStateIt = productStates.begin();
-                    // Skip the first product state for now. It's result will be std::move'd afterwards.
-                    for (++productStateIt; productStateIt != productStates.end(); ++productStateIt) {
-                        setSolutionForCurrentEpoch(*productStateIt, *solIt);
-                    }
-                    setSolutionForCurrentEpoch(productStates.front(), std::move(*solIt));
 
-                    ++solIt;
+                std::set<Epoch> predecessorEpochs, successorEpochs;
+                for (auto const& step : possibleEpochSteps) {
+                    epochManager.gatherPredecessorEpochs(predecessorEpochs, currentEpoch.get(), step);
+                    successorEpochs.insert(epochManager.getSuccessorEpoch(currentEpoch.get(), step));
                 }
-                maxSolutionsStored = std::max((uint64_t) solutions.size(), maxSolutionsStored);
+                predecessorEpochs.erase(currentEpoch.get());
+                successorEpochs.erase(currentEpoch.get());
+                STORM_LOG_ASSERT(!predecessorEpochs.empty(), "There are no predecessors for the epoch " << epochManager.toString(currentEpoch.get()));
                 
-                swInsertSol.stop();
+                // clean up solutions that are not needed anymore
+                for (auto const& successorEpoch : successorEpochs) {
+                    auto successorEpochSolutionIt = epochSolutions.find(successorEpoch);
+                    STORM_LOG_ASSERT(successorEpochSolutionIt != epochSolutions.end(), "Solution for successor epoch does not exist (anymore).");
+                    --successorEpochSolutionIt->second.count;
+                    if (successorEpochSolutionIt->second.count == 0) {
+                        epochSolutions.erase(successorEpochSolutionIt);
                     }
-            
-            template<typename ValueType, bool SingleObjectiveMode>
-            void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution) {
-                STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before.");
-            //    std::cout << "Setting solution for state " << productState << " in epoch " << epochManager.toString(currentEpoch.get()) << std::endl;
-                solutions[std::make_pair(currentEpoch.get(), productState)] = solution;
                 }
                 
-            template<typename ValueType, bool SingleObjectiveMode>
-            void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType&& solution) {
-                STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before.");
-   //             std::cout << "Setting solution for state " << productState << " in epoch " << epochManager.toString(currentEpoch.get()) << std::endl;
-                solutions[std::make_pair(currentEpoch.get(), productState)] = std::move(solution);
+                // add the new solution
+                EpochSolution solution;
+                solution.count = predecessorEpochs.size();
+                solution.productStateToSolutionVectorMap = productStateToEpochModelInStateMap;
+                solution.solutions = std::move(inStateSolutions);
+                epochSolutions[currentEpoch.get()] = std::move(solution);
+                
+                maxSolutionsStored = std::max((uint64_t) epochSolutions.size(), maxSolutionsStored);
+                swInsertSol.stop();
+                
             }
             
             template<typename ValueType, bool SingleObjectiveMode>
             typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(Epoch const& epoch, uint64_t const& productState) {
-                swFindSol.start();
-                //std::cout << "Getting solution for epoch " << epochManager.toString(epoch) << " and state " << productState  << std::endl;
-                auto solutionIt = solutions.find(std::make_pair(epoch, productState));
-                STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
-                //std::cout << "Retrieved solution for state " << productState << " in epoch " << epochManager.toString(epoch)  << std::endl;
-                swFindSol.stop();
-                return solutionIt->second;
+                STORM_LOG_ASSERT(epochSolutions.find(epoch) != epochSolutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
+                EpochSolution const& epochSolution = epochSolutions[epoch];
+                return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]];
             }
             
             template<typename ValueType, bool SingleObjectiveMode>

src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

@@ -73,7 +73,7 @@ namespace storm {
                 
                 EpochModel& setCurrentEpoch(Epoch const& epoch);
                 
-                void setSolutionForCurrentEpoch(std::vector<SolutionType>& inStateSolutions);
+                void setSolutionForCurrentEpoch(std::vector<SolutionType>&& inStateSolutions);
                 SolutionType const& getInitialStateResult(Epoch const& epoch); // Assumes that the initial state is unique
                 SolutionType const& getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex);
                 
@@ -104,8 +104,6 @@ namespace storm {
                 template<bool SO = SingleObjectiveMode, typename std::enable_if<!SO, int>::type = 0>
                 std::string solutionToString(SolutionType const& solution) const;
                 
-                void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution);
-                void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType&& solution);
                 SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState);
                 
                 storm::models::sparse::Mdp<ValueType> const& model;
@@ -114,7 +112,7 @@ namespace storm {
                 std::unique_ptr<ProductModel<ValueType>> productModel;
                 
                 std::vector<uint64_t> epochModelToProductChoiceMap;
-                std::vector<uint64_t> productToEpochModelStateMap;
+                std::shared_ptr<std::vector<uint64_t> const> productStateToEpochModelInStateMap;
                 std::vector<std::vector<uint64_t>> epochModelInStateToProductStatesMap;
                 std::set<Epoch> possibleEpochSteps;
                 
@@ -129,7 +127,12 @@ namespace storm {
                 std::vector<ValueType> scalingFactors;
                 
                 
-                std::map<std::pair<Epoch, uint64_t>, SolutionType> solutions;
+                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;

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -77,7 +77,7 @@ namespace storm {
                 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
                 
                 // initialize data that will be needed for each epoch
-                std::vector<ValueType> x, b, epochResult;
+                std::vector<ValueType> x, b;
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
                 for (auto const& epoch : epochOrder) {
                     // Update some data for the case that the Matrix has changed
@@ -108,9 +108,7 @@ namespace storm {
                     minMaxSolver->solveEquations(x, b);
                     
                     // Plug in the result into the reward unfolding
-                    epochResult.resize(epochModel.epochInStates.getNumberOfSetBits());
-                    storm::utility::vector::selectVectorValues(epochResult, epochModel.epochInStates, x);
-                    rewardUnfolding.setSolutionForCurrentEpoch(epochResult);
+                    rewardUnfolding.setSolutionForCurrentEpoch(storm::utility::vector::filterVector(x, epochModel.epochInStates));
                 }
                 
                 std::map<storm::storage::sparse::state_type, ValueType> result;