From 27ee299f637fe6dc363ce9759b381c31e8194972 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 7 Sep 2017 14:49:33 +0200 Subject: [PATCH] more efficient comparison of epoch classes --- .../MultiDimensionalRewardUnfolding.cpp | 19 ++++++++----------- .../MultiDimensionalRewardUnfolding.h | 4 +--- 2 files changed, 9 insertions(+), 14 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index d8bf245b6..78d31ffe8 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -184,7 +184,7 @@ namespace storm { template 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())) { + if (!currentEpoch || !sameEpochClass(epoch, currentEpoch.get())) { setCurrentEpochClass(epoch); } @@ -211,7 +211,7 @@ namespace storm { swAux2.start(); SolutionType choiceSolution; bool firstSuccessor = true; - if (getClassOfEpoch(epoch) == getClassOfEpoch(successorEpoch)) { + if (sameEpochClass(epoch, successorEpoch)) { swAux3.start(); for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) { if (firstSuccessor) { @@ -836,17 +836,14 @@ namespace storm { } template - typename MultiDimensionalRewardUnfolding::EpochClass MultiDimensionalRewardUnfolding::getClassOfEpoch(Epoch const& epoch) const { - // Get a BitVector that is 1 wherever the epoch is non-negative - storm::storage::BitVector classAsBitVector(epoch.size(), false); - uint64_t i = 0; - for (auto const& e : epoch) { - if (e >= 0) { - classAsBitVector.set(i, true); + bool MultiDimensionalRewardUnfolding::sameEpochClass(Epoch const& epoch1, Epoch const& epoch2) const { + assert(epoch1.size() == epoch2.size()); + for (auto e1It = epoch1.begin(), e2It = epoch2.begin(); e1It != epoch1.end(); ++e1It, ++e2It) { + if ((*e1It) < 0 != (*e2It < 0)) { + return false; } - ++i; } - return classAsBitVector.getAsInt(0, epoch.size()); + return true; } template diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 2a42c1dd6..ea70fb781 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -23,7 +23,6 @@ namespace storm { public: typedef std::vector Epoch; // The number of reward steps that are "left" for each dimension - typedef uint64_t EpochClass; // Collection of epochs that consider the same epoch model typedef typename std::conditional>::type SolutionType; @@ -132,8 +131,7 @@ namespace storm { std::vector computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; std::vector> computeObjectiveRewardsForProduct(Epoch const& epoch) const; - - EpochClass getClassOfEpoch(Epoch const& epoch) const; + bool sameEpochClass(Epoch const& epoch1, Epoch const& epoch2) const; Epoch getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const;