diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index fc732c597..bc881c089 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -154,7 +154,7 @@ namespace storm { // build a mapping between the different representations of memory states auto memoryStateMap = computeMemoryStateMap(memoryStructure); - productModel = std::make_unique>(model, memoryStructure, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps); + productModel = std::make_unique>(model, memoryStructure, dimensions, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps); } @@ -276,11 +276,6 @@ namespace storm { } swSetEpoch.start(); - epochModel.objectiveRewardFilter.clear(); - for (auto const& objRewards : epochModel.objectiveRewards) { - epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards)); - epochModel.objectiveRewardFilter.back().complement(); - } epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); auto stepSolIt = epochModel.stepSolutions.begin(); @@ -291,19 +286,24 @@ namespace storm { 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 + // Objective reward is not earned if + // a) there is an upper bounded subObjective that is still relevant but the corresponding reward bound is passed after taking the choice + // b) there is a lower bounded subObjective and the corresponding reward bound is not passed yet. for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if (epochModel.objectiveRewardFilter[objIndex].get(reducedChoice)) { + bool rewardEarned = !storm::utility::isZero(epochModel.objectiveRewards[objIndex][reducedChoice]); + if (rewardEarned) { for (auto const& dim : objectiveDimensions[objIndex]) { if (dimensions[dim].isUpperBounded == epochManager.isBottomDimension(successorEpoch, dim) && memoryState.get(dim)) { - epochModel.objectiveRewardFilter[objIndex].set(reducedChoice, false); + rewardEarned = false; break; } } } + epochModel.objectiveRewardFilter[objIndex].set(reducedChoice, rewardEarned); } // compute the solution for the stepChoices + // For optimization purposes, we distinguish the easier case where the successor epoch lies in the same epoch class SolutionType choiceSolution; bool firstSuccessor = true; if (epochManager.compareEpochClass(epoch, successorEpoch)) { @@ -316,14 +316,17 @@ namespace storm { } } } else { - storm::storage::BitVector successorRelevantDimensions(epochManager.getDimensionCount(), true); + storm::storage::BitVector allowedRelevantDimensions(epochManager.getDimensionCount(), true); + storm::storage::BitVector forcedRelevantDimensions(epochManager.getDimensionCount(), false); for (auto const& dim : memoryState) { - if (epochManager.isBottomDimension(successorEpoch, dim)) { - successorRelevantDimensions &= ~objectiveDimensions[dimensions[dim].objectiveIndex]; + if (epochManager.isBottomDimension(successorEpoch, dim) && dimensions[dim].isUpperBounded) { + allowedRelevantDimensions &= ~objectiveDimensions[dimensions[dim].objectiveIndex]; + } else if (!epochManager.isBottomDimension(successorEpoch, dim) && !dimensions[dim].isUpperBounded) { + forcedRelevantDimensions.set(dim, true); } } for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { - storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & successorRelevantDimensions; + storm::storage::BitVector successorMemoryState = (productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & allowedRelevantDimensions) | forcedRelevantDimensions; uint64_t successorProductState = productModel->getProductState(productModel->getModelState(successor.getColumn()), productModel->convertMemoryState(successorMemoryState)); SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); if (firstSuccessor) { @@ -366,10 +369,11 @@ namespace storm { template void MultiDimensionalRewardUnfolding::setCurrentEpochClass(Epoch const& epoch) { + EpochClass epochClass = epochManager.getEpochClass(epoch); // std::cout << "Setting epoch class for epoch " << storm::utility::vector::toString(epoch) << std::endl; swSetEpochClass.start(); swAux1.start(); - auto productObjectiveRewards = productModel->computeObjectiveRewards(epoch, objectives, dimensions); + auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives); storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false); uint64_t choice = 0; @@ -380,17 +384,33 @@ namespace storm { ++choice; } epochModel.epochMatrix = productModel->getProduct().getTransitionMatrix().filterEntries(~stepChoices); + // redirect transitions for the case where the lower reward bounds are not met yet + storm::storage::BitVector violatedLowerBoundedDimensions(dimensions.size(), false); + for (uint64_t dim = 0; dim < dimensions.size(); ++dim) { + if (!dimensions[dim].isUpperBounded && !epochManager.isBottomDimensionEpochClass(epochClass, dim)) { + violatedLowerBoundedDimensions.set(dim); + } + } + if (!violatedLowerBoundedDimensions.empty()) { + for (auto& entry : epochModel.epochMatrix) { + storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(entry.getColumn())); + successorMemoryState |= violatedLowerBoundedDimensions; + entry.setColumn(productModel->getProductState(productModel->getModelState(entry.getColumn()), productModel->convertMemoryState(successorMemoryState))); + } + } storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getNumberOfChoices(), true); - for (auto const& objRewards : productObjectiveRewards) { - zeroObjRewardChoices &= storm::utility::vector::filterZero(objRewards); + for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { + if (violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) { + zeroObjRewardChoices &= storm::utility::vector::filterZero(productObjectiveRewards[objIndex]); + } } swAux1.stop(); swAux2.start(); storm::storage::BitVector allProductStates(productModel->getProduct().getNumberOfStates(), true); // Get the relevant states for this epoch. - storm::storage::BitVector productInStates = productModel->computeInStates(epoch); + storm::storage::BitVector productInStates = productModel->getInStates(epochClass); // 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; @@ -414,11 +434,22 @@ namespace storm { } epochModel.objectiveRewards.clear(); - for (auto const& productObjRew : productObjectiveRewards) { + for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { + bool objHasViolatedLowerDimension = false; + for (auto const& dim : objectiveDimensions[objIndex]) { + if (!dimensions[dim].isUpperBounded && !epochManager.isBottomDimensionEpochClass(epochClass, dim)) { + objHasViolatedLowerDimension = true; + } + } std::vector reducedModelObjRewards; - reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount()); - for (auto const& productChoice : epochModelToProductChoiceMap) { - reducedModelObjRewards.push_back(productObjRew[productChoice]); + if (objHasViolatedLowerDimension) { + reducedModelObjRewards.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero()); + } else { + std::vector const& productObjRew = productObjectiveRewards[objIndex]; + reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount()); + for (auto const& productChoice : epochModelToProductChoiceMap) { + reducedModelObjRewards.push_back(productObjRew[productChoice]); + } } epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } @@ -437,6 +468,12 @@ namespace storm { } productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); + epochModel.objectiveRewardFilter.clear(); + for (auto const& objRewards : epochModel.objectiveRewards) { + epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards)); + epochModel.objectiveRewardFilter.back().complement(); + } + swAux4.stop(); swSetEpochClass.stop(); epochModelSizes.push_back(epochModel.epochMatrix.getRowGroupCount()); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 2237fe47b..f37c09e71 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -23,6 +23,7 @@ namespace storm { public: typedef typename EpochManager::Epoch Epoch; // The number of reward steps that are "left" for each dimension + typedef typename EpochManager::EpochClass EpochClass; typedef typename std::conditional>::type SolutionType; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp index 2cd3104d8..4b415eaec 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp @@ -17,11 +17,11 @@ namespace storm { 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)) { + ProductModel::ProductModel(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector&& memoryStateMap, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateMap(std::move(memoryStateMap)) { storm::storage::SparseModelMemoryProduct productBuilder(memory.product(model)); - setReachableStates(productBuilder, originalModelSteps); + setReachableProductStates(productBuilder, originalModelSteps); product = productBuilder.build()->template as>(); uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); @@ -71,52 +71,97 @@ namespace storm { } } } + + computeReachableStatesInEpochClasses(); } template - void ProductModel::setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const { + void ProductModel::setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const { + + storm::storage::BitVector lowerBoundedDimensions(dimensions.size(), false); + for (uint64_t dim = 0; dim < dimensions.size(); ++dim) { + if (!dimensions[dim].isUpperBounded) { + lowerBoundedDimensions.set(dim); + } + } + // We add additional reachable states until no more states are found 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; + bool converged = false; + while (!converged) { + for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { + auto const& memStateBv = memoryStateMap[memState]; + storm::storage::BitVector consideredObjectives(objectiveDimensions.size(), false); + do { + // The current set of considered objectives can be skipped if it contains an objective that only consists of dimensions with lower reward bounds + bool skipThisObjectiveSet = false; + for (auto const& objindex : consideredObjectives) { + if (objectiveDimensions[objindex].isSubsetOf(lowerBoundedDimensions)) { + skipThisObjectiveSet = true; + } + } + if (!skipThisObjectiveSet) { + storm::storage::BitVector memStatePrimeBv = memStateBv; for (auto const& objIndex : consideredObjectives) { - bool objectiveHasStep = false; - for (auto const& dim : objectiveDimensions[objIndex]) { - if (epochManager.getDimensionOfEpoch(originalModelSteps[choice], dim) > 0) { - objectiveHasStep = true; - break; + memStatePrimeBv &= ~objectiveDimensions[objIndex]; + } + if (memStatePrimeBv != memStateBv) { + uint64_t memStatePrime = convertMemoryState(memStatePrimeBv); + for (uint64_t choice = 0; choice < productBuilder.getOriginalModel().getTransitionMatrix().getRowCount(); ++choice) { + // Consider the choice only if for every considered objective there is one dimension for which the step of this choice is positive + bool consideredChoice = true; + for (auto const& objIndex : consideredObjectives) { + bool objectiveHasStep = false; + auto upperBoundedObjectiveDimensions = objectiveDimensions[objIndex] & (~lowerBoundedDimensions); + for (auto const& dim : upperBoundedObjectiveDimensions) { + 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) && !productBuilder.isStateReachable(successor.getColumn(), memStatePrime)) { + additionalReachableStates[memStatePrime].set(successor.getColumn()); + } + } } - } - 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()); + } + + storm::storage::BitVector consideredDimensions(dimensions.size(), false); + do { + if (consideredDimensions.isSubsetOf(lowerBoundedDimensions)) { + for (uint64_t memoryState = 0; memoryState < productBuilder.getMemory().getNumberOfStates(); ++memoryState) { + uint64_t memoryStatePrime = convertMemoryState(convertMemoryState(memoryState) | consideredDimensions); + for (uint64_t modelState = 0; modelState < productBuilder.getOriginalModel().getNumberOfStates(); ++modelState) { + if (productBuilder.isStateReachable(modelState, memoryState) && !productBuilder.isStateReachable(modelState, memoryStatePrime)) { + additionalReachableStates[memoryStatePrime].set(modelState); } } } } - consideredObjectives.increment(); - } while (!consideredObjectives.empty()); - } - - for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { - for (auto const& modelState : additionalReachableStates[memState]) { - productBuilder.addReachableState(modelState, memState); + consideredDimensions.increment(); + } while (!consideredDimensions.empty()); + + converged = true; + for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { + if (!additionalReachableStates[memState].empty()) { + converged = false; + for (auto const& modelState : additionalReachableStates[memState]) { + productBuilder.addReachableState(modelState, memState); + } + additionalReachableStates[memState].clear(); + } } } } @@ -178,7 +223,7 @@ namespace storm { } template - std::vector> ProductModel::computeObjectiveRewards(Epoch const& epoch, std::vector> const& objectives, std::vector> const& dimensions) const { + std::vector> ProductModel::computeObjectiveRewards(EpochClass const& epochClass, std::vector> const& objectives) const { std::vector> objectiveRewards; objectiveRewards.reserve(objectives.size()); @@ -208,10 +253,10 @@ namespace storm { while (!relevantObjectives.full()) { relevantObjectives.increment(); - // find out whether objective reward should be earned within this epoch + // find out whether objective reward should be earned within this epoch class bool collectRewardInEpoch = true; for (auto const& subObjIndex : relevantObjectives) { - if (dimensions[dimensionIndexMap[subObjIndex]].isUpperBounded == epochManager.isBottomDimension(epoch, dimensionIndexMap[subObjIndex])) { + if (dimensions[dimensionIndexMap[subObjIndex]].isUpperBounded == epochManager.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) { collectRewardInEpoch = false; break; } @@ -252,7 +297,7 @@ namespace storm { bool rewardCollectedInEpoch = true; if (formula.getSubformula().isCumulativeRewardFormula()) { assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1); - rewardCollectedInEpoch = !epochManager.isBottomDimension(epoch, *objectiveDimensions[objIndex].begin()); + rewardCollectedInEpoch = !epochManager.isBottomDimensionEpochClass(epochClass, *objectiveDimensions[objIndex].begin()); } else { STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); } @@ -270,115 +315,157 @@ namespace storm { } template - storm::storage::BitVector ProductModel::computeInStates(Epoch const& epoch) const { - storm::storage::SparseMatrix const& productMatrix = getProduct().getTransitionMatrix(); + storm::storage::BitVector const& ProductModel::getInStates(EpochClass const& epochClass) const { + STORM_LOG_ASSERT(inStates.find(epochClass) != inStates.end(), "Could not find InStates for the given epoch class"); + return inStates.find(epochClass)->second; + } + + template + void ProductModel::computeReachableStatesInEpochClasses() { + std::set possibleSteps(steps.begin(), steps.end()); + std::set> reachableEpochClasses(std::bind(&EpochManager::epochClassOrder, &epochManager, std::placeholders::_1, std::placeholders::_2)); - // 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(); + std::vector candidates({epochManager.getBottomEpoch()}); + std::set newCandidates; + bool converged = false; + while (!converged) { + converged = true; + for (auto const& candidate : candidates) { + converged &= !reachableEpochClasses.insert(epochManager.getEpochClass(candidate)).second; + for (auto const& step : possibleSteps) { + epochManager.gatherPredecessorEpochs(newCandidates, candidate, step); + } + } + candidates.assign(newCandidates.begin(), newCandidates.end()); + newCandidates.clear(); } - // 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; + for (auto epochClassIt = reachableEpochClasses.rbegin(); epochClassIt != reachableEpochClasses.rend(); ++epochClassIt) { + std::vector predecessors; + for (auto predecessorIt = reachableEpochClasses.rbegin(); predecessorIt != epochClassIt; ++predecessorIt) { + if (epochManager.isPredecessorEpochClass(*predecessorIt, *epochClassIt)) { + predecessors.push_back(*predecessorIt); } } - if (objIrrelevant) { - irrelevantObjectives.set(objIndex, true); + computeReachableStates(*epochClassIt, predecessors); + } + } + + + template + void ProductModel::computeReachableStates(EpochClass const& epochClass, std::vector const& predecessors) { + + storm::storage::BitVector bottomDimensions(epochManager.getDimensionCount(), false); + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) { + bottomDimensions.set(dim, true); } } - - // Perform DFS - storm::storage::BitVector reachableStates = getProduct().getInitialStates(); - std::vector stack(reachableStates.begin(), reachableStates.end()); + storm::storage::BitVector nonBottomDimensions = ~bottomDimensions; - 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; - } - } + // Bottom dimensions corresponding to upper bounded subobjectives can not be relevant anymore + // Dimensions with a lower bound where the epoch class is not bottom should stay relevant + storm::storage::BitVector allowedRelevantDimensions(epochManager.getDimensionCount(), true); + storm::storage::BitVector forcedRelevantDimensions(epochManager.getDimensionCount(), false); + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (dimensions[dim].isUpperBounded && bottomDimensions.get(dim)) { + allowedRelevantDimensions.set(dim, false); + } else if (!dimensions[dim].isUpperBounded && nonBottomDimensions.get(dim)) { + forcedRelevantDimensions.set(dim, false); + } + } + assert(forcedRelevantDimensions.isSubsetOf(allowedRelevantDimensions)); + + storm::storage::BitVector ecInStates(getProduct().getNumberOfStates(), false); + + if (!epochManager.hasBottomDimensionEpochClass(epochClass)) { + for (auto const& initState : getProduct().getInitialStates()) { + uint64_t transformedInitState = transformProductState(initState, allowedRelevantDimensions, forcedRelevantDimensions); + ecInStates.set(transformedInitState, true); + } + } + + for (auto const& predecessor : predecessors) { + storm::storage::BitVector positiveStepDimensions(epochManager.getDimensionCount(), false); + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (!epochManager.isBottomDimensionEpochClass(predecessor, dim) && bottomDimensions.get(dim)) { + positiveStepDimensions.set(dim, true); + } + } + STORM_LOG_ASSERT(reachableStates.find(predecessor) != reachableStates.end(), "Could not find reachable states of predecessor epoch class."); + storm::storage::BitVector predecessorChoices = getProduct().getTransitionMatrix().getRowFilter(reachableStates.find(predecessor)->second); + for (auto const& choice : predecessorChoices) { + bool choiceLeadsToThisClass = false; + Epoch const& choiceStep = getSteps()[choice]; + for (auto const& dim : positiveStepDimensions) { + if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { + choiceLeadsToThisClass = true; } - 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()); + } + + if (choiceLeadsToThisClass) { + for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) { + uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions); + ecInStates.set(successorState, true); } - } else { - for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { - if (!reachableStates.get(choiceSuccessor.getColumn())) { - reachableStates.set(choiceSuccessor.getColumn()); - stack.push_back(choiceSuccessor.getColumn()); - } + } + } + } + + // Find all states reachable from an InState via DFS. + storm::storage::BitVector ecReachableStates = ecInStates; + std::vector dfsStack(ecReachableStates.begin(), ecReachableStates.end()); + + while (!dfsStack.empty()) { + uint64_t currentState = dfsStack.back(); + dfsStack.pop_back(); + + for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[currentState]; choice != getProduct().getTransitionMatrix().getRowGroupIndices()[currentState + 1]; ++choice) { + + bool choiceLeadsOutsideOfEpoch = false; + Epoch const& choiceStep = getSteps()[choice]; + for (auto const& dim : nonBottomDimensions) { + if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { + choiceLeadsOutsideOfEpoch = true; + } + } + + for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) { + uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions); + if (choiceLeadsOutsideOfEpoch) { + ecInStates.set(successorState, true); + } + if (!ecReachableStates.get(successorState)) { + ecReachableStates.set(successorState, true); + dfsStack.push_back(successorState); } } } } - return result; + reachableStates[epochClass] = std::move(ecReachableStates); + inStates[epochClass] = std::move(ecInStates); } + + template + uint64_t ProductModel::transformProductState(uint64_t productState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const { + return getProductState(getModelState(productState), transformMemoryState(getMemoryState(productState), allowedRelevantDimensions, forcedRelevantDimensions)); + } + + template + uint64_t ProductModel::transformMemoryState(uint64_t memoryState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const { + if (allowedRelevantDimensions.full() && forcedRelevantDimensions.empty()) { + return memoryState; + } + storm::storage::BitVector memoryStateBv = convertMemoryState(memoryState) | forcedRelevantDimensions; + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (!allowedRelevantDimensions.get(dim) && memoryStateBv.get(dim)) { + memoryStateBv &= ~objectiveDimensions[dimensions[dim].objectiveIndex]; + } + } + return convertMemoryState(memoryStateBv); + } + template class ProductModel; template class ProductModel; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h index b03dfca9f..4c61d2db7 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h @@ -21,8 +21,10 @@ namespace storm { public: typedef typename EpochManager::Epoch Epoch; + typedef typename EpochManager::EpochClass EpochClass; + - 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); + ProductModel(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector> const& dimensions, 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; @@ -39,19 +41,27 @@ namespace storm { uint64_t getProductStateFromChoice(uint64_t const& productChoice) const; - std::vector> computeObjectiveRewards(Epoch const& epoch, std::vector> const& objectives, std::vector> const& dimensions) const; - storm::storage::BitVector computeInStates(Epoch const& epoch) const; + std::vector> computeObjectiveRewards(EpochClass const& epochClass, std::vector> const& objectives) const; + storm::storage::BitVector const& getInStates(EpochClass const& epochClass) const; private: - void setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const; + void setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const; + + void computeReachableStatesInEpochClasses(); + void computeReachableStates(EpochClass const& epochClass, std::vector const& predecessors); + uint64_t transformProductState(uint64_t productState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const; + uint64_t transformMemoryState(uint64_t memoryState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const; + std::vector> const& dimensions; std::vector const& objectiveDimensions; EpochManager const& epochManager; std::shared_ptr> product; std::vector steps; + std::map reachableStates; + std::map inStates; std::vector modelMemoryToProductStateMap; std::vector productToModelStateMap; diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 8c878eb53..e0e82903b 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -18,6 +18,10 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small std::string formulasAsString = "Pmax=? [ F{\"r\"}<=1 x=N ] "; formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]"; formulasAsString += "; \n Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]"; + formulasAsString += "; \n Pmax=? [ F{\"r\"}>=1 x=N ] "; + formulasAsString += "; \n Pmax=? [ F{\"r\"}>=3 x=N ] "; + formulasAsString += "; \n Pmin=? [ F{\"r\"}>=2 x=N ] "; + formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}>=1 x=N, F{\"l\"}>=2 x=0 )]"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); @@ -39,6 +43,22 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); EXPECT_EQ(storm::utility::convertNumber(0.0), result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[3], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(1.0), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[4], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(1.0), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[5], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(0.0), result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[6], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_EQ(storm::utility::convertNumber(1.0), result->asExplicitQuantitativeCheckResult()[initState]); + } TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) {