Browse Source

Consider only a submap of all epochsolutions for faster search

tempestpy_adaptions
TimQu 7 years ago
parent
commit
b56cd07d0e
  1. 26
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  2. 14
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

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

@ -296,7 +296,15 @@ namespace storm {
break; break;
} }
} }
std::map<Epoch, EpochSolution const*> subSolutions;
for (auto const& step : possibleEpochSteps) {
Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, step);
if (successorEpoch != epoch) {
auto successorSolIt = epochSolutions.find(successorEpoch);
STORM_LOG_ASSERT(successorSolIt != epochSolutions.end(), "Solution for successor epoch does not exist (anymore).");
subSolutions.emplace(successorEpoch, &successorSolIt->second);
}
}
epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits()); epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
auto stepSolIt = epochModel.stepSolutions.begin(); auto stepSolIt = epochModel.stepSolutions.begin();
for (auto const& reducedChoice : epochModel.stepChoices) { for (auto const& reducedChoice : epochModel.stepChoices) {
@ -328,16 +336,16 @@ namespace storm {
if (!containsLowerBoundedObjective && epochManager.compareEpochClass(epoch, successorEpoch)) { if (!containsLowerBoundedObjective && epochManager.compareEpochClass(epoch, successorEpoch)) {
for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
if (firstSuccessor) { if (firstSuccessor) {
choiceSolution = getScaledSolution(getStateSolution(successorEpoch, successor.getColumn()), successor.getValue());
choiceSolution = getScaledSolution(getStateSolution(subSolutions, successorEpoch, successor.getColumn()), successor.getValue());
firstSuccessor = false; firstSuccessor = false;
} else { } else {
addScaledSolution(choiceSolution, getStateSolution(successorEpoch, successor.getColumn()), successor.getValue());
addScaledSolution(choiceSolution, getStateSolution(subSolutions, successorEpoch, successor.getColumn()), successor.getValue());
} }
} }
} else { } else {
for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) { for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
uint64_t successorProductState = productModel->transformProductState(successor.getColumn(), successorEpochClass, memoryState); uint64_t successorProductState = productModel->transformProductState(successor.getColumn(), successorEpochClass, memoryState);
SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState);
SolutionType const& successorSolution = getStateSolution(subSolutions, successorEpoch, successorProductState);
if (firstSuccessor) { if (firstSuccessor) {
choiceSolution = getScaledSolution(successorSolution, successor.getValue()); choiceSolution = getScaledSolution(successorSolution, successor.getValue());
firstSuccessor = false; firstSuccessor = false;
@ -573,6 +581,16 @@ namespace storm {
return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]]; return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]];
} }
template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(std::map<Epoch, EpochSolution const*> const& solutions, Epoch const& epoch, uint64_t const& productState) {
auto epochSolutionIt = solutions.find(epoch);
STORM_LOG_ASSERT(epochSolutionIt != solutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
auto const& epochSolution = *epochSolutionIt->second;
STORM_LOG_ASSERT(productState < epochSolution.productStateToSolutionVectorMap->size(), "Requested solution for epoch " << epochManager.toString(epoch) << " at an unexisting product state.");
STORM_LOG_ASSERT((*epochSolution.productStateToSolutionVectorMap)[productState] < epochSolution.solutions.size(), "Requested solution for epoch " << epochManager.toString(epoch) << " at a state for which no solution was stored.");
return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]];
}
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getInitialStateResult(Epoch const& epoch) { typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getInitialStateResult(Epoch const& epoch) {
STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states."); STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states.");

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

@ -99,6 +99,13 @@ namespace storm {
std::string solutionToString(SolutionType const& solution) const; std::string solutionToString(SolutionType const& solution) const;
SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState); SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState);
struct EpochSolution {
uint64_t count;
std::shared_ptr<std::vector<uint64_t> const> productStateToSolutionVectorMap;
std::vector<SolutionType> solutions;
};
std::map<Epoch, EpochSolution> epochSolutions;
SolutionType const& getStateSolution(std::map<Epoch, EpochSolution const*> const& solutions, Epoch const& epoch, uint64_t const& productState);
storm::models::sparse::Mdp<ValueType> const& model; storm::models::sparse::Mdp<ValueType> const& model;
std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> objectives; std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> objectives;
@ -117,13 +124,6 @@ namespace storm {
std::vector<Dimension<ValueType>> dimensions; std::vector<Dimension<ValueType>> dimensions;
std::vector<storm::storage::BitVector> objectiveDimensions; std::vector<storm::storage::BitVector> objectiveDimensions;
struct EpochSolution {
uint64_t count;
std::shared_ptr<std::vector<uint64_t> const> productStateToSolutionVectorMap;
std::vector<SolutionType> solutions;
};
std::map<Epoch, EpochSolution> epochSolutions;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4; storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4;
std::vector<uint64_t> epochModelSizes; std::vector<uint64_t> epochModelSizes;

Loading…
Cancel
Save