From 11a4f8d01676293bbf382647d668a3d9df7ffc89 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 5 Sep 2017 11:30:46 +0200 Subject: [PATCH] restructured initialization of modelmemory product --- .../MultiDimensionalRewardUnfolding.cpp | 108 +++++++++--------- .../MultiDimensionalRewardUnfolding.h | 7 +- 2 files changed, 62 insertions(+), 53 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index effb240bf..479286ad2 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -113,48 +113,16 @@ namespace storm { template void MultiDimensionalRewardUnfolding::initializeMemoryProduct(std::vector> const& epochSteps) { - // build the model x memory product + // build the memory structure auto memoryStructure = computeMemoryStructure(); - storm::storage::SparseModelMemoryProduct productBuilder(memoryStructure.product(model)); - - storm::storage::BitVector memoryState(subObjectives.size(), false); - uint64_t memoryStateAsInt = memoryStructure.getNumberOfStates(); - do { - --memoryStateAsInt; - storm::storage::BitVector stepChoices(model.getNumberOfChoices(), false); - for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - auto const& subObjectives = objectiveDimensions[objIndex]; - if (subObjectives.isDisjointFrom(memoryState)) { - for (auto const& subObj : subObjectives) { - stepChoices |= storm::utility::vector::filterGreaterZero(epochSteps[subObj]); - } - } - } - - storm::storage::BitVector stepChoiceSuccessors(model.getNumberOfStates(), false); - for (auto const& choice : stepChoices) { - for (auto const& successor : model.getTransitionMatrix().getRow(choice)) { - stepChoiceSuccessors.set(successor.getColumn(), true); - } - } - - for (auto const& modelState : stepChoiceSuccessors) { - productBuilder.addReachableState(modelState, memoryStateAsInt); - } - - memoryState.increment(); - } while (!memoryState.empty()); - assert(memoryStateAsInt == 0); - - - - - - memoryProduct = MemoryProduct(productBuilder, epochSteps, memoryLabels); + // build a mapping between the different representations of memory states + auto memoryStateMap = computeMemoryStateMap(memoryStructure); + + memoryProduct = MemoryProduct(model, memoryStructure, std::move(memoryStateMap), epochSteps, objectiveDimensions); } - + template typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getStartEpoch() { Epoch startEpoch; @@ -480,7 +448,29 @@ namespace storm { } template - MultiDimensionalRewardUnfolding::MemoryProduct::MemoryProduct(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector> const& originalModelSteps, std::vector> const& memoryLabels) { + std::vector MultiDimensionalRewardUnfolding::computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const { + // Compute a mapping between the different representations of memory states + std::vector result; + result.reserve(memory.getNumberOfStates()); + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + storm::storage::BitVector relevantSubObjectives(memoryLabels.size(), false); + std::set stateLabels = memory.getStateLabeling().getLabelsOfState(memState); + for (uint64_t dim = 0; dim < memoryLabels.size(); ++dim) { + if (memoryLabels[dim] && stateLabels.find(memoryLabels[dim].get()) != stateLabels.end()) { + relevantSubObjectives.set(dim, true); + } + } + result.push_back(std::move(relevantSubObjectives)); + } + return result; + } + + template + MultiDimensionalRewardUnfolding::MemoryProduct::MemoryProduct(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector&& memoryStateMap, std::vector> const& originalModelSteps, std::vector const& objectiveDimensions) : memoryStateMap(std::move(memoryStateMap)) { + + storm::storage::SparseModelMemoryProduct productBuilder(memory.product(model)); + + setReachableStates(productBuilder, originalModelSteps, objectiveDimensions); product = productBuilder.build()->template as>(); @@ -512,18 +502,6 @@ namespace storm { } } - // Compute a mapping between the different representations of memory states - for (uint64_t memState = 0; memState < numMemoryStates; ++memState) { - storm::storage::BitVector relevantSubObjectives(memoryLabels.size(), false); - std::set stateLabels = productBuilder.getMemory().getStateLabeling().getLabelsOfState(memState); - for (uint64_t dim = 0; dim < memoryLabels.size(); ++dim) { - if (memoryLabels[dim] && stateLabels.find(memoryLabels[dim].get()) != stateLabels.end()) { - relevantSubObjectives.set(dim, true); - } - } - memoryStateMap.push_back(std::move(relevantSubObjectives)); - } - // Compute the epoch steps for the product steps.resize(getProduct().getNumberOfChoices()); for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { @@ -550,6 +528,32 @@ namespace storm { } } + template + void MultiDimensionalRewardUnfolding::MemoryProduct::setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector> const& originalModelSteps, std::vector const& objectiveDimensions) const { + for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { + auto const& memStateBv = memoryStateMap[memState]; + storm::storage::BitVector stepChoices(productBuilder.getOriginalModel().getTransitionMatrix().getRowCount(), false); + for (auto const& subObjectives : objectiveDimensions) { + if (subObjectives.isDisjointFrom(memStateBv)) { + for (auto const& subObj : subObjectives) { + stepChoices |= storm::utility::vector::filterGreaterZero(originalModelSteps[subObj]); + } + } + } + + storm::storage::BitVector stepChoiceSuccessors(productBuilder.getOriginalModel().getNumberOfStates(), false); + for (auto const& choice : stepChoices) { + for (auto const& successor : productBuilder.getOriginalModel().getTransitionMatrix().getRow(choice)) { + stepChoiceSuccessors.set(successor.getColumn(), true); + } + } + + for (auto const& modelState : stepChoiceSuccessors) { + productBuilder.addReachableState(modelState, memState); + } + } + } + template storm::models::sparse::Mdp const& MultiDimensionalRewardUnfolding::MemoryProduct::getProduct() const { return *product; @@ -689,7 +693,7 @@ namespace storm { return objectiveRewards; } - + template typename MultiDimensionalRewardUnfolding::EpochClass MultiDimensionalRewardUnfolding::getClassOfEpoch(Epoch const& epoch) const { // Get a BitVector that is 1 wherever the epoch is non-negative diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index e66dff69d..5215d1595 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -79,7 +79,7 @@ namespace storm { class MemoryProduct { public: MemoryProduct() = default; - MemoryProduct(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector> const& originalModelSteps, std::vector> const& memoryLabels); + MemoryProduct(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector&& memoryStateMap, std::vector> const& originalModelSteps, std::vector const& objectiveDimensions); storm::models::sparse::Mdp const& getProduct() const; std::vector> const& getSteps() const; @@ -95,6 +95,10 @@ namespace storm { uint64_t getProductStateFromChoice(uint64_t const& productChoice) const; private: + + void setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector> const& originalModelSteps, std::vector const& objectiveDimensions) const; + + std::shared_ptr> product; std::vector> steps; @@ -115,6 +119,7 @@ namespace storm { void initializeMemoryProduct(std::vector> const& epochSteps); storm::storage::MemoryStructure computeMemoryStructure() const; + std::vector computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; std::vector> computeObjectiveRewardsForProduct(Epoch const& epoch) const;