From 9039323fa9708c5b01530c2376def309bd664b7c Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Sep 2017 09:06:20 +0200 Subject: [PATCH] optimized setting the epoch class --- .../MultiDimensionalRewardUnfolding.cpp | 21 +++++++++---------- .../MultiDimensionalRewardUnfolding.h | 1 - 2 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index e1e06a99b..5db3147c2 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -368,7 +368,6 @@ namespace storm { EpochClass epochClass = epochManager.getEpochClass(epoch); // std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << std::endl; swSetEpochClass.start(); - swAux1.start(); auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives); storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false); @@ -413,11 +412,7 @@ namespace storm { // We assume that there is no end component in which objective reward is earned STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix, epochModel.epochMatrix.transpose(true), allProductStates, ~zeroObjRewardChoices & ~stepChoices), "There is a scheduler that yields infinite reward for one objective. This case should be excluded"); - swAux1.stop(); - swAux2.start(); auto ecElimResult = storm::transformer::EndComponentEliminator::transform(epochModel.epochMatrix, consideredStates, zeroObjRewardChoices & ~stepChoices, consideredStates); - swAux2.stop(); - swAux3.start(); epochModel.epochMatrix = std::move(ecElimResult.matrix); epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping); @@ -442,28 +437,32 @@ namespace storm { } epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } - swAux3.stop(); - swAux4.start(); + swAux4.start(); + swAux1.start(); epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); for (auto const& productState : productInStates) { 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); } + swAux1.stop(); - epochModelInStateToProductStatesMap.assign(epochModel.epochInStates.getNumberOfSetBits(), std::vector()); + swAux2.start(); std::vector toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits::max()); + std::vector epochModelStateToInStateMap = epochModel.epochInStates.getNumberOfSetBitsBeforeIndices(); for (auto const& productState : productInStates) { - toEpochModelInStatesMap[productState] = epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(ecElimResult.oldToNewStateMapping[productState]); - epochModelInStateToProductStatesMap[epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(ecElimResult.oldToNewStateMapping[productState])].push_back(productState); + toEpochModelInStatesMap[productState] = epochModelStateToInStateMap[ecElimResult.oldToNewStateMapping[productState]]; } productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); + swAux2.stop(); + swAux3.start(); epochModel.objectiveRewardFilter.clear(); for (auto const& objRewards : epochModel.objectiveRewards) { epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards)); epochModel.objectiveRewardFilter.back().complement(); } + swAux3.stop(); swAux4.stop(); swSetEpochClass.stop(); @@ -530,7 +529,7 @@ namespace storm { void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector&& 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."); + STORM_LOG_ASSERT(inStateSolutions.size() == epochModel.epochInStates.getNumberOfSetBits(), "Invalid number of solutions."); std::set predecessorEpochs, successorEpochs; for (auto const& step : possibleEpochSteps) { diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index a8f06178e..f9476c340 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -115,7 +115,6 @@ namespace storm { std::vector epochModelToProductChoiceMap; std::shared_ptr const> productStateToEpochModelInStateMap; - std::vector> epochModelInStateToProductStatesMap; std::set possibleEpochSteps; EpochModel epochModel;