From cf91a349703a2bb66ba211a03ada8d446d941545 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 7 Sep 2017 14:35:05 +0200 Subject: [PATCH] use cached memory for the epoch results --- ...dpRewardBoundedPcaaWeightVectorChecker.cpp | 22 +++++++++---------- .../MultiDimensionalRewardUnfolding.cpp | 12 +++++----- .../MultiDimensionalRewardUnfolding.h | 8 ++++--- 3 files changed, 22 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 89065d57b..b898262b6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -46,10 +46,11 @@ namespace storm { template void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector) { - auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch); + auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch); swEqBuilding.start(); - std::vector::SolutionType> result(epochModel.inStates.getNumberOfSetBits()); - + uint64_t stateSolutionSize = this->objectives.size() + 1; + auto& result = epochModel.inStateSolutions; + result.resize(epochModel.epochInStates.getNumberOfSetBits(), typename MultiDimensionalRewardUnfolding::SolutionType(stateSolutionSize)); // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives std::vector b(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); @@ -81,10 +82,8 @@ namespace storm { swMinMaxSolving.stop(); swEqBuilding.start(); auto resultIt = result.begin(); - uint64_t solSize = this->objectives.size() + 1; - for (auto const& state : epochModel.inStates) { - resultIt->reserve(solSize); - resultIt->push_back(x[state]); + for (auto const& state : epochModel.epochInStates) { + resultIt->front() = x[state]; ++resultIt; } @@ -115,14 +114,15 @@ namespace storm { linEqSolver->solveEquations(x, b); swLinEqSolving.stop(); swEqBuilding.start(); - auto resultIt = result.begin(); - for (auto const& state : epochModel.inStates) { - resultIt->push_back(x[state]); + resultIt = result.begin(); + for (auto const& state : epochModel.epochInStates) { + (*resultIt)[objIndex + 1] = x[state]; ++resultIt; } } swEqBuilding.stop(); - rewardUnfolding.setSolutionForCurrentEpoch(result); + + rewardUnfolding.setSolutionForCurrentEpoch(); } template diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index e83cd02cc..d8bf245b6 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -182,7 +182,7 @@ namespace storm { } template - typename MultiDimensionalRewardUnfolding::EpochModel const& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { + typename MultiDimensionalRewardUnfolding::EpochModel& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { // Check if we need to update the current epoch class if (!currentEpoch || getClassOfEpoch(epoch) != getClassOfEpoch(currentEpoch.get())) { setCurrentEpochClass(epoch); @@ -334,9 +334,9 @@ namespace storm { epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } - epochModel.inStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); + epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); for (auto const& productState : productInStates) { - epochModel.inStates.set(ecElimResult.oldToNewStateMapping[productState], true); + epochModel.epochInStates.set(ecElimResult.oldToNewStateMapping[productState], true); } swSetEpochClass.stop(); @@ -443,12 +443,12 @@ namespace storm { } template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& inStateSolutions) { + void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch() { swInsertSol.start(); for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) { uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[productState]; - if (reducedModelState < epochModel.epochMatrix.getRowGroupCount() && epochModel.inStates.get(reducedModelState)) { - setSolutionForCurrentEpoch(productState, inStateSolutions[epochModel.inStates.getNumberOfSetBitsBeforeIndex(reducedModelState)]); + if (reducedModelState < epochModel.epochMatrix.getRowGroupCount() && epochModel.epochInStates.get(reducedModelState)) { + setSolutionForCurrentEpoch(productState, epochModel.inStateSolutions[epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(reducedModelState)]); } } swInsertSol.stop(); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index a591316c8..2a42c1dd6 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -33,7 +33,9 @@ namespace storm { std::vector stepSolutions; std::vector> objectiveRewards; std::vector objectiveRewardFilter; - storm::storage::BitVector inStates; + storm::storage::BitVector epochInStates; + + std::vector inStateSolutions; }; /* @@ -75,9 +77,9 @@ namespace storm { Epoch getStartEpoch(); std::vector getEpochComputationOrder(Epoch const& startEpoch); - EpochModel const& setCurrentEpoch(Epoch const& epoch); + EpochModel& setCurrentEpoch(Epoch const& epoch); - void setSolutionForCurrentEpoch(std::vector const& inStateSolutions); + void setSolutionForCurrentEpoch(); SolutionType const& getInitialStateResult(Epoch const& epoch);