Browse Source

optimized setCurrentEpoch a little

tempestpy_adaptions
TimQu 7 years ago
parent
commit
57e604a815
  1. 32
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  2. 7
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

32
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp

@ -188,36 +188,37 @@ namespace storm {
}
swSetEpoch.start();
// Find out which objective rewards are earned in this particular epoch
epochModel.objectiveRewardFilter = std::vector<storm::storage::BitVector>(objectives.size(), storm::storage::BitVector(epochModel.objectiveRewards.front().size(), true));
epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
auto stepSolIt = epochModel.stepSolutions.begin();
for (auto const& reducedChoice : epochModel.stepChoices) {
uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice];
storm::storage::BitVector memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(memoryProduct.getProductStateFromChoice(productChoice)));
uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice);
auto memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState));
Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get());
// Find out whether objective reward is earned for the current choice
swAux1.start();
for (uint64_t dim = 0; dim < successorEpoch.size(); ++dim) {
if (successorEpoch[dim] < 0 && memoryState.get(dim)) {
epochModel.objectiveRewardFilter[subObjectives[dim].second].set(reducedChoice, false);
}
}
}
swAux.start();
// compute the solution for the stepChoices
epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
auto stepSolIt = epochModel.stepSolutions.begin();
for (auto const& reducedChoice : epochModel.stepChoices) {
uint64_t productChoice = ecElimResult.newToOldRowMapping[reducedChoice];
uint64_t productState = memoryProduct.getProductStateFromChoice(productChoice);
auto relevantDimensions = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState));
Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get());
swAux1.stop();
// compute the solution for the stepChoices
swAux2.start();
SolutionType choiceSolution = getZeroSolution();
if (getClassOfEpoch(epoch) == getClassOfEpoch(successorEpoch)) {
swAux3.start();
for (auto const& successor : memoryProduct.getProduct().getTransitionMatrix().getRow(productChoice)) {
addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue());
}
swAux3.stop();
} else {
swAux4.start();
storm::storage::BitVector successorRelevantDimensions(successorEpoch.size(), true);
for (auto const& dim : relevantDimensions) {
for (auto const& dim : memoryState) {
if (successorEpoch[dim] < 0) {
successorRelevantDimensions &= ~objectiveDimensions[subObjectives[dim].second];
}
@ -228,11 +229,12 @@ namespace storm {
SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState);
addScaledSolution(choiceSolution, successorSolution, successor.getValue());
}
swAux4.stop();
}
swAux2.stop();
*stepSolIt = std::move(choiceSolution);
++stepSolIt;
}
swAux.stop();
assert(epochModel.objectiveRewards.size() == objectives.size());
assert(epochModel.objectiveRewardFilter.size() == objectives.size());

7
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

@ -59,7 +59,10 @@ 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 << " aux1StopWatch: " << swAux1 << " seconds." << std::endl;
std::cout << " aux2StopWatch: " << swAux2 << " seconds." << std::endl;
std::cout << " aux3StopWatch: " << swAux3 << " seconds." << std::endl;
std::cout << " aux4StopWatch: " << swAux4 << " seconds." << std::endl;
std::cout << "---------------------------------------------" << std::endl;
std::cout << " Product size: " << memoryProduct.getProduct().getNumberOfStates() << std::endl;
std::cout << " Epoch model sizes: ";
@ -162,7 +165,7 @@ namespace storm {
std::map<std::vector<int64_t>, SolutionType> solutions;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4;
std::vector<uint64_t> epochModelSizes;
};
}

Loading…
Cancel
Save