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

first version for lower bounded properties

main
TimQu 8 years ago
parent
4ba20d11d4
commit
b054b67312
5 changed files with 312 additions and 157 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. 79
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  2. 1
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
  3. 351
      src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp
  4. 18
      src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h
  5. 20
      src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp

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

@ -154,7 +154,7 @@ namespace storm {
// build a mapping between the different representations of memory states
auto memoryStateMap = computeMemoryStateMap(memoryStructure);
productModel = std::make_unique<ProductModel<ValueType>>(model, memoryStructure, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps);
productModel = std::make_unique<ProductModel<ValueType>>(model, memoryStructure, dimensions, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps);
}
@ -276,11 +276,6 @@ namespace storm {
}
swSetEpoch.start();
epochModel.objectiveRewardFilter.clear();
for (auto const& objRewards : epochModel.objectiveRewards) {
epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards));
epochModel.objectiveRewardFilter.back().complement();
}
epochModel.stepSolutions.resize(epochModel.stepChoices.getNumberOfSetBits());
auto stepSolIt = epochModel.stepSolutions.begin();
@ -291,19 +286,24 @@ namespace storm {
Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, productModel->getSteps()[productChoice]);
// 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
// Objective reward is not earned if
// a) there is an upper bounded subObjective that is still relevant but the corresponding reward bound is passed after taking the choice
// b) there is a lower bounded subObjective and the corresponding reward bound is not passed yet.
for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (epochModel.objectiveRewardFilter[objIndex].get(reducedChoice)) {
bool rewardEarned = !storm::utility::isZero(epochModel.objectiveRewards[objIndex][reducedChoice]);
if (rewardEarned) {
for (auto const& dim : objectiveDimensions[objIndex]) {
if (dimensions[dim].isUpperBounded == epochManager.isBottomDimension(successorEpoch, dim) && memoryState.get(dim)) {
epochModel.objectiveRewardFilter[objIndex].set(reducedChoice, false);
rewardEarned = false;
break;
}
}
}
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)) {
@ -316,14 +316,17 @@ namespace storm {
}
}
} else {
storm::storage::BitVector successorRelevantDimensions(epochManager.getDimensionCount(), true);
storm::storage::BitVector allowedRelevantDimensions(epochManager.getDimensionCount(), true);
storm::storage::BitVector forcedRelevantDimensions(epochManager.getDimensionCount(), false);
for (auto const& dim : memoryState) {
if (epochManager.isBottomDimension(successorEpoch, dim)) {
successorRelevantDimensions &= ~objectiveDimensions[dimensions[dim].objectiveIndex];
if (epochManager.isBottomDimension(successorEpoch, dim) && dimensions[dim].isUpperBounded) {
allowedRelevantDimensions &= ~objectiveDimensions[dimensions[dim].objectiveIndex];
} else if (!epochManager.isBottomDimension(successorEpoch, dim) && !dimensions[dim].isUpperBounded) {
forcedRelevantDimensions.set(dim, true);
}
}
for (auto const& successor : productModel->getProduct().getTransitionMatrix().getRow(productChoice)) {
storm::storage::BitVector successorMemoryState = productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & successorRelevantDimensions;
storm::storage::BitVector successorMemoryState = (productModel->convertMemoryState(productModel->getMemoryState(successor.getColumn())) & allowedRelevantDimensions) | forcedRelevantDimensions;
uint64_t successorProductState = productModel->getProductState(productModel->getModelState(successor.getColumn()), productModel->convertMemoryState(successorMemoryState));
SolutionType const& successorSolution = getStateSolution(successorEpoch, successorProductState);
if (firstSuccessor) {
@ -366,10 +369,11 @@ 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;
swSetEpochClass.start();
swAux1.start();
auto productObjectiveRewards = productModel->computeObjectiveRewards(epoch, objectives, dimensions);
auto productObjectiveRewards = productModel->computeObjectiveRewards(epochClass, objectives);
storm::storage::BitVector stepChoices(productModel->getProduct().getNumberOfChoices(), false);
uint64_t choice = 0;
@ -380,17 +384,33 @@ namespace storm {
++choice;
}
epochModel.epochMatrix = productModel->getProduct().getTransitionMatrix().filterEntries(~stepChoices);
// redirect transitions for the case where the lower reward bounds are not met yet
storm::storage::BitVector violatedLowerBoundedDimensions(dimensions.size(), false);
for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
if (!dimensions[dim].isUpperBounded && !epochManager.isBottomDimensionEpochClass(epochClass, dim)) {
violatedLowerBoundedDimensions.set(dim);
}
}
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)));
}
}
storm::storage::BitVector zeroObjRewardChoices(productModel->getProduct().getNumberOfChoices(), true);
for (auto const& objRewards : productObjectiveRewards) {
zeroObjRewardChoices &= storm::utility::vector::filterZero(objRewards);
for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) {
if (violatedLowerBoundedDimensions.isDisjointFrom(objectiveDimensions[objIndex])) {
zeroObjRewardChoices &= storm::utility::vector::filterZero(productObjectiveRewards[objIndex]);
}
}
swAux1.stop();
swAux2.start();
storm::storage::BitVector allProductStates(productModel->getProduct().getNumberOfStates(), true);
// Get the relevant states for this epoch.
storm::storage::BitVector productInStates = productModel->computeInStates(epoch);
storm::storage::BitVector productInStates = productModel->getInStates(epochClass);
// 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, productInStates, allProductStates, ~allProductStates);
// std::cout << "numInStates = " << productInStates.getNumberOfSetBits() << std::endl;
@ -414,11 +434,22 @@ namespace storm {
}
epochModel.objectiveRewards.clear();
for (auto const& productObjRew : productObjectiveRewards) {
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> reducedModelObjRewards;
reducedModelObjRewards.reserve(epochModel.epochMatrix.getRowCount());
for (auto const& productChoice : epochModelToProductChoiceMap) {
reducedModelObjRewards.push_back(productObjRew[productChoice]);
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]);
}
}
epochModel.objectiveRewards.push_back(std::move(reducedModelObjRewards));
}
@ -437,6 +468,12 @@ namespace storm {
}
productStateToEpochModelInStateMap = std::make_shared<std::vector<uint64_t> const>(std::move(toEpochModelInStatesMap));
epochModel.objectiveRewardFilter.clear();
for (auto const& objRewards : epochModel.objectiveRewards) {
epochModel.objectiveRewardFilter.push_back(storm::utility::vector::filterZero(objRewards));
epochModel.objectiveRewardFilter.back().complement();
}
swAux4.stop();
swSetEpochClass.stop();
epochModelSizes.push_back(epochModel.epochMatrix.getRowGroupCount());

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

