diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index ca67b9a9f..a1784bea8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -43,10 +43,10 @@ namespace storm { } template - void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector) { + void SparseMdpRewardBoundedPcaaWeightVectorChecker::computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector) { auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch); swEqBuilding.start(); - std::vector::SolutionType> result(epochModel.inStates.getNumberOfSetBits()); + std::vector::SolutionType> result(epochModel.inStates.getNumberOfSetBits()); // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h index db507cc68..5f05fd242 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.h @@ -55,11 +55,11 @@ namespace storm { private: - void computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector); + void computeEpochSolution(typename MultiDimensionalRewardUnfolding::Epoch const& epoch, std::vector const& weightVector); storm::utility::Stopwatch swAll, swEqBuilding, swLinEqSolving, swMinMaxSolving; - MultiDimensionalRewardUnfolding rewardUnfolding; + MultiDimensionalRewardUnfolding rewardUnfolding; boost::optional> underApproxResult; boost::optional> overApproxResult; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index e42fa24a9..629c73a6f 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -18,15 +18,15 @@ namespace storm { namespace modelchecker { namespace multiobjective { - template - MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& allowedBottomStates) : model(model), objectives(objectives), possibleECActions(possibleECActions), allowedBottomStates(allowedBottomStates) { + template + MultiDimensionalRewardUnfolding::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& allowedBottomStates) : model(model), objectives(objectives), possibleECActions(possibleECActions), allowedBottomStates(allowedBottomStates) { initialize(); } - template - void MultiDimensionalRewardUnfolding::initialize() { + template + void MultiDimensionalRewardUnfolding::initialize() { swInit.start(); std::vector> epochSteps; initializeObjectives(epochSteps); @@ -35,8 +35,8 @@ namespace storm { swInit.stop(); } - template - void MultiDimensionalRewardUnfolding::initializeObjectives(std::vector>& epochSteps) { + template + void MultiDimensionalRewardUnfolding::initializeObjectives(std::vector>& epochSteps) { // collect the time-bounded subobjectives for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { @@ -96,8 +96,8 @@ namespace storm { } } - template - void MultiDimensionalRewardUnfolding::initializePossibleEpochSteps(std::vector> const& epochSteps) { + template + void MultiDimensionalRewardUnfolding::initializePossibleEpochSteps(std::vector> const& epochSteps) { // collect which epoch steps are possible possibleEpochSteps.clear(); for (uint64_t choiceIndex = 0; choiceIndex < epochSteps.front().size(); ++choiceIndex) { @@ -110,8 +110,8 @@ namespace storm { } } - template - void MultiDimensionalRewardUnfolding::initializeMemoryProduct(std::vector> const& epochSteps) { + template + void MultiDimensionalRewardUnfolding::initializeMemoryProduct(std::vector> const& epochSteps) { // build the memory structure auto memoryStructure = computeMemoryStructure(); @@ -123,8 +123,8 @@ namespace storm { } - template - typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getStartEpoch() { + template + typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getStartEpoch() { Epoch startEpoch; for (uint64_t dim = 0; dim < this->subObjectives.size(); ++dim) { storm::expressions::Expression bound; @@ -153,8 +153,8 @@ namespace storm { return startEpoch; } - template - std::vector::Epoch> MultiDimensionalRewardUnfolding::getEpochComputationOrder(Epoch const& startEpoch) { + template + std::vector::Epoch> MultiDimensionalRewardUnfolding::getEpochComputationOrder(Epoch const& startEpoch) { // perform DFS to get the 'reachable' epochs in the correct order. std::vector result, dfsStack; @@ -180,8 +180,8 @@ namespace storm { return result; } - template - typename MultiDimensionalRewardUnfolding::EpochModel const& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { + template + typename MultiDimensionalRewardUnfolding::EpochModel const& MultiDimensionalRewardUnfolding::setCurrentEpoch(Epoch const& epoch) { // Check if we need to update the current epoch class if (!currentEpoch || getClassOfEpoch(epoch) != getClassOfEpoch(currentEpoch.get())) { setCurrentEpochClass(epoch); @@ -208,11 +208,17 @@ namespace storm { // compute the solution for the stepChoices swAux2.start(); - SolutionType choiceSolution = getZeroSolution(); + SolutionType choiceSolution; + bool firstSuccessor = true; if (getClassOfEpoch(epoch) == getClassOfEpoch(successorEpoch)) { swAux3.start(); for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) { - addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); + if (firstSuccessor) { + choiceSolution = getScaledSolution(getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); + firstSuccessor = false; + } else { + addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); + } } swAux3.stop(); } else { @@ -227,7 +233,12 @@ namespace storm { storm::storage::BitVector successorMemoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(successor.getColumn())) & successorRelevantDimensions; uint64_t successorProductState = memoryProduct.getProductState(memoryProduct.getModelState(successor.getColumn()), memoryProduct.convertMemoryState(successorMemoryState)); SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); - addScaledSolution(choiceSolution, successorSolution, successor.getValue()); + if (firstSuccessor) { + choiceSolution = getScaledSolution(successorSolution, successor.getValue()); + firstSuccessor = false; + } else { + addScaledSolution(choiceSolution, successorSolution, successor.getValue()); + } } swAux4.stop(); } @@ -262,8 +273,8 @@ namespace storm { } - template - void MultiDimensionalRewardUnfolding::setCurrentEpochClass(Epoch const& epoch) { + template + void MultiDimensionalRewardUnfolding::setCurrentEpochClass(Epoch const& epoch) { // std::cout << "Setting epoch class for epoch " << storm::utility::vector::toString(epoch) << std::endl; swSetEpochClass.start(); auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch); @@ -331,8 +342,8 @@ namespace storm { epochModelSizes.push_back(epochModel.epochMatrix.getRowGroupCount()); } - template - storm::storage::BitVector MultiDimensionalRewardUnfolding::computeProductInStatesForEpochClass(Epoch const& epoch) { + template + storm::storage::BitVector MultiDimensionalRewardUnfolding::computeProductInStatesForEpochClass(Epoch const& epoch) { storm::storage::SparseMatrix const& productMatrix = memoryProduct.getProduct().getTransitionMatrix(); storm::storage::BitVector result(productMatrix.getRowGroupCount(), false); @@ -401,22 +412,39 @@ namespace storm { return result; } - template - typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getZeroSolution() const { + template + template::type> + typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { + //return solution * scalingFactor; + } + + template + template::type> + typename MultiDimensionalRewardUnfolding::SolutionType MultiDimensionalRewardUnfolding::getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const { SolutionType res; - res.weightedValue = storm::utility::zero(); - res.objectiveValues = std::vector(objectives.size(), storm::utility::zero()); + res.weightedValue = solution.weightedValue * scalingFactor; + res.objectiveValues.reserve(solution.objectiveValues.size()); + for (auto const& sol : solution.objectiveValues) { + res.objectiveValues.push_back(sol * scalingFactor); + } return res; } - template - void MultiDimensionalRewardUnfolding::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const { + template + template::type> + void MultiDimensionalRewardUnfolding::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const { + // solution += solutionToAdd * scalingFactor; + } + + template + template::type> + void MultiDimensionalRewardUnfolding::addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const { solution.weightedValue += solutionToAdd.weightedValue * scalingFactor; storm::utility::vector::addScaledVector(solution.objectiveValues, solutionToAdd.objectiveValues, scalingFactor); } - template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& inStateSolutions) { + template + void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& inStateSolutions) { swInsertSol.start(); for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) { uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[productState]; @@ -427,16 +455,16 @@ namespace storm { swInsertSol.stop(); } - template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution) { + template + void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution) { STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before."); std::vector solutionKey = currentEpoch.get(); solutionKey.push_back(productState); solutions[solutionKey] = solution; } - template - typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getStateSolution(Epoch const& epoch, uint64_t const& productState) { + template + typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getStateSolution(Epoch const& epoch, uint64_t const& productState) { swFindSol.start(); std::vector solutionKey = epoch; solutionKey.push_back(productState); @@ -446,14 +474,14 @@ namespace storm { return solutionIt->second; } - template - typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { + template + typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { return getStateSolution(epoch, *memoryProduct.getProduct().getInitialStates().begin()); } - template - storm::storage::MemoryStructure MultiDimensionalRewardUnfolding::computeMemoryStructure() const { + template + storm::storage::MemoryStructure MultiDimensionalRewardUnfolding::computeMemoryStructure() const { storm::modelchecker::SparsePropositionalModelChecker> mc(model); @@ -542,8 +570,8 @@ namespace storm { return memory; } - template - std::vector MultiDimensionalRewardUnfolding::computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const { + template + std::vector MultiDimensionalRewardUnfolding::computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const { // Compute a mapping between the different representations of memory states std::vector result; result.reserve(memory.getNumberOfStates()); @@ -560,8 +588,8 @@ 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)) { + 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); @@ -621,8 +649,8 @@ namespace storm { } } - template - void MultiDimensionalRewardUnfolding::MemoryProduct::setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector> const& originalModelSteps, std::vector const& objectiveDimensions) const { + template + void MultiDimensionalRewardUnfolding::MemoryProduct::setReachableStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector> const& originalModelSteps, std::vector const& objectiveDimensions) 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]; @@ -668,56 +696,56 @@ namespace storm { } } - template - storm::models::sparse::Mdp const& MultiDimensionalRewardUnfolding::MemoryProduct::getProduct() const { + template + storm::models::sparse::Mdp const& MultiDimensionalRewardUnfolding::MemoryProduct::getProduct() const { return *product; } - template - std::vector::Epoch>> const& MultiDimensionalRewardUnfolding::MemoryProduct::getSteps() const { + 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 { + 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 { + 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 { + 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 { + 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 { + template + storm::storage::BitVector const& MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(uint64_t const& memoryState) const { return memoryStateMap[memoryState]; } - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(storm::storage::BitVector const& memoryState) const { + template + uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::convertMemoryState(storm::storage::BitVector const& memoryState) const { auto memStateIt = std::find(memoryStateMap.begin(), memoryStateMap.end(), memoryState); return memStateIt - memoryStateMap.begin(); } - template - uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getProductStateFromChoice(uint64_t const& productChoice) const { + template + uint64_t MultiDimensionalRewardUnfolding::MemoryProduct::getProductStateFromChoice(uint64_t const& productChoice) const { return choiceToStateMap[productChoice]; } - template - std::vector> MultiDimensionalRewardUnfolding::computeObjectiveRewardsForProduct(Epoch const& epoch) const { + template + std::vector> MultiDimensionalRewardUnfolding::computeObjectiveRewardsForProduct(Epoch const& epoch) const { std::vector> objectiveRewards; objectiveRewards.reserve(objectives.size()); @@ -808,8 +836,8 @@ namespace storm { return objectiveRewards; } - template - typename MultiDimensionalRewardUnfolding::EpochClass MultiDimensionalRewardUnfolding::getClassOfEpoch(Epoch const& epoch) const { + template + typename MultiDimensionalRewardUnfolding::EpochClass MultiDimensionalRewardUnfolding::getClassOfEpoch(Epoch const& epoch) const { // Get a BitVector that is 1 wherever the epoch is non-negative storm::storage::BitVector classAsBitVector(epoch.size(), false); uint64_t i = 0; @@ -822,8 +850,8 @@ namespace storm { return classAsBitVector.getAsInt(0, epoch.size()); } - template - typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const { + template + typename MultiDimensionalRewardUnfolding::Epoch MultiDimensionalRewardUnfolding::getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const { assert(epoch.size() == step.size()); Epoch result; result.reserve(epoch.size()); @@ -836,8 +864,10 @@ namespace storm { } - template class MultiDimensionalRewardUnfolding; - template class MultiDimensionalRewardUnfolding; + template class MultiDimensionalRewardUnfolding; + 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 33297feab..1b003d703 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -18,13 +18,15 @@ namespace storm { namespace multiobjective { - template + template class MultiDimensionalRewardUnfolding { public: typedef std::vector Epoch; // The number of reward steps that are "left" for each dimension typedef uint64_t EpochClass; // Collection of epochs that consider the same epoch model +// typedef typename std::conditional>::type; SolutionType + struct SolutionType { ValueType weightedValue; std::vector objectiveValues; @@ -137,7 +139,15 @@ namespace storm { EpochClass getClassOfEpoch(Epoch const& epoch) const; Epoch getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const; - SolutionType getZeroSolution() const; + + template::type = 0> + SolutionType getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const; + template::type = 0> + SolutionType getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const; + + template::type = 0> + void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const; + template::type = 0> void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const; void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution);