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

Fixes for lower bounds

tempestpy_adaptions
TimQu 7 years ago
parent
ade8078759
commit
7d4a438e82
3 changed files with 82 additions and 61 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 71
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  2. 71
      src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp
  3. 1
      src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h

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

@ -155,7 +155,6 @@ namespace storm {
auto memoryStateMap = computeMemoryStateMap(memoryStructure);
productModel = std::make_unique<ProductModel<ValueType>>(model, memoryStructure, dimensions, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps);
}
template<typename ValueType, bool SingleObjectiveMode>
@ -276,6 +275,13 @@ namespace storm {
}
swSetEpoch.start();
bool containsLowerBoundedObjective = false;
for (auto const& dimension : dimensions) {
if (!dimension.isUpperBounded) {
containsLowerBoundedObjective = true;
break;
}
}
epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
auto stepSolIt = epochModel.stepSolutions.begin();
@ -301,12 +307,11 @@ namespace storm {
}
epochModel.objectiveRewardFilter[objIndex].set(reducedChoice, rewardEarned);
}
// compute the solution for the stepChoices
// For optimization purposes, we distinguish the easier case where the successor epoch lies in the same epoch class
SolutionType choiceSolution;
bool firstSuccessor = true;
if (epochManager.compareEpochClass(epoch, successorEpoch)) {
if (!containsLowerBoundedObjective && epochManager.compareEpochClass(epoch, successorEpoch)) {
for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
if (firstSuccessor) {
choiceSolution = getScaledSolution(getStateSolution(successorEpoch, successor.getColumn()), successor.getValue());
@ -326,7 +331,7 @@ namespace storm {
}
}
for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
storm::storage::BitVector successorMemoryState = (productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & allowedRelevantDimensions) | forcedRelevantDimensions;
storm::storage::BitVector successorMemoryState = (productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) | forcedRelevantDimensions) & allowedRelevantDimensions;
uint64_t successorProductState = productModel->getProductState(productModel->getModelState(successor.getColumn()), productModel->convertMemoryState(successorMemoryState));
SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState);
if (firstSuccessor) {
@ -370,7 +375,7 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setCurrentEpochClass(Epoch const& epoch) {
EpochClass epochClass = epochManager.getEpochClass(epoch);
// std::cout << "Setting epoch class for epoch " << storm::utility::vector::toString(epoch) << std::endl;
// std::cout << "Setting epoch class for epoch " << epochManager.toString(epoch) << std::endl;
swSetEpochClass.start();
swAux1.start();
auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives);
@ -392,10 +397,14 @@ namespace storm {
}
}
if (!violatedLowerBoundedDimensions.empty()) {
for (auto& entry : epochModel.epochMatrix) {
storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(entry.getColumn()));
successorMemoryState |= violatedLowerBoundedDimensions;
entry.setColumn(productModel->getProductState(productModel->getModelState(entry.getColumn()), productModel->convertMemoryState(successorMemoryState)));
for (uint64_t state = 0; state < epochModel.epochMatrix.getRowGroupCount(); ++state) {
auto const& memoryState = productModel->convertMemoryState(productModel->getMemoryState(state));
storm::storage::BitVector forcedRelevantDimensions = memoryState & violatedLowerBoundedDimensions;
for (auto& entry : epochModel.epochMatrix.getRowGroup(state)) {
storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(entry.getColumn()));
successorMemoryState |= forcedRelevantDimensions;
entry.setColumn(productModel->getProductState(productModel->getModelState(entry.getColumn()), productModel->convertMemoryState(successorMemoryState)));
}
}
}
@ -435,21 +444,15 @@ namespace storm {
epochModel.objectiveRewards.clear();
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
bool objHasViolatedLowerDimension = false;
for (auto const& dim : objectiveDimensions[objIndex]) {
if (!dimensions[dim].isUpperBounded && !epochManager.isBottomDimensionEpochClass(epochClass, dim)) {
objHasViolatedLowerDimension = true;
}
}
std::vector<ValueType> const& productObjRew = productObjectiveRewards[objIndex];
std::vector<ValueType> reducedModelObjRewards;
if (objHasViolatedLowerDimension) {
reducedModelObjRewards.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero<ValueType>());
} else {
std::vector<ValueType> const& productObjRew = productObjectiveRewards[objIndex];
reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount());
for (auto const& productChoice : epochModelToProductChoiceMap) {
reducedModelObjRewards.push_back(productObjRew[productChoice]);
}
reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount());
for (auto const& productChoice : epochModelToProductChoiceMap) {
reducedModelObjRewards.push_back(productObjRew[productChoice]);
}
// Check if the objective is violated in the current epoch
if (!violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) {
storm::utility::vector::setVectorValues(reducedModelObjRewards, ~epochModel.stepChoices, storm::utility::zero<ValueType>());
}
epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards));
}
@ -512,24 +515,27 @@ namespace storm {
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);
std::stringstream stringstream;
stringstream << solution;
return stringstream.str();
}
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 = "(";
std::stringstream stringstream;
stringstream << "(";
bool first = true;
for (auto const& s : solution) {
if (first) {
first = false;
} else {
res += ", ";
stringstream << ", ";
}
res += std::to_string(s);
stringstream << s;
}
res += ")";
return res;
stringstream << ")";
return stringstream.str();
}
template<typename ValueType, bool SingleObjectiveMode>
@ -571,8 +577,11 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStateSolution(Epoch const& epoch, uint64_t const& productState) {
STORM_LOG_ASSERT(epochSolutions.find(epoch) != epochSolutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << ".");
EpochSolution const& epochSolution = epochSolutions[epoch];
auto epochSolutionIt = epochSolutions.find(epoch);
STORM_LOG_ASSERT(epochSolutionIt != epochSolutions.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]];
}