@ -23,6 +23,7 @@ namespace storm {
public:
typedef typename EpochManager::Epoch Epoch; // The number of reward steps that are "left" for each dimension
typedef typename EpochManager::EpochClass EpochClass;
typedef typename std::conditional<SingleObjectiveMode, ValueType, std::vector<ValueType>>::type SolutionType;

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

@ -17,11 +17,11 @@ namespace storm {
namespace multiobjective {
template<typename ValueType>
ProductModel<ValueType>::ProductModel(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<storm::storage::BitVector> const& objectiveDimensions, EpochManager const& epochManager, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<Epoch> const& originalModelSteps) : objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateMap(std::move(memoryStateMap)) {
ProductModel<ValueType>::ProductModel(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<Dimension<ValueType>> const& dimensions, std::vector<storm::storage::BitVector> const& objectiveDimensions, EpochManager const& epochManager, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<Epoch> const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateMap(std::move(memoryStateMap)) {
storm::storage::SparseModelMemoryProduct<ValueType> productBuilder(memory.product(model));
setReachableStates(productBuilder, originalModelSteps);
setReachableProductStates(productBuilder, originalModelSteps);
product = productBuilder.build()->template as<storm::models::sparse::Mdp<ValueType>>();
uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates();
@ -71,52 +71,97 @@ namespace storm {
}
}
}
computeReachableStatesInEpochClasses();
}
template<typename ValueType>
void ProductModel<ValueType>::setReachableStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps) const {
void ProductModel<ValueType>::setReachableProductStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps) const {
storm::storage::BitVector lowerBoundedDimensions(dimensions.size(), false);
for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
if (!dimensions[dim].isUpperBounded) {
lowerBoundedDimensions.set(dim);
}
}
// We add additional reachable states until no more states are found
std::vector<storm::storage::BitVector> additionalReachableStates(memoryStateMap.size(), storm::storage::BitVector(productBuilder.getOriginalModel().getNumberOfStates(), false));
for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) {
auto const& memStateBv = memoryStateMap[memState];
storm::storage::BitVector consideredObjectives(objectiveDimensions.size(), false);
do {
storm::storage::BitVector memStatePrimeBv = memStateBv;
for (auto const& objIndex : consideredObjectives) {
memStatePrimeBv &= ~objectiveDimensions[objIndex];
}
if (memStatePrimeBv != memStateBv) {
for (uint64_t choice = 0; choice < productBuilder.getOriginalModel().getTransitionMatrix().getRowCount(); ++choice) {
bool consideredChoice = true;
bool converged = false;
while (!converged) {
for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) {
auto const& memStateBv = memoryStateMap[memState];
storm::storage::BitVector consideredObjectives(objectiveDimensions.size(), false);
do {
// The current set of considered objectives can be skipped if it contains an objective that only consists of dimensions with lower reward bounds
bool skipThisObjectiveSet = false;
for (auto const& objindex : consideredObjectives) {
if (objectiveDimensions[objindex].isSubsetOf(lowerBoundedDimensions)) {
skipThisObjectiveSet = true;
}
}
if (!skipThisObjectiveSet) {
storm::storage::BitVector memStatePrimeBv = memStateBv;
for (auto const& objIndex : consideredObjectives) {
bool objectiveHasStep = false;
for (auto const& dim : objectiveDimensions[objIndex]) {
if (epochManager.getDimensionOfEpoch(originalModelSteps[choice], dim) > 0) {
objectiveHasStep = true;
break;
memStatePrimeBv &= ~objectiveDimensions[objIndex];
}
if (memStatePrimeBv != memStateBv) {
uint64_t memStatePrime = convertMemoryState(memStatePrimeBv);
for (uint64_t choice = 0; choice < productBuilder.getOriginalModel().getTransitionMatrix().getRowCount(); ++choice) {
// Consider the choice only if for every considered objective there is one dimension for which the step of this choice is positive
bool consideredChoice = true;
for (auto const& objIndex : consideredObjectives) {
bool objectiveHasStep = false;
auto upperBoundedObjectiveDimensions = objectiveDimensions[objIndex] & (~lowerBoundedDimensions);
for (auto const& dim : upperBoundedObjectiveDimensions) {
if (epochManager.getDimensionOfEpoch(originalModelSteps[choice], dim) > 0) {
objectiveHasStep = true;
break;
}
}
if (!objectiveHasStep) {
consideredChoice = false;
break;
}
}
if (consideredChoice) {
for (auto const& successor : productBuilder.getOriginalModel().getTransitionMatrix().getRow(choice)) {
if (productBuilder.isStateReachable(successor.getColumn(), memState) && !productBuilder.isStateReachable(successor.getColumn(), memStatePrime)) {
additionalReachableStates[memStatePrime].set(successor.getColumn());
}
}
}
}
if (!objectiveHasStep) {
consideredChoice = false;
break;
}
}
if (consideredChoice) {
for (auto const& successor : productBuilder.getOriginalModel().getTransitionMatrix().getRow(choice)) {
if (productBuilder.isStateReachable(successor.getColumn(), memState)) {
additionalReachableStates[convertMemoryState(memStatePrimeBv)].set(successor.getColumn());
}
}
consideredObjectives.increment();
} while (!consideredObjectives.empty());
}
storm::storage::BitVector consideredDimensions(dimensions.size(), false);
do {
if (consideredDimensions.isSubsetOf(lowerBoundedDimensions)) {
for (uint64_t memoryState = 0; memoryState < productBuilder.getMemory().getNumberOfStates(); ++memoryState) {
uint64_t memoryStatePrime = convertMemoryState(convertMemoryState(memoryState) | consideredDimensions);
for (uint64_t modelState = 0; modelState < productBuilder.getOriginalModel().getNumberOfStates(); ++modelState) {
if (productBuilder.isStateReachable(modelState, memoryState) && !productBuilder.isStateReachable(modelState, memoryStatePrime)) {
additionalReachableStates[memoryStatePrime].set(modelState);
}
}
}
}
consideredObjectives.increment();
} while (!consideredObjectives.empty());
}
for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) {
for (auto const& modelState : additionalReachableStates[memState]) {
productBuilder.addReachableState(modelState, memState);
consideredDimensions.increment();
} while (!consideredDimensions.empty());
converged = true;
for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) {
if (!additionalReachableStates[memState].empty()) {
converged = false;
for (auto const& modelState : additionalReachableStates[memState]) {
productBuilder.addReachableState(modelState, memState);
}
additionalReachableStates[memState].clear();
}
}
}
}
@ -178,7 +223,7 @@ namespace storm {
}
template<typename ValueType>
std::vector<std::vector<ValueType>> ProductModel<ValueType>::computeObjectiveRewards(Epoch const& epoch, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives, std::vector<Dimension<ValueType>> const& dimensions) const {
std::vector<std::vector<ValueType>> ProductModel<ValueType>::computeObjectiveRewards(EpochClass const& epochClass, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) const {
std::vector<std::vector<ValueType>> objectiveRewards;
objectiveRewards.reserve(objectives.size());
@ -208,10 +253,10 @@ namespace storm {
while (!relevantObjectives.full()) {
relevantObjectives.increment();
// find out whether objective reward should be earned within this epoch
// 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.isBottomDimension(epoch, dimensionIndexMap[subObjIndex])) {
if (dimensions[dimensionIndexMap[subObjIndex]].isUpperBounded == epochManager.isBottomDimensionEpochClass(epochClass, dimensionIndexMap[subObjIndex])) {
collectRewardInEpoch = false;
break;
}
@ -252,7 +297,7 @@ namespace storm {
bool rewardCollectedInEpoch = true;
if (formula.getSubformula().isCumulativeRewardFormula()) {
assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1);
rewardCollectedInEpoch = !epochManager.isBottomDimension(epoch, *objectiveDimensions[objIndex].begin());
rewardCollectedInEpoch = !epochManager.isBottomDimensionEpochClass(epochClass, *objectiveDimensions[objIndex].begin());
} else {
STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula);
}
@ -270,115 +315,157 @@ namespace storm {
}
template<typename ValueType>
storm::storage::BitVector ProductModel<ValueType>::computeInStates(Epoch const& epoch) const {
storm::storage::SparseMatrix<ValueType> const& productMatrix = getProduct().getTransitionMatrix();
storm::storage::BitVector const& ProductModel<ValueType>::getInStates(EpochClass const& epochClass) const {
STORM_LOG_ASSERT(inStates.find(epochClass) != inStates.end(), "Could not find InStates for the given epoch class");
return inStates.find(epochClass)->second;
}
template<typename ValueType>
void ProductModel<ValueType>::computeReachableStatesInEpochClasses() {
std::set<Epoch> possibleSteps(steps.begin(), steps.end());
std::set<EpochClass, std::function<bool(EpochClass const&, EpochClass const&)>> reachableEpochClasses(std::bind(&EpochManager::epochClassOrder, &epochManager, std::placeholders::_1, std::placeholders::_2));
// Initialize the result. Initial states are only considered if the epoch contains no bottom dimension.
storm::storage::BitVector result;
if (epochManager.hasBottomDimension(epoch)) {
result = storm::storage::BitVector(getProduct().getNumberOfStates());
} else {
result = getProduct().getInitialStates();
std::vector<Epoch> candidates({epochManager.getBottomEpoch()});
std::set<Epoch> newCandidates;
bool converged = false;
while (!converged) {
converged = true;
for (auto const& candidate : candidates) {
converged &= !reachableEpochClasses.insert(epochManager.getEpochClass(candidate)).second;
for (auto const& step : possibleSteps) {
epochManager.gatherPredecessorEpochs(newCandidates, candidate, step);
}
}
candidates.assign(newCandidates.begin(), newCandidates.end());
newCandidates.clear();
}
// Compute the set of objectives that can not be satisfied anymore in the current epoch
storm::storage::BitVector irrelevantObjectives(objectiveDimensions.size(), false);
for (uint64_t objIndex = 0; objIndex < objectiveDimensions.size(); ++objIndex) {
bool objIrrelevant = true;
for (auto const& dim : objectiveDimensions[objIndex]) {
if (!epochManager.isBottomDimension(epoch, dim)) {
objIrrelevant = false;
for (auto epochClassIt = reachableEpochClasses.rbegin(); epochClassIt != reachableEpochClasses.rend(); ++epochClassIt) {
std::vector<EpochClass> predecessors;
for (auto predecessorIt = reachableEpochClasses.rbegin(); predecessorIt != epochClassIt; ++predecessorIt) {
if (epochManager.isPredecessorEpochClass(*predecessorIt, *epochClassIt)) {
predecessors.push_back(*predecessorIt);
}
}
if (objIrrelevant) {
irrelevantObjectives.set(objIndex, true);
computeReachableStates(*epochClassIt, predecessors);
}
}
template<typename ValueType>
void ProductModel<ValueType>::computeReachableStates(EpochClass const& epochClass, std::vector<EpochClass> const& predecessors) {
storm::storage::BitVector bottomDimensions(epochManager.getDimensionCount(), false);
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) {
bottomDimensions.set(dim, true);
}
}
// Perform DFS
storm::storage::BitVector reachableStates = getProduct().getInitialStates();
std::vector<uint_fast64_t> stack(reachableStates.begin(), reachableStates.end());
storm::storage::BitVector nonBottomDimensions = ~bottomDimensions;
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 = getSteps()[choice];
if (!epochManager.isZeroEpoch(choiceStep)) {
// Compute the set of objectives that might or might not become irrelevant when the epoch is reached via the current choice
storm::storage::BitVector maybeIrrelevantObjectives(objectiveDimensions.size(), false);
for (uint64_t objIndex = 0; objIndex < objectiveDimensions.size(); ++objIndex) {
for (auto const& dim : objectiveDimensions[objIndex]) {
if (epochManager.isBottomDimension(epoch, dim) && epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) {
maybeIrrelevantObjectives.set(objIndex);
break;
}
}
// Bottom dimensions corresponding to upper bounded subobjectives can not be relevant anymore
// Dimensions with a lower bound where the epoch class is not bottom should stay relevant
storm::storage::BitVector allowedRelevantDimensions(epochManager.getDimensionCount(), true);
storm::storage::BitVector forcedRelevantDimensions(epochManager.getDimensionCount(), false);
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (dimensions[dim].isUpperBounded && bottomDimensions.get(dim)) {
allowedRelevantDimensions.set(dim, false);
} else if (!dimensions[dim].isUpperBounded && nonBottomDimensions.get(dim)) {
forcedRelevantDimensions.set(dim, false);
}
}
assert(forcedRelevantDimensions.isSubsetOf(allowedRelevantDimensions));
storm::storage::BitVector ecInStates(getProduct().getNumberOfStates(), false);
if (!epochManager.hasBottomDimensionEpochClass(epochClass)) {
for (auto const& initState : getProduct().getInitialStates()) {
uint64_t transformedInitState = transformProductState(initState, allowedRelevantDimensions, forcedRelevantDimensions);
ecInStates.set(transformedInitState, true);
}
}
for (auto const& predecessor : predecessors) {
storm::storage::BitVector positiveStepDimensions(epochManager.getDimensionCount(), false);
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (!epochManager.isBottomDimensionEpochClass(predecessor, dim) && bottomDimensions.get(dim)) {
positiveStepDimensions.set(dim, true);
}
}
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;
}
maybeIrrelevantObjectives &= ~irrelevantObjectives;
// For optimization purposes, we treat the case that all objectives will be relevant seperately
if (maybeIrrelevantObjectives.empty() && irrelevantObjectives.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 {
// Enumerate all possible combinations of maybe relevant objectives
storm::storage::BitVector maybeObjSubset(maybeIrrelevantObjectives.getNumberOfSetBits(), false);
do {
for (auto const& choiceSuccessor : productMatrix.getRow(choice)) {
// Compute the successor memory state for the current objective-subset and transition
storm::storage::BitVector successorMemoryState = convertMemoryState(getMemoryState(choiceSuccessor.getColumn()));
// Unselect dimensions belonging to irrelevant objectives
for (auto const& irrelevantObjIndex : irrelevantObjectives) {
successorMemoryState &= ~objectiveDimensions[irrelevantObjIndex];
}
// Unselect objectives that are not in the current subset of maybe relevant objectives
// We can skip a subset if it selects an objective that is irrelevant anyway (according to the original successor memorystate).
bool skipThisSubSet = false;
uint64_t i = 0;
for (auto const& objIndex : maybeIrrelevantObjectives) {
if (maybeObjSubset.get(i)) {
if (successorMemoryState.isDisjointFrom(objectiveDimensions[objIndex])) {
skipThisSubSet = true;
break;
} else {
successorMemoryState &= ~objectiveDimensions[objIndex];
}
}
++i;
}
if (!skipThisSubSet) {
uint64_t successorState = getProductState(getModelState(choiceSuccessor.getColumn()), convertMemoryState(successorMemoryState));
result.set(successorState, true);
if (!reachableStates.get(successorState)) {
reachableStates.set(successorState);
stack.push_back(successorState);
}
}
}
maybeObjSubset.increment();
} while (!maybeObjSubset.empty());
}
if (choiceLeadsToThisClass) {
for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) {
uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions);
ecInStates.set(successorState, true);
}
} else {
for (auto const& choiceSuccessor : productMatrix.getRow(choice)) {
if (!reachableStates.get(choiceSuccessor.getColumn())) {
reachableStates.set(choiceSuccessor.getColumn());
stack.push_back(choiceSuccessor.getColumn());
}
}
}
}
// Find all states reachable from an InState via DFS.
storm::storage::BitVector ecReachableStates = ecInStates;
std::vector<uint64_t> dfsStack(ecReachableStates.begin(), ecReachableStates.end());
while (!dfsStack.empty()) {
uint64_t currentState = dfsStack.back();
dfsStack.pop_back();
for (uint64_t choice = getProduct().getTransitionMatrix().getRowGroupIndices()[currentState]; choice != getProduct().getTransitionMatrix().getRowGroupIndices()[currentState + 1]; ++choice) {
bool choiceLeadsOutsideOfEpoch = false;
Epoch const& choiceStep = getSteps()[choice];
for (auto const& dim : nonBottomDimensions) {
if (epochManager.getDimensionOfEpoch(choiceStep, dim) > 0) {
choiceLeadsOutsideOfEpoch = true;
}
}
for (auto const& transition : getProduct().getTransitionMatrix().getRow(choice)) {
uint64_t successorState = transformProductState(transition.getColumn(), allowedRelevantDimensions, forcedRelevantDimensions);
if (choiceLeadsOutsideOfEpoch) {
ecInStates.set(successorState, true);
}
if (!ecReachableStates.get(successorState)) {
ecReachableStates.set(successorState, true);
dfsStack.push_back(successorState);
}
}
}
}
return result;
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;
}
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>;

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

@ -21,8 +21,10 @@ namespace storm {
public:
typedef typename EpochManager::Epoch Epoch;
typedef typename EpochManager::EpochClass EpochClass;
ProductModel(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<storm::storage::BitVector> const& objectiveDimensions, EpochManager const& epochManager, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<Epoch> const& originalModelSteps);
ProductModel(storm::models::sparse::Mdp<ValueType> const& model, storm::storage::MemoryStructure const& memory, std::vector<Dimension<ValueType>> const& dimensions, std::vector<storm::storage::BitVector> const& objectiveDimensions, EpochManager const& epochManager, std::vector<storm::storage::BitVector>&& memoryStateMap, std::vector<Epoch> const& originalModelSteps);
storm::models::sparse::Mdp<ValueType> const& getProduct() const;
std::vector<Epoch> const& getSteps() const;
@ -39,19 +41,27 @@ namespace storm {
uint64_t getProductStateFromChoice(uint64_t const& productChoice) const;
std::vector<std::vector<ValueType>> computeObjectiveRewards(Epoch const& epoch, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives, std::vector<Dimension<ValueType>> const& dimensions) const;
storm::storage::BitVector computeInStates(Epoch const& epoch) const;
std::vector<std::vector<ValueType>> computeObjectiveRewards(EpochClass const& epochClass, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives) const;
storm::storage::BitVector const& getInStates(EpochClass const& epochClass) const;
private:
void setReachableStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps) const;
void setReachableProductStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps) const;
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;
EpochManager const& epochManager;
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> product;
std::vector<Epoch> steps;
std::map<EpochClass, storm::storage::BitVector> reachableStates;
std::map<EpochClass, storm::storage::BitVector> inStates;
std::vector<uint64_t> modelMemoryToProductStateMap;
std::vector<uint64_t> productToModelStateMap;

20
src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
View File

@ -18,6 +18,10 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small
std::string formulasAsString = "Pmax=? [ F{\"r\"}<=1 x=N ] ";
formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]";
formulasAsString += "; \n Pmin=? [ multi( F{\"r\"}<=1 x=N, F{\"l\"}<=2 x=0 )]";
formulasAsString += "; \n Pmax=? [ F{\"r\"}>=1 x=N ] ";
formulasAsString += "; \n Pmax=? [ F{\"r\"}>=3 x=N ] ";
formulasAsString += "; \n Pmin=? [ F{\"r\"}>=2 x=N ] ";
formulasAsString += "; \n Pmax=? [ multi( F{\"r\"}>=1 x=N, F{\"l\"}>=2 x=0 )]";
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);
@ -39,6 +43,22 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_small
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[3], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[4], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[5], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(0.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask<storm::RationalNumber>(formulas[6], true));
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
EXPECT_EQ(storm::utility::convertNumber<storm::RationalNumber>(1.0), result->asExplicitQuantitativeCheckResult<storm::RationalNumber>()[initState]);
}
TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_large) {

Write Preview
Loading…
Cancel
Save