From 3044aaa3f5160ed31cc5692b6dab2bea90ac04ea Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 13 Sep 2017 12:17:16 +0200 Subject: [PATCH] The product model is now handled in a separate class --- .../MultiDimensionalRewardUnfolding.cpp | 417 +----------------- .../MultiDimensionalRewardUnfolding.h | 51 +-- .../rewardbounded/ProductModel.cpp | 388 ++++++++++++++++ .../rewardbounded/ProductModel.h | 64 +++ 4 files changed, 476 insertions(+), 444 deletions(-) create mode 100644 src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp create mode 100644 src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index d695f86cf..413444142 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -6,9 +6,7 @@ #include "storm/utility/macros.h" #include "storm/logic/Formulas.h" -#include "storm/logic/CloneVisitor.h" #include "storm/storage/memorystructure/MemoryStructureBuilder.h" -#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -148,7 +146,7 @@ namespace storm { // build a mapping between the different representations of memory states auto memoryStateMap = computeMemoryStateMap(memoryStructure); - memoryProduct = MemoryProduct(model, memoryStructure, std::move(memoryStateMap), epochSteps, objectiveDimensions); + productModel = std::make_unique>(model, memoryStructure, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps); } @@ -272,9 +270,9 @@ namespace storm { auto stepSolIt = epochModel.stepSolutions.begin(); for (auto const& reducedChoice : epochModel.stepChoices) { uint64_t productChoice = epochModelToProductChoiceMap[reducedChoice]; - uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice); - auto memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState)); - Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice]); + uint64_t productState = productModel->getProductStateFromChoice(productChoice); + auto memoryState = productModel->convertMemoryState(productModel->getMemoryState(productState)); + Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, productModel->getSteps()[productChoice]); // Find out whether objective reward is earned for the current choice // Objective reward is not earned if there is a subObjective that is still relevant but the corresponding reward bound is passed after taking the choice @@ -293,7 +291,7 @@ namespace storm { SolutionType choiceSolution; bool firstSuccessor = true; if (epochManager.compareEpochClass(epoch, successorEpoch)) { - for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) { + for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { if (firstSuccessor) { choiceSolution = getScaledSolution(getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); firstSuccessor = false; @@ -308,9 +306,9 @@ namespace storm { successorRelevantDimensions &= ~objectiveDimensions[subObjectives[dim].second]; } } - for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) { - storm::storage::BitVector successorMemoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(successor.getColumn())) & successorRelevantDimensions; - uint64_t successorProductState = memoryProduct.getProductState(memoryProduct.getModelState(successor.getColumn()), memoryProduct.convertMemoryState(successorMemoryState)); + for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { + storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & successorRelevantDimensions; + uint64_t successorProductState = productModel->getProductState(productModel->getModelState(successor.getColumn()), productModel->convertMemoryState(successorMemoryState)); SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); if (firstSuccessor) { choiceSolution = getScaledSolution(successorSolution, successor.getValue()); @@ -355,28 +353,28 @@ namespace storm { // std::cout << "Setting epoch class for epoch " << storm::utility::vector::toString(epoch) << std::endl; swSetEpochClass.start(); swAux1.start(); - auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch); + auto productObjectiveRewards = productModel->computeObjectiveRewards(epoch, objectives, subObjectives, memoryLabels); - storm::storage::BitVector stepChoices(memoryProduct.getProduct().getNumberOfChoices(), false); + storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false); uint64_t choice = 0; - for (auto const& step : memoryProduct.getSteps()) { + for (auto const& step : productModel->getSteps()) { if (!epochManager.isZeroEpoch(step) && epochManager.getSuccessorEpoch(epoch, step) != epoch) { stepChoices.set(choice, true); } ++choice; } - epochModel.epochMatrix = memoryProduct.getProduct().getTransitionMatrix().filterEntries(~stepChoices); + epochModel.epochMatrix = productModel->getProduct().getTransitionMatrix().filterEntries(~stepChoices); - storm::storage::BitVector zeroObjRewardChoices(memoryProduct.getProduct().getNumberOfChoices(), true); + storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getNumberOfChoices(), true); for (auto const& objRewards : productObjectiveRewards) { zeroObjRewardChoices &= storm::utility::vector::filterZero(objRewards); } swAux1.stop(); swAux2.start(); - storm::storage::BitVector allProductStates(memoryProduct.getProduct().getNumberOfStates(), true); + storm::storage::BitVector allProductStates(productModel->getProduct().getNumberOfStates(), true); // Get the relevant states for this epoch. These are all states - storm::storage::BitVector productInStates = computeProductInStatesForEpochClass(epoch); + storm::storage::BitVector productInStates = productModel->computeInStates(epoch); // The epoch model only needs to consider the states that are reachable from a relevant state storm::storage::BitVector consideredStates = storm::utility::graph::getReachableStates(epochModel.epochMatrix, productInStates, allProductStates, ~allProductStates); // std::cout << "numInStates = " << productInStates.getNumberOfSetBits() << std::endl; @@ -426,114 +424,7 @@ namespace storm { epochModelSizes.push_back(epochModel.epochMatrix.getRowGroupCount()); } - template - storm::storage::BitVector MultiDimensionalRewardUnfolding::computeProductInStatesForEpochClass(Epoch const& epoch) { - storm::storage::SparseMatrix const& productMatrix = memoryProduct.getProduct().getTransitionMatrix(); - - // Initialize the result. Initial states are only considered if the epoch contains no bottom dimension. - storm::storage::BitVector result; - if (epochManager.hasBottomDimension(epoch)) { - result = storm::storage::BitVector(memoryProduct.getProduct().getNumberOfStates()); - } else { - result = memoryProduct.getProduct().getInitialStates(); - } - - // Compute the set of objectives that can not be satisfied anymore in the current epoch - storm::storage::BitVector irrelevantObjectives(objectives.size(), false); - for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - bool objIrrelevant = true; - for (auto const& dim : objectiveDimensions[objIndex]) { - if (!epochManager.isBottomDimension(epoch, dim)) { - objIrrelevant = false; - } - } - if (objIrrelevant) { - irrelevantObjectives.set(objIndex, true); - } - } - - // Perform DFS - storm::storage::BitVector reachableStates = memoryProduct.getProduct().getInitialStates(); - std::vector stack(reachableStates.begin(), reachableStates.end()); - - while (!stack.empty()) { - uint64_t state = stack.back(); - stack.pop_back(); - for (uint64_t choice = productMatrix.getRowGroupIndices()[state]; choice < productMatrix.getRowGroupIndices()[state + 1]; ++choice) { - auto const& choiceStep = memoryProduct.getSteps()[choice]; - if (!epochManager.isZeroEpoch(choiceStep)) { - // Compute the set of objectives that might or might not become irrelevant when the epoch is reached via the current choice - storm::storage::BitVector maybeIrrelevantObjectives(objectives.size(), false); - for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { - if (epochManager.isBottomDimension(epoch, dim) && epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { - maybeIrrelevantObjectives.set(subObjectives[dim].second); - } - } - maybeIrrelevantObjectives &= ~irrelevantObjectives; - - // For optimization purposes, we treat the case that all objectives will be relevant seperately - if (maybeIrrelevantObjectives.empty() && irrelevantObjectives.empty()) { - for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { - result.set(choiceSuccessor.getColumn(), true); - if (!reachableStates.get(choiceSuccessor.getColumn())) { - reachableStates.set(choiceSuccessor.getColumn()); - stack.push_back(choiceSuccessor.getColumn()); - } - } - } else { - // Enumerate all possible combinations of maybe relevant objectives - storm::storage::BitVector maybeObjSubset(maybeIrrelevantObjectives.getNumberOfSetBits(), false); - do { - for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { - // Compute the successor memory state for the current objective-subset and transition - storm::storage::BitVector successorMemoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(choiceSuccessor.getColumn())); - // Unselect dimensions belonging to irrelevant objectives - for (auto const& irrelevantObjIndex : irrelevantObjectives) { - successorMemoryState &= ~objectiveDimensions[irrelevantObjIndex]; - } - // Unselect objectives that are not in the current subset of maybe relevant objectives - // We can skip a subset if it selects an objective that is irrelevant anyway (according to the original successor memorystate). - bool skipThisSubSet = false; - uint64_t i = 0; - for (auto const& objIndex : maybeIrrelevantObjectives) { - if (maybeObjSubset.get(i)) { - if (successorMemoryState.isDisjointFrom(objectiveDimensions[objIndex])) { - skipThisSubSet = true; - break; - } else { - successorMemoryState &= ~objectiveDimensions[objIndex]; - } - } - ++i; - } - if (!skipThisSubSet) { - uint64_t successorState = memoryProduct.getProductState(memoryProduct.getModelState(choiceSuccessor.getColumn()), memoryProduct.convertMemoryState(successorMemoryState)); - result.set(successorState, true); - if (!reachableStates.get(successorState)) { - reachableStates.set(successorState); - stack.push_back(successorState); - } - } - } - - maybeObjSubset.increment(); - } while (!maybeObjSubset.empty()); - } - } else { - for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { - if (!reachableStates.get(choiceSuccessor.getColumn())) { - reachableStates.set(choiceSuccessor.getColumn()); - stack.push_back(choiceSuccessor.getColumn()); - } - } - } - } - } - - return result; - } - template template::type> typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { @@ -635,16 +526,16 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states."); - STORM_LOG_ASSERT(memoryProduct.getProduct().getInitialStates().getNumberOfSetBits() == 1, "The product has multiple initial states."); - return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin()); + STORM_LOG_ASSERT(productModel->getProduct().getInitialStates().getNumberOfSetBits() == 1, "The product has multiple initial states."); + return getStateSolution(epoch, *productModel->getProduct().getInitialStates().begin()); } template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex) { STORM_LOG_ASSERT(model.getInitialStates().get(initialStateIndex), "The given model state is not an initial state."); - for (uint64_t memState = 0; memState < memoryProduct.getNumberOfMemoryState(); ++memState) { - uint64_t productState = memoryProduct.getProductState(initialStateIndex, memState); - if (memoryProduct.getProduct().getInitialStates().get(productState)) { + for (uint64_t memState = 0; memState < productModel->getNumberOfMemoryState(); ++memState) { + uint64_t productState = productModel->getProductState(initialStateIndex, memState); + if (productModel->getProduct().getInitialStates().get(productState)) { return getStateSolution(epoch, productState); } } @@ -760,274 +651,6 @@ namespace storm { 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>(); - - uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); - uint64_t numMemoryStates = productBuilder.getMemory().getNumberOfStates(); - uint64_t numProductStates = getProduct().getNumberOfStates(); - - // Compute a mappings from product states to model/memory states and back - modelMemoryToProductStateMap.resize(numMemoryStates * numModelStates, std::numeric_limits::max()); - productToModelStateMap.resize(numProductStates, std::numeric_limits::max()); - productToMemoryStateMap.resize(numProductStates, std::numeric_limits::max()); - for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { - for (uint64_t memoryState = 0; memoryState < numMemoryStates; ++memoryState) { - if (productBuilder.isStateReachable(modelState, memoryState)) { - uint64_t productState = productBuilder.getResultState(modelState, memoryState); - modelMemoryToProductStateMap[modelState * numMemoryStates + memoryState] = productState; - productToModelStateMap[productState] = modelState; - productToMemoryStateMap[productState] = memoryState; - } - } - } - - // Map choice indices of the product to the state where it origins - choiceToStateMap.reserve(getProduct().getNumberOfChoices()); - for (uint64_t productState = 0; productState < numProductStates; ++productState) { - uint64_t groupSize = getProduct().getTransitionMatrix().getRowGroupSize(productState); - for (uint64_t i = 0; i < groupSize; ++i) { - choiceToStateMap.push_back(productState); - } - } - - // Compute the epoch steps for the product - steps.resize(getProduct().getNumberOfChoices(), 0); - for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { - uint64_t numChoices = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupSize(modelState); - uint64_t firstChoice = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupIndices()[modelState]; - for (uint64_t choiceOffset = 0; choiceOffset < numChoices; ++choiceOffset) { - Epoch const& step = originalModelSteps[firstChoice + choiceOffset]; - if (step != 0) { - for (uint64_t memState = 0; memState < numMemoryStates; ++memState) { - if (productStateExists(modelState, memState)) { - uint64_t productState = getProductState(modelState, memState); - uint64_t productChoice = getProduct().getTransitionMatrix().getRowGroupIndices()[productState] + choiceOffset; - assert(productChoice < getProduct().getTransitionMatrix().getRowGroupIndices()[productState + 1]); - steps[productChoice] = step; - } - } - } - } - } - } - - template - void MultiDimensionalRewardUnfolding::MemoryProduct::setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps, std::vector const& objectiveDimensions) const { - - // todo: find something else to perform getDimensionOfEpoch at this point - uint64_t dimensionCount = objectiveDimensions.front().size(); - uint64_t bitsPerDimension = 64 / dimensionCount; - uint64_t dimensionBitMask; - if (dimensionCount == 1) { - dimensionBitMask = -1ull; - } else { - dimensionBitMask = (1ull << bitsPerDimension) - 1; - } - - - - - - std::vector additionalReachableStates(memoryStateMap.size(), storm::storage::BitVector(productBuilder.getOriginalModel().getNumberOfStates(), false)); - for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { - auto const& memStateBv = memoryStateMap[memState]; - storm::storage::BitVector consideredObjectives(objectiveDimensions.size(), false); - do { - storm::storage::BitVector memStatePrimeBv = memStateBv; - for (auto const& objIndex : consideredObjectives) { - memStatePrimeBv &= ~objectiveDimensions[objIndex]; - } - if (memStatePrimeBv != memStateBv) { - for (uint64_t choice = 0; choice < productBuilder.getOriginalModel().getTransitionMatrix().getRowCount(); ++choice) { - bool consideredChoice = true; - for (auto const& objIndex : consideredObjectives) { - bool objectiveHasStep = false; - for (auto const& dim : objectiveDimensions[objIndex]) { - // TODO: this can not be called currently if (getDimensionOfEpoch(originalModelSteps[choice], dim) > 0) { - // .. instead we do this - if (((originalModelSteps[choice] >> (dim * bitsPerDimension)) & dimensionBitMask) > 0) { - objectiveHasStep = true; - break; - } - } - if (!objectiveHasStep) { - consideredChoice = false; - break; - } - } - if (consideredChoice) { - for (auto const& successor : productBuilder.getOriginalModel().getTransitionMatrix().getRow(choice)) { - if (productBuilder.isStateReachable(successor.getColumn(), memState)) { - additionalReachableStates[convertMemoryState(memStatePrimeBv)].set(successor.getColumn()); - } - } - } - } - } - consideredObjectives.increment(); - } while (!consideredObjectives.empty()); - } - - for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { - for (auto const& modelState : additionalReachableStates[memState]) { - productBuilder.addReachableState(modelState, memState); - } - } - } - - template - storm::models::sparse::Mdp const& MultiDimensionalRewardUnfolding::MemoryProduct::getProduct() const { - return *product; - } - - template - std::vector::Epoch> const& MultiDimensionalRewardUnfolding::MemoryProduct::getSteps() const { - return steps; - } - - template - bool MultiDimensionalRewardUnfolding::MemoryProduct::productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve whether a product state exists but the memoryStateMap is not yet initialized."); - return modelMemoryToProductStateMap[modelState * memoryStateMap.size() + memoryState] < getProduct().getNumberOfStates(); - } - - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getProductState(uint64_t const& modelState, uint64_t const& memoryState) const { - STORM_LOG_ASSERT(productStateExists(modelState, memoryState), "Tried to obtain a state in the model-memory-product that does not exist"); - return modelMemoryToProductStateMap[modelState * memoryStateMap.size() + memoryState]; - } - - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getModelState(uint64_t const& productState) const { - return productToModelStateMap[productState]; - } - - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getMemoryState(uint64_t const& productState) const { - return productToMemoryStateMap[productState]; - } - - template - storm::storage::BitVector const& MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(uint64_t const& memoryState) const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); - return memoryStateMap[memoryState]; - } - - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(storm::storage::BitVector const& memoryState) const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); - auto memStateIt = std::find(memoryStateMap.begin(), memoryStateMap.end(), memoryState); - return memStateIt - memoryStateMap.begin(); - } - - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getNumberOfMemoryState() const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve the number of memory states but the memoryStateMap is not yet initialized."); - return memoryStateMap.size(); - } - - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getProductStateFromChoice(uint64_t const& productChoice) const { - return choiceToStateMap[productChoice]; - } - - template - std::vector> MultiDimensionalRewardUnfolding::computeObjectiveRewardsForProduct(Epoch const& epoch) const { - std::vector> objectiveRewards; - objectiveRewards.reserve(objectives.size()); - - for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - auto const& formula = *this->objectives[objIndex].formula; - if (formula.isProbabilityOperatorFormula()) { - storm::modelchecker::SparsePropositionalModelChecker> mc(memoryProduct.getProduct()); - std::vector dimensionIndexMap; - for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { - dimensionIndexMap.push_back(globalDimensionIndex); - } - - std::shared_ptr sinkStatesFormula; - for (auto const& dim : objectiveDimensions[objIndex]) { - auto memLabelFormula = std::make_shared(memoryLabels[dim].get()); - if (sinkStatesFormula) { - sinkStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, sinkStatesFormula, memLabelFormula); - } else { - sinkStatesFormula = memLabelFormula; - } - } - sinkStatesFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, sinkStatesFormula); - - std::vector objRew(memoryProduct.getProduct().getTransitionMatrix().getRowCount(), storm::utility::zero()); - storm::storage::BitVector relevantObjectives(objectiveDimensions[objIndex].getNumberOfSetBits()); - - while (!relevantObjectives.full()) { - relevantObjectives.increment(); - - // find out whether objective reward should be earned within this epoch - bool collectRewardInEpoch = true; - for (auto const& subObjIndex : relevantObjectives) { - if (epochManager.isBottomDimension(epoch, dimensionIndexMap[subObjIndex])) { - collectRewardInEpoch = false; - break; - } - } - - if (collectRewardInEpoch) { - std::shared_ptr relevantStatesFormula; - std::shared_ptr goalStatesFormula = storm::logic::CloneVisitor().clone(*sinkStatesFormula); - for (uint64_t subObjIndex = 0; subObjIndex < dimensionIndexMap.size(); ++subObjIndex) { - std::shared_ptr memLabelFormula = std::make_shared(memoryLabels[dimensionIndexMap[subObjIndex]].get()); - if (relevantObjectives.get(subObjIndex)) { - auto rightSubFormula = subObjectives[dimensionIndexMap[subObjIndex]].first->asBoundedUntilFormula().getRightSubformula().asSharedPointer(); - goalStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, goalStatesFormula, rightSubFormula); - } else { - memLabelFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, memLabelFormula); - } - if (relevantStatesFormula) { - relevantStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, relevantStatesFormula, memLabelFormula); - } else { - relevantStatesFormula = memLabelFormula; - } - } - - storm::storage::BitVector relevantStates = mc.check(*relevantStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - storm::storage::BitVector relevantChoices = memoryProduct.getProduct().getTransitionMatrix().getRowFilter(relevantStates); - storm::storage::BitVector goalStates = mc.check(*goalStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - for (auto const& choice : relevantChoices) { - objRew[choice] += memoryProduct.getProduct().getTransitionMatrix().getConstrainedRowSum(choice, goalStates); - } - } - } - - objectiveRewards.push_back(std::move(objRew)); - - } else if (formula.isRewardOperatorFormula()) { - auto const& rewModel = memoryProduct.getProduct().getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); - STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); - bool rewardCollectedInEpoch = true; - if (formula.getSubformula().isCumulativeRewardFormula()) { - assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1); - rewardCollectedInEpoch = !epochManager.isBottomDimension(epoch, *objectiveDimensions[objIndex].begin()); - } else { - STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); - } - if (rewardCollectedInEpoch) { - objectiveRewards.push_back(rewModel.getTotalRewardVector(memoryProduct.getProduct().getTransitionMatrix())); - } else { - objectiveRewards.emplace_back(memoryProduct.getProduct().getTransitionMatrix().getRowCount(), storm::utility::zero()); - } - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); - } - } - - return objectiveRewards; - } - template class MultiDimensionalRewardUnfolding; template class MultiDimensionalRewardUnfolding; template class MultiDimensionalRewardUnfolding; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index b47522c9e..a749f5300 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -6,12 +6,10 @@ #include "storm/storage/SparseMatrix.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/modelchecker/multiobjective/rewardbounded/EpochManager.h" -#include "storm/modelchecker/CheckTask.h" +#include "storm/modelchecker/multiobjective/rewardbounded/ProductModel.h" #include "storm/models/sparse/Mdp.h" #include "storm/utility/vector.h" #include "storm/storage/memorystructure/MemoryStructure.h" -#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" -#include "storm/transformer/EndComponentEliminator.h" #include "storm/utility/Stopwatch.h" namespace storm { @@ -23,7 +21,7 @@ namespace storm { class MultiDimensionalRewardUnfolding { public: - typedef uint64_t Epoch; // The number of reward steps that are "left" for each dimension + typedef typename EpochManager::Epoch Epoch; // The number of reward steps that are "left" for each dimension typedef typename std::conditional>::type SolutionType; @@ -58,7 +56,7 @@ namespace storm { 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 << " Product size: " << productModel->getProduct().getNumberOfStates() << std::endl; std::cout << "maxSolutionsStored: " << maxSolutionsStored << std::endl; std::cout << " Epoch model sizes: "; for (auto const& i : epochModelSizes) { @@ -82,45 +80,7 @@ namespace storm { private: - class MemoryProduct { - public: - MemoryProduct() = default; - 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; - - bool productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const; - uint64_t getProductState(uint64_t const& modelState, uint64_t const& memoryState) const; - uint64_t getModelState(uint64_t const& productState) const; - uint64_t getMemoryState(uint64_t const& productState) const; - - uint64_t convertMemoryState(storm::storage::BitVector const& memoryState) const; - storm::storage::BitVector const& convertMemoryState(uint64_t const& memoryState) const; - - uint64_t getNumberOfMemoryState() const; - - 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; - - std::vector modelMemoryToProductStateMap; - std::vector productToModelStateMap; - std::vector productToMemoryStateMap; - std::vector choiceToStateMap; - std::vector memoryStateMap; - - }; - void setCurrentEpochClass(Epoch const& epoch); - storm::storage::BitVector computeProductInStatesForEpochClass(Epoch const& epoch); - void initialize(); void initializeObjectives(std::vector& epochSteps); @@ -128,10 +88,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; - private: - template::type = 0> SolutionType getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const; template::type = 0> @@ -154,7 +111,7 @@ namespace storm { storm::models::sparse::Mdp const& model; std::vector> objectives; - MemoryProduct memoryProduct; + std::unique_ptr> productModel; std::vector epochModelToProductChoiceMap; std::vector productToEpochModelStateMap; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp new file mode 100644 index 000000000..fbcdfbb1b --- /dev/null +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp @@ -0,0 +1,388 @@ +#include "storm/modelchecker/multiobjective/rewardbounded/ProductModel.h" + + +#include "storm/utility/macros.h" +#include "storm/logic/Formulas.h" +#include "storm/logic/CloneVisitor.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" + +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + ProductModel::ProductModel(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector&& memoryStateMap, std::vector const& originalModelSteps) : objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateMap(std::move(memoryStateMap)) { + + storm::storage::SparseModelMemoryProduct productBuilder(memory.product(model)); + + setReachableStates(productBuilder, originalModelSteps); + product = productBuilder.build()->template as>(); + + uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); + uint64_t numMemoryStates = productBuilder.getMemory().getNumberOfStates(); + uint64_t numProductStates = getProduct().getNumberOfStates(); + + // Compute a mappings from product states to model/memory states and back + modelMemoryToProductStateMap.resize(numMemoryStates * numModelStates, std::numeric_limits::max()); + productToModelStateMap.resize(numProductStates, std::numeric_limits::max()); + productToMemoryStateMap.resize(numProductStates, std::numeric_limits::max()); + for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { + for (uint64_t memoryState = 0; memoryState < numMemoryStates; ++memoryState) { + if (productBuilder.isStateReachable(modelState, memoryState)) { + uint64_t productState = productBuilder.getResultState(modelState, memoryState); + modelMemoryToProductStateMap[modelState * numMemoryStates + memoryState] = productState; + productToModelStateMap[productState] = modelState; + productToMemoryStateMap[productState] = memoryState; + } + } + } + + // Map choice indices of the product to the state where it origins + choiceToStateMap.reserve(getProduct().getNumberOfChoices()); + for (uint64_t productState = 0; productState < numProductStates; ++productState) { + uint64_t groupSize = getProduct().getTransitionMatrix().getRowGroupSize(productState); + for (uint64_t i = 0; i < groupSize; ++i) { + choiceToStateMap.push_back(productState); + } + } + + // Compute the epoch steps for the product + steps.resize(getProduct().getNumberOfChoices(), 0); + for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { + uint64_t numChoices = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupSize(modelState); + uint64_t firstChoice = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupIndices()[modelState]; + for (uint64_t choiceOffset = 0; choiceOffset < numChoices; ++choiceOffset) { + Epoch const& step = originalModelSteps[firstChoice + choiceOffset]; + if (step != 0) { + for (uint64_t memState = 0; memState < numMemoryStates; ++memState) { + if (productStateExists(modelState, memState)) { + uint64_t productState = getProductState(modelState, memState); + uint64_t productChoice = getProduct().getTransitionMatrix().getRowGroupIndices()[productState] + choiceOffset; + assert(productChoice < getProduct().getTransitionMatrix().getRowGroupIndices()[productState + 1]); + steps[productChoice] = step; + } + } + } + } + } + } + + template + void ProductModel::setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const { + + std::vector additionalReachableStates(memoryStateMap.size(), storm::storage::BitVector(productBuilder.getOriginalModel().getNumberOfStates(), false)); + for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { + auto const& memStateBv = memoryStateMap[memState]; + storm::storage::BitVector consideredObjectives(objectiveDimensions.size(), false); + do { + storm::storage::BitVector memStatePrimeBv = memStateBv; + for (auto const& objIndex : consideredObjectives) { + memStatePrimeBv &= ~objectiveDimensions[objIndex]; + } + if (memStatePrimeBv != memStateBv) { + for (uint64_t choice = 0; choice < productBuilder.getOriginalModel().getTransitionMatrix().getRowCount(); ++choice) { + bool consideredChoice = true; + for (auto const& objIndex : consideredObjectives) { + bool objectiveHasStep = false; + for (auto const& dim : objectiveDimensions[objIndex]) { + if (epochManager.getDimensionOfEpoch(originalModelSteps[choice], dim) > 0) { + objectiveHasStep = true; + break; + } + } + if (!objectiveHasStep) { + consideredChoice = false; + break; + } + } + if (consideredChoice) { + for (auto const& successor : productBuilder.getOriginalModel().getTransitionMatrix().getRow(choice)) { + if (productBuilder.isStateReachable(successor.getColumn(), memState)) { + additionalReachableStates[convertMemoryState(memStatePrimeBv)].set(successor.getColumn()); + } + } + } + } + } + consideredObjectives.increment(); + } while (!consideredObjectives.empty()); + } + + for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { + for (auto const& modelState : additionalReachableStates[memState]) { + productBuilder.addReachableState(modelState, memState); + } + } + } + + template + storm::models::sparse::Mdp const& ProductModel::getProduct() const { + return *product; + } + + template + std::vector::Epoch> const& ProductModel::getSteps() const { + return steps; + } + + template + bool ProductModel::productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve whether a product state exists but the memoryStateMap is not yet initialized."); + return modelMemoryToProductStateMap[modelState * memoryStateMap.size() + memoryState] < getProduct().getNumberOfStates(); + } + + template + uint64_t ProductModel::getProductState(uint64_t const& modelState, uint64_t const& memoryState) const { + STORM_LOG_ASSERT(productStateExists(modelState, memoryState), "Tried to obtain a state in the model-memory-product that does not exist"); + return modelMemoryToProductStateMap[modelState * memoryStateMap.size() + memoryState]; + } + + template + uint64_t ProductModel::getModelState(uint64_t const& productState) const { + return productToModelStateMap[productState]; + } + + template + uint64_t ProductModel::getMemoryState(uint64_t const& productState) const { + return productToMemoryStateMap[productState]; + } + + template + storm::storage::BitVector const& ProductModel::convertMemoryState(uint64_t const& memoryState) const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); + return memoryStateMap[memoryState]; + } + + template + uint64_t ProductModel::convertMemoryState(storm::storage::BitVector const& memoryState) const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); + auto memStateIt = std::find(memoryStateMap.begin(), memoryStateMap.end(), memoryState); + return memStateIt - memoryStateMap.begin(); + } + + template + uint64_t ProductModel::getNumberOfMemoryState() const { + STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve the number of memory states but the memoryStateMap is not yet initialized."); + return memoryStateMap.size(); + } + + template + uint64_t ProductModel::getProductStateFromChoice(uint64_t const& productChoice) const { + return choiceToStateMap[productChoice]; + } + + template + std::vector> ProductModel::computeObjectiveRewards(Epoch const& epoch, std::vector> const& objectives, std::vector, uint64_t>> subObjectives, std::vector> const& memoryLabels) const { + std::vector> objectiveRewards; + objectiveRewards.reserve(objectives.size()); + + for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { + auto const& formula = *objectives[objIndex].formula; + if (formula.isProbabilityOperatorFormula()) { + storm::modelchecker::SparsePropositionalModelChecker> mc(getProduct()); + std::vector dimensionIndexMap; + for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { + dimensionIndexMap.push_back(globalDimensionIndex); + } + + std::shared_ptr sinkStatesFormula; + for (auto const& dim : objectiveDimensions[objIndex]) { + auto memLabelFormula = std::make_shared(memoryLabels[dim].get()); + if (sinkStatesFormula) { + sinkStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, sinkStatesFormula, memLabelFormula); + } else { + sinkStatesFormula = memLabelFormula; + } + } + sinkStatesFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, sinkStatesFormula); + + std::vector objRew(getProduct().getTransitionMatrix().getRowCount(), storm::utility::zero()); + storm::storage::BitVector relevantObjectives(objectiveDimensions[objIndex].getNumberOfSetBits()); + + while (!relevantObjectives.full()) { + relevantObjectives.increment(); + + // find out whether objective reward should be earned within this epoch + bool collectRewardInEpoch = true; + for (auto const& subObjIndex : relevantObjectives) { + if (epochManager.isBottomDimension(epoch, dimensionIndexMap[subObjIndex])) { + collectRewardInEpoch = false; + break; + } + } + + if (collectRewardInEpoch) { + std::shared_ptr relevantStatesFormula; + std::shared_ptr goalStatesFormula = storm::logic::CloneVisitor().clone(*sinkStatesFormula); + for (uint64_t subObjIndex = 0; subObjIndex < dimensionIndexMap.size(); ++subObjIndex) { + std::shared_ptr memLabelFormula = std::make_shared(memoryLabels[dimensionIndexMap[subObjIndex]].get()); + if (relevantObjectives.get(subObjIndex)) { + auto rightSubFormula = subObjectives[dimensionIndexMap[subObjIndex]].first->asBoundedUntilFormula().getRightSubformula().asSharedPointer(); + goalStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, goalStatesFormula, rightSubFormula); + } else { + memLabelFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, memLabelFormula); + } + if (relevantStatesFormula) { + relevantStatesFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, relevantStatesFormula, memLabelFormula); + } else { + relevantStatesFormula = memLabelFormula; + } + } + + storm::storage::BitVector relevantStates = mc.check(*relevantStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector relevantChoices = getProduct().getTransitionMatrix().getRowFilter(relevantStates); + storm::storage::BitVector goalStates = mc.check(*goalStatesFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + for (auto const& choice : relevantChoices) { + objRew[choice] += getProduct().getTransitionMatrix().getConstrainedRowSum(choice, goalStates); + } + } + } + + objectiveRewards.push_back(std::move(objRew)); + + } else if (formula.isRewardOperatorFormula()) { + auto const& rewModel = getProduct().getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); + STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected."); + bool rewardCollectedInEpoch = true; + if (formula.getSubformula().isCumulativeRewardFormula()) { + assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1); + rewardCollectedInEpoch = !epochManager.isBottomDimension(epoch, *objectiveDimensions[objIndex].begin()); + } else { + STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); + } + if (rewardCollectedInEpoch) { + objectiveRewards.push_back(rewModel.getTotalRewardVector(getProduct().getTransitionMatrix())); + } else { + objectiveRewards.emplace_back(getProduct().getTransitionMatrix().getRowCount(), storm::utility::zero()); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); + } + } + + return objectiveRewards; + } + + template + storm::storage::BitVector ProductModel::computeInStates(Epoch const& epoch) const { + storm::storage::SparseMatrix const& productMatrix = getProduct().getTransitionMatrix(); + + // Initialize the result. Initial states are only considered if the epoch contains no bottom dimension. + storm::storage::BitVector result; + if (epochManager.hasBottomDimension(epoch)) { + result = storm::storage::BitVector(getProduct().getNumberOfStates()); + } else { + result = getProduct().getInitialStates(); + } + + // Compute the set of objectives that can not be satisfied anymore in the current epoch + storm::storage::BitVector irrelevantObjectives(objectiveDimensions.size(), false); + for (uint64_t objIndex = 0; objIndex < objectiveDimensions.size(); ++objIndex) { + bool objIrrelevant = true; + for (auto const& dim : objectiveDimensions[objIndex]) { + if (!epochManager.isBottomDimension(epoch, dim)) { + objIrrelevant = false; + } + } + if (objIrrelevant) { + irrelevantObjectives.set(objIndex, true); + } + } + + // Perform DFS + storm::storage::BitVector reachableStates = getProduct().getInitialStates(); + std::vector stack(reachableStates.begin(), reachableStates.end()); + + while (!stack.empty()) { + uint64_t state = stack.back(); + stack.pop_back(); + for (uint64_t choice = productMatrix.getRowGroupIndices()[state]; choice < productMatrix.getRowGroupIndices()[state + 1]; ++choice) { + auto const& choiceStep = getSteps()[choice]; + if (!epochManager.isZeroEpoch(choiceStep)) { + + // Compute the set of objectives that might or might not become irrelevant when the epoch is reached via the current choice + storm::storage::BitVector maybeIrrelevantObjectives(objectiveDimensions.size(), false); + for (uint64_t objIndex = 0; objIndex < objectiveDimensions.size(); ++objIndex) { + for (auto const& dim : objectiveDimensions[objIndex]) { + if (epochManager.isBottomDimension(epoch, dim) && epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { + maybeIrrelevantObjectives.set(objIndex); + break; + } + } + } + maybeIrrelevantObjectives &= ~irrelevantObjectives; + + // For optimization purposes, we treat the case that all objectives will be relevant seperately + if (maybeIrrelevantObjectives.empty() && irrelevantObjectives.empty()) { + for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { + result.set(choiceSuccessor.getColumn(), true); + if (!reachableStates.get(choiceSuccessor.getColumn())) { + reachableStates.set(choiceSuccessor.getColumn()); + stack.push_back(choiceSuccessor.getColumn()); + } + } + } else { + // Enumerate all possible combinations of maybe relevant objectives + storm::storage::BitVector maybeObjSubset(maybeIrrelevantObjectives.getNumberOfSetBits(), false); + do { + for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { + // Compute the successor memory state for the current objective-subset and transition + storm::storage::BitVector successorMemoryState = convertMemoryState(getMemoryState(choiceSuccessor.getColumn())); + // Unselect dimensions belonging to irrelevant objectives + for (auto const& irrelevantObjIndex : irrelevantObjectives) { + successorMemoryState &= ~objectiveDimensions[irrelevantObjIndex]; + } + // Unselect objectives that are not in the current subset of maybe relevant objectives + // We can skip a subset if it selects an objective that is irrelevant anyway (according to the original successor memorystate). + bool skipThisSubSet = false; + uint64_t i = 0; + for (auto const& objIndex : maybeIrrelevantObjectives) { + if (maybeObjSubset.get(i)) { + if (successorMemoryState.isDisjointFrom(objectiveDimensions[objIndex])) { + skipThisSubSet = true; + break; + } else { + successorMemoryState &= ~objectiveDimensions[objIndex]; + } + } + ++i; + } + if (!skipThisSubSet) { + uint64_t successorState = getProductState(getModelState(choiceSuccessor.getColumn()), convertMemoryState(successorMemoryState)); + result.set(successorState, true); + if (!reachableStates.get(successorState)) { + reachableStates.set(successorState); + stack.push_back(successorState); + } + } + } + + maybeObjSubset.increment(); + } while (!maybeObjSubset.empty()); + } + } else { + for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { + if (!reachableStates.get(choiceSuccessor.getColumn())) { + reachableStates.set(choiceSuccessor.getColumn()); + stack.push_back(choiceSuccessor.getColumn()); + } + } + } + } + } + + return result; + } + + template class ProductModel; + template class ProductModel; + + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h new file mode 100644 index 000000000..0fa2e0796 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h @@ -0,0 +1,64 @@ +#pragma once + +#include + +#include "storm/storage/BitVector.h" +#include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/modelchecker/multiobjective/rewardbounded/EpochManager.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/utility/vector.h" +#include "storm/storage/memorystructure/MemoryStructure.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + + template + class ProductModel { + public: + + typedef typename EpochManager::Epoch Epoch; + + ProductModel(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector&& memoryStateMap, std::vector const& originalModelSteps); + + storm::models::sparse::Mdp const& getProduct() const; + std::vector const& getSteps() const; + + bool productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const; + uint64_t getProductState(uint64_t const& modelState, uint64_t const& memoryState) const; + uint64_t getModelState(uint64_t const& productState) const; + uint64_t getMemoryState(uint64_t const& productState) const; + + uint64_t convertMemoryState(storm::storage::BitVector const& memoryState) const; + storm::storage::BitVector const& convertMemoryState(uint64_t const& memoryState) const; + + uint64_t getNumberOfMemoryState() const; + + uint64_t getProductStateFromChoice(uint64_t const& productChoice) const; + + std::vector> computeObjectiveRewards(Epoch const& epoch, std::vector> const& objectives, std::vector, uint64_t>> subObjectives, std::vector> const& memoryLabels) const; + storm::storage::BitVector computeInStates(Epoch const& epoch) const; + + + private: + + void setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const; + + std::vector const& objectiveDimensions; + EpochManager const& epochManager; + + std::shared_ptr> product; + std::vector steps; + + std::vector modelMemoryToProductStateMap; + std::vector productToModelStateMap; + std::vector productToMemoryStateMap; + std::vector choiceToStateMap; + std::vector memoryStateMap; + + }; + } + } +} \ No newline at end of file