sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

fixed selection of considered state in reduced model and optimized setting the stepsolutions

tempestpy_adaptions
TimQu 7 years ago
parent
11fc1d29eb
commit
e4ac32a6fc
3 changed files with 97 additions and 60 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  2. 140
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  3. 11
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

6
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
View File

@ -46,7 +46,7 @@ namespace storm {
void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType>::Epoch const& epoch, std::vector<ValueType> const& weightVector) { void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::computeEpochSolution(typename MultiDimensionalRewardUnfolding<ValueType>::Epoch const& epoch, std::vector<ValueType> const& weightVector) {
auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch); auto const& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
swEqBuilding.start(); swEqBuilding.start();
std::vector<typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType> result(epochModel.relevantStates.getNumberOfSetBits());
std::vector<typename MultiDimensionalRewardUnfolding<ValueType>::SolutionType> result(epochModel.inStates.getNumberOfSetBits());
// Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives // 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(); swMinMaxSolving.stop();
swEqBuilding.start(); swEqBuilding.start();
auto resultIt = result.begin(); auto resultIt = result.begin();
for (auto const& state : epochModel.relevantStates) {
for (auto const& state : epochModel.inStates) {
resultIt->weightedValue = x[state]; resultIt->weightedValue = x[state];
++resultIt; ++resultIt;
} }
@ -112,7 +112,7 @@ namespace storm {
swLinEqSolving.stop(); swLinEqSolving.stop();
swEqBuilding.start(); swEqBuilding.start();
auto resultIt = result.begin(); auto resultIt = result.begin();
for (auto const& state : epochModel.relevantStates) {
for (auto const& state : epochModel.inStates) {
resultIt->objectiveValues.push_back(x[state]); resultIt->objectiveValues.push_back(x[state]);
++resultIt; ++resultIt;
} }

140
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -201,6 +201,7 @@ namespace storm {
} }
} }
swAux.start();
// compute the solution for the stepChoices // compute the solution for the stepChoices
epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
auto stepSolIt = epochModel.stepSolutions.begin(); auto stepSolIt = epochModel.stepSolutions.begin();
@ -208,23 +209,30 @@ namespace storm {
uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice]; uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice];
uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice); uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice);
auto relevantDimensions = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState)); auto relevantDimensions = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState));
SolutionType choiceSolution = getZeroSolution();
Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get()); 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 = std::move(choiceSolution);
++stepSolIt; ++stepSolIt;
} }
swAux.stop();
assert(epochModel.objectiveRewards.size() == objectives.size()); assert(epochModel.objectiveRewards.size() == objectives.size());
assert(epochModel.objectiveRewardFilter.size() == objectives.size()); assert(epochModel.objectiveRewardFilter.size() == objectives.size());
@ -254,6 +262,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
void MultiDimensionalRewardUnfolding<ValueType>::setCurrentEpochClass(Epoch const& epoch) { void MultiDimensionalRewardUnfolding<ValueType>::setCurrentEpochClass(Epoch const& epoch) {
// std::cout << "Setting epoch class for epoch " << storm::utility::vector::toString(epoch) << std::endl;
swSetEpochClass.start(); swSetEpochClass.start();
auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch); auto productObjectiveRewards = computeObjectiveRewardsForProduct(epoch);
@ -282,9 +291,11 @@ namespace storm {
storm::storage::BitVector allProductStates(memoryProduct.getProduct().getNumberOfStates(), true); storm::storage::BitVector allProductStates(memoryProduct.getProduct().getNumberOfStates(), true);
// Get the relevant states for this epoch. These are all states // 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 // 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 // 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"); 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.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(); swSetEpochClass.stop();
@ -319,47 +330,72 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
storm::storage::BitVector MultiDimensionalRewardUnfolding<ValueType>::computeRelevantProductStatesForEpochClass(Epoch const& epoch) {
storm::storage::BitVector result(memoryProduct.getProduct().getNumberOfStates(), false);
result.set(*memoryProduct.getProduct().getInitialStates().begin(), true);
storm::storage::BitVector MultiDimensionalRewardUnfolding<ValueType>::computeProductInStatesForEpochClass(Epoch const& epoch) {
storm::storage::SparseMatrix<ValueType> 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<uint_fast64_t> 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; return result;
} }
@ -378,12 +414,12 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void MultiDimensionalRewardUnfolding<ValueType>::setSolutionForCurrentEpoch(std::vector<SolutionType> const& relevantStateSolutions) {
void MultiDimensionalRewardUnfolding<ValueType>::setSolutionForCurrentEpoch(std::vector<SolutionType> const& inStateSolutions) {
swInsertSol.start(); swInsertSol.start();
for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) { for (uint64_t productState = 0; productState < memoryProduct.getProduct().getNumberOfStates(); ++productState) {
uint64_t reducedModelState = ecElimResult.oldToNewStateMapping[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(); swInsertSol.stop();

11
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
View File

@ -36,7 +36,7 @@ namespace storm {
std::vector<SolutionType> stepSolutions; std::vector<SolutionType> stepSolutions;
std::vector<std::vector<ValueType>> objectiveRewards; std::vector<std::vector<ValueType>> objectiveRewards;
std::vector<storm::storage::BitVector> objectiveRewardFilter; std::vector<storm::storage::BitVector> objectiveRewardFilter;
storm::storage::BitVector relevantStates;
storm::storage::BitVector inStates;
}; };
/* /*
@ -59,8 +59,9 @@ namespace storm {
std::cout << " setEpochClass: " << swSetEpochClass << " seconds." << std::endl; std::cout << " setEpochClass: " << swSetEpochClass << " seconds." << std::endl;
std::cout << " findSolutions: " << swFindSol << " seconds." << std::endl; std::cout << " findSolutions: " << swFindSol << " seconds." << std::endl;
std::cout << " insertSolutions: " << swInsertSol << " seconds." << std::endl; std::cout << " insertSolutions: " << swInsertSol << " seconds." << std::endl;
std::cout << " auxStopWatch: " << swAux << " seconds." << std::endl;
std::cout << "---------------------------------------------" << 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: "; std::cout << " Epoch model sizes: ";
for (auto const& i : epochModelSizes) { for (auto const& i : epochModelSizes) {
std::cout << i << " "; std::cout << i << " ";
@ -76,7 +77,7 @@ namespace storm {
EpochModel const& setCurrentEpoch(Epoch const& epoch); EpochModel const& setCurrentEpoch(Epoch const& epoch);
void setSolutionForCurrentEpoch(std::vector<SolutionType> const& relevantStateSolutions);
void setSolutionForCurrentEpoch(std::vector<SolutionType> const& inStateSolutions);
SolutionType const& getInitialStateResult(Epoch const& epoch); SolutionType const& getInitialStateResult(Epoch const& epoch);
@ -117,7 +118,7 @@ namespace storm {
}; };
void setCurrentEpochClass(Epoch const& epoch); void setCurrentEpochClass(Epoch const& epoch);
storm::storage::BitVector computeRelevantProductStatesForEpochClass(Epoch const& epoch);
storm::storage::BitVector computeProductInStatesForEpochClass(Epoch const& epoch);
void initialize(); void initialize();
@ -161,7 +162,7 @@ namespace storm {
std::map<std::vector<int64_t>, SolutionType> solutions; std::map<std::vector<int64_t>, SolutionType> solutions;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux;
std::vector<uint64_t> epochModelSizes; std::vector<uint64_t> epochModelSizes;
}; };
} }

Write Preview
Loading…
Cancel
Save