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

epochs are now uints instead of vector<int>s

tempestpy_adaptions
TimQu 7 years ago
parent
27ee299f63
commit
3a309caafc
2 changed files with 202 additions and 80 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. 247
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  2. 35
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

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

@ -1,5 +1,7 @@
#include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h"
#include <string>
#include "storm/utility/macros.h" #include "storm/utility/macros.h"
#include "storm/logic/Formulas.h" #include "storm/logic/Formulas.h"
#include "storm/logic/CloneVisitor.h" #include "storm/logic/CloneVisitor.h"
@ -29,16 +31,15 @@ namespace storm {
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initialize() { void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initialize() {
swInit.start(); swInit.start();
STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives."); STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives.");
std::vector<std::vector<uint64_t>> epochSteps;
std::vector<Epoch> epochSteps;
initializeObjectives(epochSteps); initializeObjectives(epochSteps);
initializePossibleEpochSteps(epochSteps);
initializeMemoryProduct(epochSteps); initializeMemoryProduct(epochSteps);
swInit.stop(); swInit.stop();
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initializeObjectives(std::vector<std::vector<uint64_t>>& epochSteps) {
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initializeObjectives(std::vector<Epoch>& epochSteps) {
std::vector<std::vector<uint64_t>> dimensionWiseEpochSteps;
// collect the time-bounded subobjectives // collect the time-bounded subobjectives
for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
auto const& formula = *this->objectives[objIndex].formula; auto const& formula = *this->objectives[objIndex].formula;
@ -61,7 +62,7 @@ namespace storm {
} }
memoryLabels.push_back(memLabel); memoryLabels.push_back(memLabel);
if (boundedUntilFormula.getTimeBoundReference(dim).isTimeBound() || boundedUntilFormula.getTimeBoundReference(dim).isStepBound()) { if (boundedUntilFormula.getTimeBoundReference(dim).isTimeBound() || boundedUntilFormula.getTimeBoundReference(dim).isStepBound()) {
epochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
scalingFactors.push_back(storm::utility::one<ValueType>()); scalingFactors.push_back(storm::utility::one<ValueType>());
} else { } else {
STORM_LOG_ASSERT(boundedUntilFormula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound."); STORM_LOG_ASSERT(boundedUntilFormula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound.");
@ -71,7 +72,7 @@ namespace storm {
STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds."); STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds.");
std::vector<ValueType> actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix()); std::vector<ValueType> actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix());
auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector<ValueType, uint64_t>(actionRewards); auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector<ValueType, uint64_t>(actionRewards);
epochSteps.push_back(std::move(discretizedRewardsAndFactor.first));
dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first));
scalingFactors.push_back(std::move(discretizedRewardsAndFactor.second)); scalingFactors.push_back(std::move(discretizedRewardsAndFactor.second));
} }
} }
@ -79,7 +80,7 @@ namespace storm {
} }
} else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) { } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) {
subObjectives.push_back(std::make_pair(formula.getSubformula().asSharedPointer(), objIndex)); subObjectives.push_back(std::make_pair(formula.getSubformula().asSharedPointer(), objIndex));
epochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
scalingFactors.push_back(storm::utility::one<ValueType>()); scalingFactors.push_back(storm::utility::one<ValueType>());
memoryLabels.push_back(boost::none); memoryLabels.push_back(boost::none);
} }
@ -95,24 +96,43 @@ namespace storm {
} }
objectiveDimensions.push_back(std::move(dimensions)); objectiveDimensions.push_back(std::move(dimensions));
} }
}
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initializePossibleEpochSteps(std::vector<std::vector<uint64_t>> const& epochSteps) {
// collect which epoch steps are possible
possibleEpochSteps.clear();
for (uint64_t choiceIndex = 0; choiceIndex < epochSteps.front().size(); ++choiceIndex) {
// Precompute some data to easily access epoch information;
dimensionCount = subObjectives.size();
STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::UnexpectedException, "Invoked multi dimensional reward unfolding with zero dimensions...");
bitsPerDimension = 64 / dimensionCount;
if (dimensionCount == 1) {
dimensionBitMask = -1ull;
} else {
dimensionBitMask = (1ull << bitsPerDimension) - 1;
}
//std::cout << "dim count: " << dimensionCount << std::endl;
//std::cout << "bitsPerDimension: " << bitsPerDimension << std::endl;
//std::cout << "dimensionBitMask: " << dimensionBitMask << std::endl;
// Convert the epoch steps to a choice-wise representation
epochSteps.reserve(model.getNumberOfChoices());
for (uint64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) {
Epoch step; Epoch step;
step.reserve(epochSteps.size());
for (auto const& dimensionRewards : epochSteps) {
step.push_back(dimensionRewards[choiceIndex]);
uint64_t dim = 0;
for (auto const& dimensionSteps : dimensionWiseEpochSteps) {
setDimensionOfEpoch(step, dim, dimensionSteps[choice]);
++dim;
} }
epochSteps.push_back(step);
}
// collect which epoch steps are possible
possibleEpochSteps.clear();
for (auto const& step : epochSteps) {
possibleEpochSteps.insert(step); possibleEpochSteps.insert(step);
} }
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initializeMemoryProduct(std::vector<std::vector<uint64_t>> const& epochSteps) {
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initializeMemoryProduct(std::vector<Epoch> const& epochSteps) {
// build the memory structure // build the memory structure
auto memoryStructure = computeMemoryStructure(); auto memoryStructure = computeMemoryStructure();
@ -127,7 +147,7 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStartEpoch() { typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStartEpoch() {
Epoch startEpoch; Epoch startEpoch;
for (uint64_t dim = 0; dim < this->subObjectives.size(); ++dim) {
for (uint64_t dim = 0; dim < dimensionCount; ++dim) {
storm::expressions::Expression bound; storm::expressions::Expression bound;
bool isStrict = false; bool isStrict = false;
storm::logic::Formula const& dimFormula = *subObjectives[dim].first; storm::logic::Formula const& dimFormula = *subObjectives[dim].first;
@ -148,9 +168,11 @@ namespace storm {
} else { } else {
discretizedBound = storm::utility::floor(discretizedBound); discretizedBound = storm::utility::floor(discretizedBound);
} }
startEpoch.push_back(storm::utility::convertNumber<uint64_t>(discretizedBound));
uint64_t dimensionValue = storm::utility::convertNumber<uint64_t>(discretizedBound);
STORM_LOG_THROW(isValidDimensionValue(dimensionValue), storm::exceptions::NotSupportedException, "The bound " << bound << " is too high for the considered number of dimensions.");
setDimensionOfEpoch(startEpoch, dim, dimensionValue);
} }
//std::cout << "Start epoch is " << epochToString(startEpoch) << std::endl;
return startEpoch; return startEpoch;
} }
@ -183,6 +205,8 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::EpochModel& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setCurrentEpoch(Epoch const& epoch) { typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::EpochModel& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setCurrentEpoch(Epoch const& epoch) {
// std::cout << "Setting model for epoch " << epochToString(epoch) << std::endl;
// Check if we need to update the current epoch class // Check if we need to update the current epoch class
if (!currentEpoch || !sameEpochClass(epoch, currentEpoch.get())) { if (!currentEpoch || !sameEpochClass(epoch, currentEpoch.get())) {
setCurrentEpochClass(epoch); setCurrentEpochClass(epoch);
@ -196,12 +220,13 @@ 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 memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState)); auto memoryState = memoryProduct.convertMemoryState(memoryProduct.getMemoryState(productState));
Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice].get());
Epoch successorEpoch = getSuccessorEpoch(epoch, memoryProduct.getSteps()[productChoice]);
// Find out whether objective reward is earned for the current choice // Find out whether objective reward is earned for the current choice
// Objective reward is not earned if there is a subObjective that is still relevant but the corresponding reward bound is passed after taking the choice
swAux1.start(); swAux1.start();
for (uint64_t dim = 0; dim < successorEpoch.size(); ++dim) {
if (successorEpoch[dim] < 0 && memoryState.get(dim)) {
for (uint64_t dim = 0; dim < dimensionCount; ++dim) {
if (isBottomDimension(successorEpoch, dim) && memoryState.get(dim)) {
epochModel.objectiveRewardFilter[subObjectives[dim].second].set(reducedChoice, false); epochModel.objectiveRewardFilter[subObjectives[dim].second].set(reducedChoice, false);
} }
} }
@ -224,9 +249,9 @@ namespace storm {
swAux3.stop(); swAux3.stop();
} else { } else {
swAux4.start(); swAux4.start();
storm::storage::BitVector successorRelevantDimensions(successorEpoch.size(), true);
storm::storage::BitVector successorRelevantDimensions(dimensionCount, true);
for (auto const& dim : memoryState) { for (auto const& dim : memoryState) {
if (successorEpoch[dim] < 0) {
if (isBottomDimension(successorEpoch, dim)) {
successorRelevantDimensions &= ~objectiveDimensions[subObjectives[dim].second]; successorRelevantDimensions &= ~objectiveDimensions[subObjectives[dim].second];
} }
} }
@ -283,15 +308,8 @@ namespace storm {
storm::storage::BitVector stepChoices(memoryProduct.getProduct().getNumberOfChoices(), false); storm::storage::BitVector stepChoices(memoryProduct.getProduct().getNumberOfChoices(), false);
uint64_t choice = 0; uint64_t choice = 0;
for (auto const& step : memoryProduct.getSteps()) { for (auto const& step : memoryProduct.getSteps()) {
if (step) {
auto eIt = epoch.begin();
for (auto const& s : step.get()) {
if (s != 0 && *eIt >= 0) {
stepChoices.set(choice, true);
break;
}
++eIt;
}
if (!isZeroEpoch(step) && getSuccessorEpoch(epoch, step) != epoch) {
stepChoices.set(choice, true);
} }
++choice; ++choice;
} }
@ -353,16 +371,18 @@ namespace storm {
storm::storage::BitVector reachableStates = result; storm::storage::BitVector reachableStates = result;
std::vector<uint_fast64_t> stack(reachableStates.begin(), reachableStates.end()); std::vector<uint_fast64_t> stack(reachableStates.begin(), reachableStates.end());
// std::cout << "Computing product In states for epoch " << epochToString(epoch) << std::endl;
while (!stack.empty()) { while (!stack.empty()) {
uint64_t state = stack.back(); uint64_t state = stack.back();
stack.pop_back(); stack.pop_back();
for (uint64_t choice = productMatrix.getRowGroupIndices()[state]; choice < productMatrix.getRowGroupIndices()[state + 1]; ++choice) { for (uint64_t choice = productMatrix.getRowGroupIndices()[state]; choice < productMatrix.getRowGroupIndices()[state + 1]; ++choice) {
auto const& choiceStep = memoryProduct.getSteps()[choice]; auto const& choiceStep = memoryProduct.getSteps()[choice];
if (choiceStep) {
if (!isZeroEpoch(choiceStep)) {
storm::storage::BitVector objectiveSet(objectives.size(), false); storm::storage::BitVector objectiveSet(objectives.size(), false);
for (uint64_t dim = 0; dim < epoch.size(); ++dim) {
if (epoch[dim] < 0 && choiceStep.get()[dim] > 0) {
for (uint64_t dim = 0; dim < dimensionCount; ++dim) {
if (isBottomDimension(epoch, dim) && getDimensionOfEpoch(choiceStep, dim) > 0) {
objectiveSet.set(subObjectives[dim].second); objectiveSet.set(subObjectives[dim].second);
} }
} }
@ -442,6 +462,29 @@ namespace storm {
storm::utility::vector::addScaledVector(solution, solutionToAdd, scalingFactor); storm::utility::vector::addScaledVector(solution, solutionToAdd, scalingFactor);
} }
template<typename ValueType, bool SingleObjectiveMode>
template<bool SO, typename std::enable_if<SO, int>::type>
std::string MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::solutionToString(SolutionType const& solution) const {
return std::to_string(solution);
}
template<typename ValueType, bool SingleObjectiveMode>
template<bool SO, typename std::enable_if<!SO, int>::type>
std::string MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::solutionToString(SolutionType const& solution) const {
std::string res = "(";
bool first = true;
for (auto const& s : solution) {
if (first) {
first = false;
} else {
res += ", ";
}
res += std::to_string(s);
}
res += ")";
return res;
}
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch() { void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch() {
swInsertSol.start(); swInsertSol.start();
@ -457,18 +500,18 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution) { void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::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."); STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before.");
std::vector<int64_t> solutionKey = currentEpoch.get();
solutionKey.push_back(productState);
//std::cout << "Storing solution for epoch " << epochToString(currentEpoch.get()) << " and state " << productState << std::endl;
std::vector<uint64_t> solutionKey = { currentEpoch.get() , productState};
solutions[solutionKey] = solution; solutions[solutionKey] = solution;
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(Epoch const& epoch, uint64_t const& productState) { typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(Epoch const& epoch, uint64_t const& productState) {
swFindSol.start(); swFindSol.start();
std::vector<int64_t> solutionKey = epoch;
solutionKey.push_back(productState);
//std::cout << "Getting solution for epoch " << epochToString(epoch) << " and state " << productState << std::endl;
std::vector<uint64_t> solutionKey = { epoch , productState};
auto solutionIt = solutions.find(solutionKey); auto solutionIt = solutions.find(solutionKey);
STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << storm::utility::vector::toString(epoch) << ".");
STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << epochToString(epoch) << ".");
swFindSol.stop(); swFindSol.stop();
return solutionIt->second; return solutionIt->second;
} }
@ -575,9 +618,9 @@ namespace storm {
std::vector<storm::storage::BitVector> result; std::vector<storm::storage::BitVector> result;
result.reserve(memory.getNumberOfStates()); result.reserve(memory.getNumberOfStates());
for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) {
storm::storage::BitVector relevantSubObjectives(memoryLabels.size(), false);
storm::storage::BitVector relevantSubObjectives(dimensionCount, false);
std::set<std::string> stateLabels = memory.getStateLabeling().getLabelsOfState(memState); std::set<std::string> stateLabels = memory.getStateLabeling().getLabelsOfState(memState);
for (uint64_t dim = 0; dim < memoryLabels.size(); ++dim) {
for (uint64_t dim = 0; dim < dimensionCount; ++dim) {
if (memoryLabels[dim] && stateLabels.find(memoryLabels[dim].get()) != stateLabels.end()) { if (memoryLabels[dim] && stateLabels.find(memoryLabels[dim].get()) != stateLabels.end()) {
relevantSubObjectives.set(dim, true); relevantSubObjectives.set(dim, true);
} }
@ -588,7 +631,7 @@ namespace storm {
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::MemoryProduct(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<std::vector<uint64_t>> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions) : memoryStateMap(std::move(memoryStateMap)) {
MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::MemoryProduct(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<Epoch> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions) : memoryStateMap(std::move(memoryStateMap)) {
storm::storage::SparseModelMemoryProduct<ValueType> productBuilder(memory.product(model)); storm::storage::SparseModelMemoryProduct<ValueType> productBuilder(memory.product(model));
setReachableStates(productBuilder, originalModelSteps, objectiveDimensions); setReachableStates(productBuilder, originalModelSteps, objectiveDimensions);
@ -623,18 +666,13 @@ namespace storm {
} }
// Compute the epoch steps for the product // Compute the epoch steps for the product
steps.resize(getProduct().getNumberOfChoices());
steps.resize(getProduct().getNumberOfChoices(), 0);
for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) {
uint64_t numChoices = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupSize(modelState); uint64_t numChoices = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupSize(modelState);
uint64_t firstChoice = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupIndices()[modelState]; uint64_t firstChoice = productBuilder.getOriginalModel().getTransitionMatrix().getRowGroupIndices()[modelState];
for (uint64_t choiceOffset = 0; choiceOffset < numChoices; ++choiceOffset) { for (uint64_t choiceOffset = 0; choiceOffset < numChoices; ++choiceOffset) {
Epoch step;
bool isZeroStep = true;
for (uint64_t dim = 0; dim < originalModelSteps.size(); ++dim) {
step.push_back(originalModelSteps[dim][firstChoice + choiceOffset]);
isZeroStep = isZeroStep && step.back() == 0;
}
if (!isZeroStep) {
Epoch const& step = originalModelSteps[firstChoice + choiceOffset];
if (step != 0) {
for (uint64_t memState = 0; memState < numMemoryStates; ++memState) { for (uint64_t memState = 0; memState < numMemoryStates; ++memState) {
if (productStateExists(modelState, memState)) { if (productStateExists(modelState, memState)) {
uint64_t productState = getProductState(modelState, memState); uint64_t productState = getProductState(modelState, memState);
@ -649,7 +687,22 @@ namespace storm {
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::setReachableStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<std::vector<uint64_t>> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions) const {
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::setReachableStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions) const {
// todo: find something else to check whether a specific dimension at a specific choice is bottom
uint64_t dimensionCount = objectiveDimensions.front().size();
uint64_t bitsPerDimension = 64 / dimensionCount;
uint64_t dimensionBitMask;
if (dimensionCount == 1) {
dimensionBitMask = -1ull;
} else {
dimensionBitMask = (1ull << bitsPerDimension) - 1;
}
std::vector<storm::storage::BitVector> additionalReachableStates(memoryStateMap.size(), storm::storage::BitVector(productBuilder.getOriginalModel().getNumberOfStates(), false)); std::vector<storm::storage::BitVector> additionalReachableStates(memoryStateMap.size(), storm::storage::BitVector(productBuilder.getOriginalModel().getNumberOfStates(), false));
for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) {
auto const& memStateBv = memoryStateMap[memState]; auto const& memStateBv = memoryStateMap[memState];
@ -665,7 +718,9 @@ namespace storm {
for (auto const& objIndex : consideredObjectives) { for (auto const& objIndex : consideredObjectives) {
bool objectiveHasStep = false; bool objectiveHasStep = false;
for (auto const& dim : objectiveDimensions[objIndex]) { for (auto const& dim : objectiveDimensions[objIndex]) {
if (originalModelSteps[dim][choice] > 0) {
// TODO: this can not be called currently if (getDimensionOfEpoch(originalModelSteps[choice], dim) > 0) {
// .. instead we do this
if (((originalModelSteps[choice] >> (dim * bitsPerDimension)) & dimensionBitMask) > 0) {
objectiveHasStep = true; objectiveHasStep = true;
break; break;
} }
@ -701,7 +756,7 @@ namespace storm {
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
std::vector<boost::optional<typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch>> const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::getSteps() const {
std::vector<typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch> const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MemoryProduct::getSteps() const {
return steps; return steps;
} }
@ -777,7 +832,7 @@ namespace storm {
// find out whether objective reward should be earned within this epoch // find out whether objective reward should be earned within this epoch
bool collectRewardInEpoch = true; bool collectRewardInEpoch = true;
for (auto const& subObjIndex : relevantObjectives) { for (auto const& subObjIndex : relevantObjectives) {
if (epoch[dimensionIndexMap[subObjIndex]] < 0) {
if (isBottomDimension(epoch, dimensionIndexMap[subObjIndex])) {
collectRewardInEpoch = false; collectRewardInEpoch = false;
break; break;
} }
@ -818,7 +873,7 @@ namespace storm {
bool rewardCollectedInEpoch = true; bool rewardCollectedInEpoch = true;
if (formula.getSubformula().isCumulativeRewardFormula()) { if (formula.getSubformula().isCumulativeRewardFormula()) {
assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1); assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1);
rewardCollectedInEpoch = epoch[*objectiveDimensions[objIndex].begin()] >= 0;
rewardCollectedInEpoch = !isBottomDimension(epoch, *objectiveDimensions[objIndex].begin());
} else { } else {
STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula); STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula);
} }
@ -837,28 +892,80 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
bool MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::sameEpochClass(Epoch const& epoch1, Epoch const& epoch2) const { bool MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::sameEpochClass(Epoch const& epoch1, Epoch const& epoch2) const {
assert(epoch1.size() == epoch2.size());
for (auto e1It = epoch1.begin(), e2It = epoch2.begin(); e1It != epoch1.end(); ++e1It, ++e2It) {
if ((*e1It) < 0 != (*e2It < 0)) {
uint64_t mask = dimensionBitMask;
for (uint64_t d = 0; d < dimensionCount; ++d) {
if (((epoch1 & mask) == mask) != ((epoch2 & mask) == mask)) {
return false; return false;
} }
mask = mask << bitsPerDimension;
} }
return true; return true;
} }
template<typename ValueType, bool SingleObjectiveMode> template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const { typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const {
assert(epoch.size() == step.size());
Epoch result;
result.reserve(epoch.size());
auto stepIt = step.begin();
for (auto const& e : epoch) {
result.push_back(std::max((int64_t) -1, e - *stepIt));
++stepIt;
// Start with dimension zero
uint64_t mask = dimensionBitMask;
uint64_t e_d = epoch & mask;
uint64_t s_d = step & mask;
assert(s_d != mask);
uint64_t result = (e_d < s_d || e_d == mask) ? mask : e_d - s_d;
// Consider the remaining dimensions
for (uint64_t d = 1; d < dimensionCount; ++d) {
mask = mask << bitsPerDimension;
e_d = epoch & mask;
s_d = step & mask;
assert(s_d != mask);
result |= ((e_d < s_d || e_d == mask) ? mask : e_d - s_d);
} }
return result; return result;
} }
template<typename ValueType, bool SingleObjectiveMode>
bool MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::isValidDimensionValue(uint64_t const& value) const {
return ((value & dimensionBitMask) == value) && value != dimensionBitMask;
}
template<typename ValueType, bool SingleObjectiveMode>
bool MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::isZeroEpoch(Epoch const& epoch) const {
return epoch == 0;
}
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setBottomDimension(Epoch& epoch, uint64_t const& dimension) const {
epoch |= (dimensionBitMask << (dimension * bitsPerDimension));
}
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setDimensionOfEpoch(Epoch& epoch, uint64_t const& dimension, uint64_t const& value) const {
STORM_LOG_ASSERT(isValidDimensionValue(value), "The dimension value " << value << " is too high.");
epoch &= ~(dimensionBitMask << (dimension * bitsPerDimension));
epoch |= (value << (dimension * bitsPerDimension));
}
template<typename ValueType, bool SingleObjectiveMode>
bool MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const {
return (epoch | (dimensionBitMask << (dimension * bitsPerDimension))) == epoch;
}
template<typename ValueType, bool SingleObjectiveMode>
uint64_t MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const {
return (epoch >> (dimension * bitsPerDimension)) & dimensionBitMask;
}
template<typename ValueType, bool SingleObjectiveMode>
std::string MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::epochToString(Epoch const& epoch) const {
std::string res = "<" + std::to_string(getDimensionOfEpoch(epoch, 0));
for (uint64_t d = 1; d < dimensionCount; ++d) {
res += ", ";
res += std::to_string(getDimensionOfEpoch(epoch, d));
}
res += ">";
return res;
}
template class MultiDimensionalRewardUnfolding<double, true>; template class MultiDimensionalRewardUnfolding<double, true>;
template class MultiDimensionalRewardUnfolding<double, false>; template class MultiDimensionalRewardUnfolding<double, false>;

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

@ -22,7 +22,7 @@ namespace storm {
class MultiDimensionalRewardUnfolding { class MultiDimensionalRewardUnfolding {
public: public:
typedef std::vector<int64_t> Epoch; // The number of reward steps that are "left" for each dimension
typedef uint64_t Epoch; // The number of reward steps that are "left" for each dimension
typedef typename std::conditional<SingleObjectiveMode, ValueType, std::vector<ValueType>>::type SolutionType; typedef typename std::conditional<SingleObjectiveMode, ValueType, std::vector<ValueType>>::type SolutionType;
@ -87,10 +87,10 @@ namespace storm {
class MemoryProduct { class MemoryProduct {
public: public:
MemoryProduct() = default; MemoryProduct() = default;
MemoryProduct(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<std::vector<uint64_t>> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions);
MemoryProduct(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<Epoch> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions);
storm::models::sparse::Mdp<ValueType> const& getProduct() const; storm::models::sparse::Mdp<ValueType> const& getProduct() const;
std::vector<boost::optional<Epoch>> const& getSteps() const;
std::vector<Epoch> const& getSteps() const;
bool productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const; bool productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const;
uint64_t getProductState(uint64_t const& modelState, uint64_t const& memoryState) const; uint64_t getProductState(uint64_t const& modelState, uint64_t const& memoryState) const;
@ -104,11 +104,11 @@ namespace storm {
private: private:
void setReachableStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<std::vector<uint64_t>> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions) const;
void setReachableStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps, std::vector<storm::storage::BitVector> const& objectiveDimensions) const;
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> product; std::shared_ptr<storm::models::sparse::Mdp<ValueType>> product;
std::vector<boost::optional<Epoch>> steps;
std::vector<Epoch> steps;
std::vector<uint64_t> modelMemoryToProductStateMap; std::vector<uint64_t> modelMemoryToProductStateMap;
std::vector<uint64_t> productToModelStateMap; std::vector<uint64_t> productToModelStateMap;
@ -123,17 +123,22 @@ namespace storm {
void initialize(); void initialize();
void initializeObjectives(std::vector<std::vector<uint64_t>>& epochSteps);
void initializePossibleEpochSteps(std::vector<std::vector<uint64_t>> const& epochSteps);
void initializeObjectives(std::vector<Epoch>& epochSteps);
void initializeMemoryProduct(std::vector<std::vector<uint64_t>> const& epochSteps);
void initializeMemoryProduct(std::vector<Epoch> const& epochSteps);
storm::storage::MemoryStructure computeMemoryStructure() const; storm::storage::MemoryStructure computeMemoryStructure() const;
std::vector<storm::storage::BitVector> computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; std::vector<storm::storage::BitVector> computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const;
std::vector<std::vector<ValueType>> computeObjectiveRewardsForProduct(Epoch const& epoch) const; std::vector<std::vector<ValueType>> computeObjectiveRewardsForProduct(Epoch const& epoch) const;
bool sameEpochClass(Epoch const& epoch1, Epoch const& epoch2) const; bool sameEpochClass(Epoch const& epoch1, Epoch const& epoch2) const;
Epoch getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const; Epoch getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const;
bool isZeroEpoch(Epoch const& epoch) const;
bool isValidDimensionValue(uint64_t const& value) const;
void setBottomDimension(Epoch& epoch, uint64_t const& dimension) const;
void setDimensionOfEpoch(Epoch& epoch, uint64_t const& dimension, uint64_t const& value) const; // assumes that the value is small enough
bool isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const;
uint64_t getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const; // assumes that the dimension is not bottom
std::string epochToString(Epoch const& epoch) const;
template<bool SO = SingleObjectiveMode, typename std::enable_if<SO, int>::type = 0> template<bool SO = SingleObjectiveMode, typename std::enable_if<SO, int>::type = 0>
SolutionType getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const; SolutionType getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const;
@ -145,6 +150,11 @@ namespace storm {
template<bool SO = SingleObjectiveMode, typename std::enable_if<!SO, int>::type = 0> template<bool SO = SingleObjectiveMode, typename std::enable_if<!SO, int>::type = 0>
void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const; void addScaledSolution(SolutionType& solution, SolutionType const& solutionToAdd, ValueType const& scalingFactor) const;
template<bool SO = SingleObjectiveMode, typename std::enable_if<SO, int>::type = 0>
std::string solutionToString(SolutionType const& solution) const;
template<bool SO = SingleObjectiveMode, typename std::enable_if<!SO, int>::type = 0>
std::string solutionToString(SolutionType const& solution) const;
void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution); void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution);
SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState); SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState);
@ -162,12 +172,17 @@ namespace storm {
boost::optional<Epoch> currentEpoch; boost::optional<Epoch> currentEpoch;
uint64_t dimensionCount;
uint64_t bitsPerDimension;
uint64_t dimensionBitMask;
std::vector<storm::storage::BitVector> objectiveDimensions; std::vector<storm::storage::BitVector> objectiveDimensions;
std::vector<std::pair<std::shared_ptr<storm::logic::Formula const>, uint64_t>> subObjectives; std::vector<std::pair<std::shared_ptr<storm::logic::Formula const>, uint64_t>> subObjectives;
std::vector<boost::optional<std::string>> memoryLabels; std::vector<boost::optional<std::string>> memoryLabels;
std::vector<ValueType> scalingFactors; std::vector<ValueType> scalingFactors;
std::map<std::vector<int64_t>, SolutionType> solutions;
std::map<std::vector<uint64_t>, SolutionType> solutions;
storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4; storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4;

Write Preview
Loading…
Cancel
Save