From e4ac32a6fce5abd60ef6f72b7e97216006b2e8e2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 6 Sep 2017 17:54:53 +0200 Subject: [PATCH] fixed selection of considered state in reduced model and optimized setting the stepsolutions --- ...dpRewardBoundedPcaaWeightVectorChecker.cpp | 6 +- .../MultiDimensionalRewardUnfolding.cpp | 140 +++++++++++------- .../MultiDimensionalRewardUnfolding.h | 11 +- 3 files changed, 97 insertions(+), 60 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 2170ad0f2..ca67b9a9f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -46,7 +46,7 @@ namespace storm { 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.relevantStates.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 @@ -79,7 +79,7 @@ namespace storm { swMinMaxSolving.stop(); swEqBuilding.start(); auto resultIt = result.begin(); - for (auto const& state : epochModel.relevantStates) { + for (auto const& state : epochModel.inStates) { resultIt->weightedValue = x[state]; ++resultIt; } @@ -112,7 +112,7 @@ namespace storm { swLinEqSolving.stop(); swEqBuilding.start(); auto resultIt = result.begin(); - for (auto const& state : epochModel.relevantStates) { + for (auto const& state : epochModel.inStates) { resultIt->objectiveValues.push_back(x[state]); ++resultIt; } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 18c53b5af..49223642d 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -201,6 +201,7 @@ namespace storm { } } + swAux.start(); // compute the solution for the stepChoices epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); auto stepSolIt = epochModel.stepSolutions.begin(); @@ -208,23 +209,30 @@ namespace storm { uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice]; uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice); auto relevantDimensions = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState)); - SolutionType choiceSolution = getZeroSolution(); Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get()); - storm::storage::BitVector successorRelevantDimensions(successorEpoch.size(), true); - for (auto const& dim : relevantDimensions) { - if (successorEpoch[dim] < 0) { - successorRelevantDimensions &= ~objectiveDimensions[subObjectives[dim].second]; + SolutionType choiceSolution = getZeroSolution(); + if (getClassOfEpoch(epoch) == getClassOfEpoch(successorEpoch)) { + for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) { + addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue()); + } + } else { + storm::storage::BitVector successorRelevantDimensions(successorEpoch.size(), true); + for (auto const& dim : relevantDimensions) { + if (successorEpoch[dim] < 0) { + 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)); + SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); + addScaledSolution(choiceSolution, successorSolution, successor.getValue()); } - } - 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)); - SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState); - addScaledSolution(choiceSolution, successorSolution, successor.getValue()); } *stepSolIt = std::move(choiceSolution); ++stepSolIt; } + swAux.stop(); assert(epochModel.objectiveRewards.size() == objectives.size()); assert(epochModel.objectiveRewardFilter.size() == objectives.size()); @@ -254,6 +262,7 @@ namespace storm { 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); @@ -282,9 +291,11 @@ namespace storm { storm::storage::BitVector allProductStates(memoryProduct.getProduct().getNumberOfStates(), true); // Get the relevant states for this epoch. These are all states - storm::storage::BitVector productRelevantStates = computeRelevantProductStatesForEpochClass(epoch); + storm::storage::BitVector productInStates = computeProductInStatesForEpochClass(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, productRelevantStates, allProductStates, ~allProductStates); + storm::storage::BitVector consideredStates = storm::utility::graph::getReachableStates(epochModel.epochMatrix, productInStates, allProductStates, ~allProductStates); + // std::cout << "numInStates = " << productInStates.getNumberOfSetBits() << std::endl; + // std::cout << "numConsideredStates = " << consideredStates.getNumberOfSetBits() << std::endl; // We assume that there is no end component in which objective reward is earned STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix, epochModel.epochMatrix.transpose(true), allProductStates, ~zeroObjRewardChoices & ~stepChoices), "There is a scheduler that yields infinite reward for one objective. This case should be excluded"); @@ -309,9 +320,9 @@ namespace storm { epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards)); } - epochModel.relevantStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); - for (auto const& productState : productRelevantStates) { - epochModel.relevantStates.set(ecElimResult.oldToNewStateMapping[productState], true); + epochModel.inStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); + for (auto const& productState : productInStates) { + epochModel.inStates.set(ecElimResult.oldToNewStateMapping[productState], true); } swSetEpochClass.stop(); @@ -319,47 +330,72 @@ namespace storm { } template - storm::storage::BitVector MultiDimensionalRewardUnfolding::computeRelevantProductStatesForEpochClass(Epoch const& epoch) { - storm::storage::BitVector result(memoryProduct.getProduct().getNumberOfStates(), false); - result.set(*memoryProduct.getProduct().getInitialStates().begin(), true); + storm::storage::BitVector MultiDimensionalRewardUnfolding::computeProductInStatesForEpochClass(Epoch const& epoch) { + storm::storage::SparseMatrix const& productMatrix = memoryProduct.getProduct().getTransitionMatrix(); - for (uint64_t choice = 0; choice < memoryProduct.getProduct().getNumberOfChoices(); ++choice) { - auto const& choiceStep = memoryProduct.getSteps()[choice]; - if (choiceStep) { - storm::storage::BitVector objectiveSet(objectives.size(), false); - for (uint64_t dim = 0; dim < epoch.size(); ++dim) { - if (epoch[dim] < 0 && choiceStep.get()[dim] > 0) { - objectiveSet.set(subObjectives[dim].second); - } - } - - if (objectiveSet.empty()) { - for (auto const& choiceSuccessor : memoryProduct.getProduct().getTransitionMatrix().getRow(choice)) { - result.set(choiceSuccessor.getColumn(), true); + storm::storage::BitVector result(productMatrix.getRowGroupCount(), false); + result.set(*memoryProduct.getProduct().getInitialStates().begin(), true); + // Perform DFS + storm::storage::BitVector reachableStates = result; + 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 (choiceStep) { + storm::storage::BitVector objectiveSet(objectives.size(), false); + for (uint64_t dim = 0; dim < epoch.size(); ++dim) { + if (epoch[dim] < 0 && choiceStep.get()[dim] > 0) { + objectiveSet.set(subObjectives[dim].second); + } } - } else { - storm::storage::BitVector objectiveSubSet(objectiveSet.getNumberOfSetBits(), false); - do { - for (auto const& choiceSuccessor : memoryProduct.getProduct().getTransitionMatrix().getRow(choice)) { - uint64_t modelState = memoryProduct.getModelState(choiceSuccessor.getColumn()); - uint64_t memoryState = memoryProduct.getMemoryState(choiceSuccessor.getColumn()); - storm::storage::BitVector memoryStatePrimeBv = memoryProduct.convertMemoryState(memoryState); - uint64_t i = 0; - for (auto const& objIndex : objectiveSet) { - if (objectiveSubSet.get(i)) { - memoryStatePrimeBv &= ~objectiveDimensions[objIndex]; + + if (objectiveSet.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 { + storm::storage::BitVector objectiveSubSet(objectiveSet.getNumberOfSetBits(), false); + do { + for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { + uint64_t modelState = memoryProduct.getModelState(choiceSuccessor.getColumn()); + uint64_t memoryState = memoryProduct.getMemoryState(choiceSuccessor.getColumn()); + storm::storage::BitVector memoryStatePrimeBv = memoryProduct.convertMemoryState(memoryState); + uint64_t i = 0; + for (auto const& objIndex : objectiveSet) { + if (objectiveSubSet.get(i)) { + memoryStatePrimeBv &= ~objectiveDimensions[objIndex]; + } + ++i; + } + uint64_t successorState = memoryProduct.getProductState(modelState, memoryProduct.convertMemoryState(memoryStatePrimeBv)); + result.set(successorState, true); + if (!reachableStates.get(successorState)) { + reachableStates.set(successorState); + stack.push_back(successorState); } - ++i; } - result.set(memoryProduct.getProductState(modelState, memoryProduct.convertMemoryState(memoryStatePrimeBv)), true); + + objectiveSubSet.increment(); + } while (!objectiveSubSet.empty()); + } + } else { + for (auto const& choiceSuccessor : productMatrix.getRow(choice)) { + if (!reachableStates.get(choiceSuccessor.getColumn())) { + reachableStates.set(choiceSuccessor.getColumn()); + stack.push_back(choiceSuccessor.getColumn()); } - - objectiveSubSet.increment(); - } while (!objectiveSubSet.empty()); + } } } } - return result; } @@ -378,12 +414,12 @@ namespace storm { } template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector const& relevantStateSolutions) { + 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]; - if (reducedModelState < epochModel.epochMatrix.getRowGroupCount() && epochModel.relevantStates.get(reducedModelState)) { - setSolutionForCurrentEpoch(productState, relevantStateSolutions[epochModel.relevantStates.getNumberOfSetBitsBeforeIndex(reducedModelState)]); + if (reducedModelState < epochModel.epochMatrix.getRowGroupCount() && epochModel.inStates.get(reducedModelState)) { + setSolutionForCurrentEpoch(productState, inStateSolutions[epochModel.inStates.getNumberOfSetBitsBeforeIndex(reducedModelState)]); } } swInsertSol.stop(); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 3e5d4924f..1932338d7 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -36,7 +36,7 @@ namespace storm { std::vector stepSolutions; std::vector> objectiveRewards; std::vector objectiveRewardFilter; - storm::storage::BitVector relevantStates; + storm::storage::BitVector inStates; }; /* @@ -59,8 +59,9 @@ namespace storm { std::cout << " setEpochClass: " << swSetEpochClass << " seconds." << std::endl; std::cout << " findSolutions: " << swFindSol << " seconds." << std::endl; std::cout << " insertSolutions: " << swInsertSol << " seconds." << std::endl; + std::cout << " auxStopWatch: " << swAux << " seconds." << std::endl; std::cout << "---------------------------------------------" << std::endl; - std::cout << " Product size: " << memoryProduct.getProduct().getNumberOfStates(); + std::cout << " Product size: " << memoryProduct.getProduct().getNumberOfStates() << std::endl; std::cout << " Epoch model sizes: "; for (auto const& i : epochModelSizes) { std::cout << i << " "; @@ -76,7 +77,7 @@ namespace storm { EpochModel const& setCurrentEpoch(Epoch const& epoch); - void setSolutionForCurrentEpoch(std::vector const& relevantStateSolutions); + void setSolutionForCurrentEpoch(std::vector const& inStateSolutions); SolutionType const& getInitialStateResult(Epoch const& epoch); @@ -117,7 +118,7 @@ namespace storm { }; void setCurrentEpochClass(Epoch const& epoch); - storm::storage::BitVector computeRelevantProductStatesForEpochClass(Epoch const& epoch); + storm::storage::BitVector computeProductInStatesForEpochClass(Epoch const& epoch); void initialize(); @@ -161,7 +162,7 @@ namespace storm { std::map, SolutionType> solutions; - storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass; + storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux; std::vector epochModelSizes; }; }