diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 49223642d..e42fa24a9 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -188,36 +188,37 @@ namespace storm { } swSetEpoch.start(); - // Find out which objective rewards are earned in this particular epoch epochModel.objectiveRewardFilter = std::vector(objectives.size(), storm::storage::BitVector(epochModel.objectiveRewards.front().size(), true)); + epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); + auto stepSolIt = epochModel.stepSolutions.begin(); for (auto const& reducedChoice : epochModel.stepChoices) { uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice]; - storm::storage::BitVector memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(memoryProduct.getProductStateFromChoice(productChoice))); + uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice); + auto memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState)); Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get()); + + // Find out whether objective reward is earned for the current choice + swAux1.start(); for (uint64_t dim = 0; dim < successorEpoch.size(); ++dim) { if (successorEpoch[dim] < 0 && memoryState.get(dim)) { epochModel.objectiveRewardFilter[subObjectives[dim].second].set(reducedChoice, false); } } - } - - swAux.start(); - // compute the solution for the stepChoices - epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); - auto stepSolIt = epochModel.stepSolutions.begin(); - for (auto const& reducedChoice : epochModel.stepChoices) { - uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice]; - uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice); - auto relevantDimensions = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState)); - Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get()); + swAux1.stop(); + + // compute the solution for the stepChoices + swAux2.start(); SolutionType choiceSolution = getZeroSolution(); if (getClassOfEpoch(epoch) == getClassOfEpoch(successorEpoch)) { + swAux3.start(); for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) { addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); } + swAux3.stop(); } else { + swAux4.start(); storm::storage::BitVector successorRelevantDimensions(successorEpoch.size(), true); - for (auto const& dim : relevantDimensions) { + for (auto const& dim : memoryState) { if (successorEpoch[dim] < 0) { successorRelevantDimensions &= ~objectiveDimensions[subObjectives[dim].second]; } @@ -228,11 +229,12 @@ namespace storm { SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); addScaledSolution(choiceSolution, successorSolution, successor.getValue()); } + swAux4.stop(); } + swAux2.stop(); *stepSolIt = std::move(choiceSolution); ++stepSolIt; } - swAux.stop(); assert(epochModel.objectiveRewards.size() == objectives.size()); assert(epochModel.objectiveRewardFilter.size() == objectives.size()); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 1932338d7..33297feab 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -59,7 +59,10 @@ namespace storm { std::cout << " setEpochClass: " << swSetEpochClass << " seconds." << std::endl; std::cout << " findSolutions: " << swFindSol << " seconds." << std::endl; std::cout << " insertSolutions: " << swInsertSol << " seconds." << std::endl; - std::cout << " auxStopWatch: " << swAux << " seconds." << std::endl; + std::cout << " aux1StopWatch: " << swAux1 << " seconds." << std::endl; + std::cout << " aux2StopWatch: " << swAux2 << " seconds." << std::endl; + std::cout << " aux3StopWatch: " << swAux3 << " seconds." << std::endl; + std::cout << " aux4StopWatch: " << swAux4 << " seconds." << std::endl; std::cout << "---------------------------------------------" << std::endl; std::cout << " Product size: " << memoryProduct.getProduct().getNumberOfStates() << std::endl; std::cout << " Epoch model sizes: "; @@ -162,7 +165,7 @@ namespace storm { std::map, SolutionType> solutions; - storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux; + storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4; std::vector epochModelSizes; }; }