71
src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp
View File

@ -140,6 +140,7 @@ namespace storm {
storm::storage::BitVector consideredDimensions(dimensions.size(), false);
do {
// todo: this selects more states then necessary
if (consideredDimensions.isSubsetOf(lowerBoundedDimensions)) {
for (uint64_t memoryState = 0; memoryState < productBuilder.getMemory().getNumberOfStates(); ++memoryState) {
uint64_t memoryStatePrime = convertMemoryState(convertMemoryState(memoryState) | consideredDimensions);
@ -256,7 +257,7 @@ namespace storm {
// find out whether objective reward should be earned within this epoch class
bool collectRewardInEpoch = true;
for (auto const& subObjIndex : relevantObjectives) {
if (dimensions[dimensionIndexMap[subObjIndex]].isUpperBounded == epochManager.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) {
if (dimensions[dimensionIndexMap[subObjIndex]].isUpperBounded && epochManager.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) {
collectRewardInEpoch = false;
break;
}
@ -371,7 +372,7 @@ namespace storm {
if (dimensions[dim].isUpperBounded && bottomDimensions.get(dim)) {
allowedRelevantDimensions.set(dim, false);
} else if (!dimensions[dim].isUpperBounded && nonBottomDimensions.get(dim)) {
forcedRelevantDimensions.set(dim, false);
forcedRelevantDimensions.set(dim, true);
}
}
assert(forcedRelevantDimensions.isSubsetOf(allowedRelevantDimensions));
@ -393,20 +394,31 @@ namespace storm {
}
}
STORM_LOG_ASSERT(reachableStates.find(predecessor) != reachableStates.end(), "Could not find reachable states of predecessor epoch class.");
storm::storage::BitVector predecessorChoices = getProduct().getTransitionMatrix().getRowFilter(reachableStates.find(predecessor)->second);
for (auto const& choice : predecessorChoices) {
bool choiceLeadsToThisClass = false;
Epoch const& choiceStep = getSteps()[choice];
for (auto const& dim : positiveStepDimensions) {
if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) {
choiceLeadsToThisClass = true;
storm::storage::BitVector predecessorStates = reachableStates.find(predecessor)->second;
for (auto const& predecessorState : predecessorStates) {
storm::storage::BitVector const& predecessorMemStateBv = convertMemoryState(getMemoryState(predecessorState));
storm::storage::BitVector currentAllowedRelDim = allowedRelevantDimensions;
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (!allowedRelevantDimensions.get(dim) && predecessorMemStateBv.get(dim)) {
currentAllowedRelDim &= ~objectiveDimensions[dimensions[dim].objectiveIndex];
}
}
if (choiceLeadsToThisClass) {
for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) {
uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions);
ecInStates.set(successorState, true);
storm::storage::BitVector currentForcedRelDim = forcedRelevantDimensions & predecessorMemStateBv;
for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[predecessorState]; choice < getProduct().getTransitionMatrix().getRowGroupIndices()[predecessorState + 1]; ++choice) {
bool choiceLeadsToThisClass = false;
Epoch const& choiceStep = getSteps()[choice];
for (auto const& dim : positiveStepDimensions) {
if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) {
choiceLeadsToThisClass = true;
}
}
if (choiceLeadsToThisClass) {
for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) {
uint64_t successorState = transformProductState(transition.getColumn(), currentAllowedRelDim, currentForcedRelDim);
ecInStates.set(successorState, true);
}
}
}
}
@ -420,6 +432,16 @@ namespace storm {
uint64_t currentState = dfsStack.back();
dfsStack.pop_back();
storm::storage::BitVector const& currentMemStateBv = convertMemoryState(getMemoryState(currentState));
storm::storage::BitVector currentAllowedRelDim = allowedRelevantDimensions;
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (!allowedRelevantDimensions.get(dim) && currentMemStateBv.get(dim)) {
currentAllowedRelDim &= ~objectiveDimensions[dimensions[dim].objectiveIndex];
}
}
storm::storage::BitVector currentForcedRelDim = forcedRelevantDimensions & currentMemStateBv;
for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[currentState]; choice != getProduct().getTransitionMatrix().getRowGroupIndices()[currentState + 1]; ++choice) {
bool choiceLeadsOutsideOfEpoch = false;
@ -431,7 +453,7 @@ namespace storm {
}
for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) {
uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions);
uint64_t successorState = transformProductState(transition.getColumn(), currentAllowedRelDim, currentForcedRelDim);
if (choiceLeadsOutsideOfEpoch) {
ecInStates.set(successorState, true);
}
@ -444,29 +466,20 @@ namespace storm {
}
reachableStates[epochClass] = std::move(ecReachableStates);
inStates[epochClass] = std::move(ecInStates);
}
template<typename ValueType>
uint64_t ProductModel<ValueType>::transformProductState(uint64_t productState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const {
return getProductState(getModelState(productState), transformMemoryState(getMemoryState(productState), allowedRelevantDimensions, forcedRelevantDimensions));
}
template<typename ValueType>
uint64_t ProductModel<ValueType>::transformMemoryState(uint64_t memoryState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const {
if (allowedRelevantDimensions.full() && forcedRelevantDimensions.empty()) {
return memoryState;
return productState;
} else {
storm::storage::BitVector memoryStateBv = (convertMemoryState(getMemoryState(productState)) | forcedRelevantDimensions) & allowedRelevantDimensions;
return getProductState(getModelState(productState), convertMemoryState(memoryStateBv));
}
storm::storage::BitVector memoryStateBv = convertMemoryState(memoryState) | forcedRelevantDimensions;
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (!allowedRelevantDimensions.get(dim) && memoryStateBv.get(dim)) {
memoryStateBv &= ~objectiveDimensions[dimensions[dim].objectiveIndex];
}
}
return convertMemoryState(memoryStateBv);
}
template class ProductModel<double>;
template class ProductModel<storm::RationalNumber>;

1
src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h
View File

@ -52,7 +52,6 @@ namespace storm {
void computeReachableStatesInEpochClasses();
void computeReachableStates(EpochClass const& epochClass, std::vector<EpochClass> const& predecessors);
uint64_t transformProductState(uint64_t productState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const;
uint64_t transformMemoryState(uint64_t memoryState, storm::storage::BitVector const& allowedRelevantDimensions, storm::storage::BitVector const& forcedRelevantDimensions) const;
std::vector<Dimension<ValueType>> const& dimensions;
std::vector<storm::storage::BitVector> const& objectiveDimensions;

Write Preview
Loading…
Cancel
Save