diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index bc881c089..9af9fe78a 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -155,7 +155,6 @@ namespace storm { auto memoryStateMap = computeMemoryStateMap(memoryStructure); productModel = std::make_unique>(model, memoryStructure, dimensions, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps); - } template @@ -276,6 +275,13 @@ namespace storm { } swSetEpoch.start(); + bool containsLowerBoundedObjective = false; + for (auto const& dimension : dimensions) { + if (!dimension.isUpperBounded) { + containsLowerBoundedObjective = true; + break; + } + } epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); auto stepSolIt = epochModel.stepSolutions.begin(); @@ -301,12 +307,11 @@ namespace storm { } 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)) { + if (!containsLowerBoundedObjective && epochManager.compareEpochClass(epoch, successorEpoch)) { for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { if (firstSuccessor) { choiceSolution = getScaledSolution(getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); @@ -326,7 +331,7 @@ namespace storm { } } for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { - storm::storage::BitVector successorMemoryState = (productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & allowedRelevantDimensions) | forcedRelevantDimensions; + storm::storage::BitVector successorMemoryState = (productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) | forcedRelevantDimensions) & allowedRelevantDimensions; uint64_t successorProductState = productModel->getProductState(productModel->getModelState(successor.getColumn()), productModel->convertMemoryState(successorMemoryState)); SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); if (firstSuccessor) { @@ -370,7 +375,7 @@ 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; + // std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << std::endl; swSetEpochClass.start(); swAux1.start(); auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives); @@ -392,10 +397,14 @@ namespace storm { } } 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))); + for (uint64_t state = 0; state < epochModel.epochMatrix.getRowGroupCount(); ++state) { + auto const& memoryState = productModel->convertMemoryState(productModel->getMemoryState(state)); + storm::storage::BitVector forcedRelevantDimensions = memoryState & violatedLowerBoundedDimensions; + for (auto& entry : epochModel.epochMatrix.getRowGroup(state)) { + storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(entry.getColumn())); + successorMemoryState |= forcedRelevantDimensions; + entry.setColumn(productModel->getProductState(productModel->getModelState(entry.getColumn()), productModel->convertMemoryState(successorMemoryState))); + } } } @@ -435,21 +444,15 @@ namespace storm { epochModel.objectiveRewards.clear(); 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 const& productObjRew = productObjectiveRewards[objIndex]; std::vector reducedModelObjRewards; - 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]); - } + reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount()); + for (auto const& productChoice : epochModelToProductChoiceMap) { + reducedModelObjRewards.push_back(productObjRew[productChoice]); + } + // Check if the objective is violated in the current epoch + if (!violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) { + storm::utility::vector::setVectorValues(reducedModelObjRewards, ~epochModel.stepChoices, storm::utility::zero()); } epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } @@ -512,24 +515,27 @@ namespace storm { template template::type> std::string MultiDimensionalRewardUnfolding::solutionToString(SolutionType const& solution) const { - return std::to_string(solution); + std::stringstream stringstream; + stringstream << solution; + return stringstream.str(); } template template::type> std::string MultiDimensionalRewardUnfolding::solutionToString(SolutionType const& solution) const { - std::string res = "("; + std::stringstream stringstream; + stringstream << "("; bool first = true; for (auto const& s : solution) { if (first) { first = false; } else { - res += ", "; + stringstream << ", "; } - res += std::to_string(s); + stringstream << s; } - res += ")"; - return res; + stringstream << ")"; + return stringstream.str(); } template @@ -571,8 +577,11 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getStateSolution(Epoch const& epoch, uint64_t const& productState) { - STORM_LOG_ASSERT(epochSolutions.find(epoch) != epochSolutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << "."); - EpochSolution const& epochSolution = epochSolutions[epoch]; + auto epochSolutionIt = epochSolutions.find(epoch); + STORM_LOG_ASSERT(epochSolutionIt != epochSolutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << "."); + auto const& epochSolution = epochSolutionIt->second; + STORM_LOG_ASSERT(productState < epochSolution.productStateToSolutionVectorMap->size(), "Requested solution for epoch " << epochManager.toString(epoch) << " at an unexisting product state."); + STORM_LOG_ASSERT((*epochSolution.productStateToSolutionVectorMap)[productState] < epochSolution.solutions.size(), "Requested solution for epoch " << epochManager.toString(epoch) << " at a state for which no solution was stored."); return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]]; } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp index 4b415eaec..782b34f03 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp @@ -140,6 +140,7 @@ namespace storm { storm::storage::BitVector consideredDimensions(dimensions.size(), false); do { + // todo: this selects more states then necessary if (consideredDimensions.isSubsetOf(lowerBoundedDimensions)) { for (uint64_t memoryState = 0; memoryState < productBuilder.getMemory().getNumberOfStates(); ++memoryState) { uint64_t memoryStatePrime = convertMemoryState(convertMemoryState(memoryState) | consideredDimensions); @@ -256,7 +257,7 @@ namespace storm { // 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.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) { + if (dimensions[dimensionIndexMap[subObjIndex]].isUpperBounded && epochManager.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) { collectRewardInEpoch = false; break; } @@ -371,7 +372,7 @@ namespace storm { if (dimensions[dim].isUpperBounded && bottomDimensions.get(dim)) { allowedRelevantDimensions.set(dim, false); } else if (!dimensions[dim].isUpperBounded && nonBottomDimensions.get(dim)) { - forcedRelevantDimensions.set(dim, false); + forcedRelevantDimensions.set(dim, true); } } assert(forcedRelevantDimensions.isSubsetOf(allowedRelevantDimensions)); @@ -393,20 +394,31 @@ namespace storm { } } 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; + storm::storage::BitVector predecessorStates = reachableStates.find(predecessor)->second; + for (auto const& predecessorState : predecessorStates) { + storm::storage::BitVector const& predecessorMemStateBv = convertMemoryState(getMemoryState(predecessorState)); + storm::storage::BitVector currentAllowedRelDim = allowedRelevantDimensions; + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (!allowedRelevantDimensions.get(dim) && predecessorMemStateBv.get(dim)) { + currentAllowedRelDim &= ~objectiveDimensions[dimensions[dim].objectiveIndex]; } } - - if (choiceLeadsToThisClass) { - for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) { - uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions); - ecInStates.set(successorState, true); + storm::storage::BitVector currentForcedRelDim = forcedRelevantDimensions & predecessorMemStateBv; + + for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[predecessorState]; choice < getProduct().getTransitionMatrix().getRowGroupIndices()[predecessorState + 1]; ++choice) { + bool choiceLeadsToThisClass = false; + Epoch const& choiceStep = getSteps()[choice]; + for (auto const& dim : positiveStepDimensions) { + if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) { + choiceLeadsToThisClass = true; + } + } + + if (choiceLeadsToThisClass) { + for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) { + uint64_t successorState = transformProductState(transition.getColumn(), currentAllowedRelDim, currentForcedRelDim); + ecInStates.set(successorState, true); + } } } } @@ -420,6 +432,16 @@ namespace storm { uint64_t currentState = dfsStack.back(); dfsStack.pop_back(); + storm::storage::BitVector const& currentMemStateBv = convertMemoryState(getMemoryState(currentState)); + storm::storage::BitVector currentAllowedRelDim = allowedRelevantDimensions; + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (!allowedRelevantDimensions.get(dim) && currentMemStateBv.get(dim)) { + currentAllowedRelDim &= ~objectiveDimensions[dimensions[dim].objectiveIndex]; + } + } + storm::storage::BitVector currentForcedRelDim = forcedRelevantDimensions & currentMemStateBv; + + for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[currentState]; choice != getProduct().getTransitionMatrix().getRowGroupIndices()[currentState + 1]; ++choice) { bool choiceLeadsOutsideOfEpoch = false; @@ -431,7 +453,7 @@ namespace storm { } for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) { - uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions); + uint64_t successorState = transformProductState(transition.getColumn(), currentAllowedRelDim, currentForcedRelDim); if (choiceLeadsOutsideOfEpoch) { ecInStates.set(successorState, true); } @@ -444,29 +466,20 @@ namespace storm { } 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; + return productState; + } else { + storm::storage::BitVector memoryStateBv = (convertMemoryState(getMemoryState(productState)) | forcedRelevantDimensions) & allowedRelevantDimensions; + return getProductState(getModelState(productState), convertMemoryState(memoryStateBv)); } - 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 4c61d2db7..b0663145d 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h @@ -52,7 +52,6 @@ namespace storm { 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;