diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/Dimension.h b/src/storm/modelchecker/multiobjective/rewardbounded/Dimension.h index 3d43d22eb..6f5a9cebb 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/Dimension.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/Dimension.h @@ -23,6 +23,7 @@ namespace storm { boost::optional memoryLabel; bool isUpperBounded; ValueType scalingFactor; + storm::storage::BitVector dependentDimensions; boost::optional maxValue; }; } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 0c18046af..c09ee91f5 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -112,15 +112,37 @@ namespace storm { } // Compute a mapping for each objective to the set of dimensions it considers + // Also store for each dimension dim, which dimensions should be unsatisfiable whenever the bound of dim is violated + uint64_t dim = 0; for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { storm::storage::BitVector objDimensions(dimensions.size(), false); - for (uint64_t dim = 0; dim < dimensions.size(); ++dim) { - if (dimensions[dim].objectiveIndex == objIndex) { - objDimensions.set(dim, true); + if (objectives[objIndex].formula->isProbabilityOperatorFormula() && objectives[objIndex].formula->getSubformula().isBoundedUntilFormula()) { + auto const& boundedUntilFormula = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula(); + for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) { + objDimensions.set(currDim); } + for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) { + if (!boundedUntilFormula.hasMultiDimensionalSubformulas() || dimensions[currDim].isUpperBounded) { + dimensions[currDim].dependentDimensions = objDimensions; + std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl; + } else { + dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false); + dimensions[currDim].dependentDimensions.set(currDim, true); + std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl; + } + } + dim += boundedUntilFormula.getDimension(); + } else if (objectives[objIndex].formula->isRewardOperatorFormula() && objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) { + objDimensions.set(dim, true); + dimensions[dim].dependentDimensions = objDimensions; + ++dim; } + + std::cout << "obj " << objIndex << " has dimensions " << objDimensions << std::endl; objectiveDimensions.push_back(std::move(objDimensions)); } + assert(dim == dimensions.size()); + // Initialize the epoch manager epochManager = EpochManager(dimensions.size()); @@ -143,6 +165,9 @@ namespace storm { possibleEpochSteps.insert(step); } + // Set the maximal values we need to consider for each dimension + computeMaxDimensionValues(); + } template @@ -158,8 +183,7 @@ namespace storm { } template - typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getStartEpoch() { - Epoch startEpoch; + void MultiDimensionalRewardUnfolding::computeMaxDimensionValues() { for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { storm::expressions::Expression bound; bool isStrict = false; @@ -191,7 +215,16 @@ namespace storm { } uint64_t dimensionValue = storm::utility::convertNumber(discretizedBound); STORM_LOG_THROW(epochManager.isValidDimensionValue(dimensionValue), storm::exceptions::NotSupportedException, "The bound " << bound << " is too high for the considered number of dimensions."); - epochManager.setDimensionOfEpoch(startEpoch, dim, dimensionValue); + dimensions[dim].maxValue = dimensionValue; + } + } + + template + typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getStartEpoch() { + Epoch startEpoch = epochManager.getZeroEpoch(); + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + STORM_LOG_ASSERT(dimensions[dim].maxValue, "No max-value for dimension " << dim << " was given."); + epochManager.setDimensionOfEpoch(startEpoch, dim, dimensions[dim].maxValue.get()); } STORM_LOG_TRACE("Start epoch is " << epochManager.toString(startEpoch)); return startEpoch; @@ -234,32 +267,6 @@ namespace storm { std::cout << std::endl; */ return std::vector(collectedEpochs.begin(), collectedEpochs.end()); - - /* - - // perform DFS to get the 'reachable' epochs in the correct order. - std::vector result, dfsStack; - std::set seenEpochs; - seenEpochs.insert(startEpoch); - dfsStack.push_back(startEpoch); - while (!dfsStack.empty()) { - bool hasUnseenSuccessor = false; - for (auto const& step : possibleEpochSteps) { - Epoch successorEpoch = epochManager.getSuccessorEpoch(dfsStack.back(), step); - if (seenEpochs.find(successorEpoch) == seenEpochs.end()) { - seenEpochs.insert(successorEpoch); - dfsStack.push_back(std::move(successorEpoch)); - hasUnseenSuccessor = true; - } - } - if (!hasUnseenSuccessor) { - result.push_back(std::move(dfsStack.back())); - dfsStack.pop_back(); - } - } - - return result; - */ } template @@ -291,7 +298,7 @@ namespace storm { auto const& memoryState = productModel->getMemoryState(productState); auto const& memoryStateBv = productModel->convertMemoryState(memoryState); Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, productModel->getSteps()[productChoice]); - + EpochClass successorEpochClass = epochManager.getEpochClass(successorEpoch); // Find out whether objective reward is earned for the current 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 @@ -323,7 +330,7 @@ namespace storm { } } else { for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { - uint64_t successorProductState = productModel->transformProductState(successor.getColumn(), epochManager.getEpochClass(successorEpoch), memoryState); + uint64_t successorProductState = productModel->transformProductState(successor.getColumn(), successorEpochClass, memoryState); SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); if (firstSuccessor) { choiceSolution = getScaledSolution(successorSolution, successor.getValue()); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index f37c09e71..377a99a9b 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -86,6 +86,8 @@ namespace storm { void initialize(); void initializeObjectives(std::vector& epochSteps); + void computeMaxDimensionValues(); + void initializeMemoryProduct(std::vector const& epochSteps); storm::storage::MemoryStructure computeMemoryStructure() const;