diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 3b2f2999b..8ef7be0a9 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -121,7 +121,7 @@ namespace storm { } Formula const& BoundedUntilFormula::getRightSubformula() const { - STORM_LOG_ASSERT(leftSubformula.size() == 1, "The right subformula is not unique."); + STORM_LOG_ASSERT(rightSubformula.size() == 1, "The right subformula is not unique."); return *rightSubformula.at(0); } @@ -323,10 +323,10 @@ namespace storm { if (this->isMultiDimensional()) { out << "]"; } + + this->getRightSubformula().writeToStream(out); } - - this->getRightSubformula().writeToStream(out); return out; } } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp new file mode 100644 index 000000000..df1411ea7 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.cpp @@ -0,0 +1,74 @@ +#include "storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h" + +#include "storm/utility/macros.h" + +#include "storm/exceptions/IllegalArgumentException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + MemoryStateManager::MemoryStateManager(uint64_t dimensionCount) : dimensionCount(dimensionCount), dimensionBitMask(1ull), relevantBitsMask((1ull << dimensionCount) - 1), stateCount(dimensionBitMask << dimensionCount) { + STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked MemoryStateManager with zero dimension count."); + STORM_LOG_THROW(dimensionCount <= 64, storm::exceptions::IllegalArgumentException, "Invoked MemoryStateManager with too many dimensions."); + } + + uint64_t const& MemoryStateManager::getDimensionCount() const { + return dimensionCount; + } + + uint64_t const& MemoryStateManager::getMemoryStateCount() const { + return stateCount; + } + + MemoryStateManager::MemoryState MemoryStateManager::getInitialMemoryState() const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); + return relevantBitsMask; + } + + bool MemoryStateManager::isRelevantDimension(MemoryState const& state, uint64_t dimension) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); + return (state & (dimensionBitMask << dimension)) != 0; + } + + void MemoryStateManager::setRelevantDimension(MemoryState& state, uint64_t dimension, bool value) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); + STORM_LOG_ASSERT(dimension < dimensionCount, "Tried to set a dimension that is larger then the number of considered dimensions"); + if (value) { + state |= (dimensionBitMask << dimension); + } else { + state &= ~(dimensionBitMask << dimension); + } + assert(state < getMemoryStateCount()); + } + + void MemoryStateManager::setRelevantDimensions(MemoryState& state, storm::storage::BitVector const& dimensions, bool value) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count."); + STORM_LOG_ASSERT(dimensions.size() == dimensionCount, "Invalid size of given bitset."); + if (value) { + for (auto const& d : dimensions) { + state |= (dimensionBitMask << d); + } + } else { + for (auto const& d : dimensions) { + state &= ~(dimensionBitMask << d); + } + } + assert(state < getMemoryStateCount()); + } + + std::string MemoryStateManager::toString(MemoryState const& state) const { + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + std::string res = "["; + res += (isRelevantDimension(state, 0) ? "1" : "0"); + for (uint64_t d = 1; d < dimensionCount; ++d) { + res += ", "; + res += (isRelevantDimension(state, d) ? "1" : "0"); + } + res += "]"; + return res; + } + + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h new file mode 100644 index 000000000..db3ef06ad --- /dev/null +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h @@ -0,0 +1,40 @@ +#pragma once + +#include +#include +#include + +#include "storm/storage/BitVector.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + + class MemoryStateManager { + public: + + typedef uint64_t MemoryState; + + MemoryStateManager(uint64_t dimensionCount); + + uint64_t const& getDimensionCount() const; + uint64_t const& getMemoryStateCount() const; + + MemoryState getInitialMemoryState() const; + bool isRelevantDimension(MemoryState const& state, uint64_t dimension) const; + void setRelevantDimension(MemoryState& state, uint64_t dimension, bool value = true) const; + void setRelevantDimensions(MemoryState& state, storm::storage::BitVector const& dimensions, bool value = true) const; + + std::string toString(MemoryState const& state) const; + + private: + uint64_t const dimensionCount; + uint64_t const dimensionBitMask; + uint64_t const relevantBitsMask; + uint64_t const stateCount; + + }; + } + } +} \ No newline at end of file diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index c09ee91f5..3a2c427ff 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -6,7 +6,6 @@ #include "storm/utility/macros.h" #include "storm/logic/Formulas.h" -#include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -83,7 +82,10 @@ namespace storm { } dimension.memoryLabel = memLabel; dimension.isUpperBounded = subformula.hasUpperBound(dim); + // for simplicity we do not allow intervals or unbounded formulas. STORM_LOG_THROW(subformula.hasLowerBound(dim) != dimension.isUpperBounded, storm::exceptions::NotSupportedException, "Bounded until formulas are only supported by this method if they consider either an upper bound or a lower bound. Got " << subformula << " instead."); + // lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the ProductModel::transformMemoryState method). + STORM_LOG_THROW(dimension.isUpperBounded || subformula.getLeftSubformula(dim).isTrueFormula(), storm::exceptions::NotSupportedException, "Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got " << subformula << " instead."); if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) { dimensionWiseEpochSteps.push_back(std::vector(model.getNumberOfChoices(), 1)); dimension.scalingFactor = storm::utility::one(); @@ -124,12 +126,11 @@ namespace storm { for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) { if (!boundedUntilFormula.hasMultiDimensionalSubformulas() || dimensions[currDim].isUpperBounded) { dimensions[currDim].dependentDimensions = objDimensions; - std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl; } else { dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false); dimensions[currDim].dependentDimensions.set(currDim, true); - std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl; } + // std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl; } dim += boundedUntilFormula.getDimension(); } else if (objectives[objIndex].formula->isRewardOperatorFormula() && objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) { @@ -138,7 +139,6 @@ namespace storm { ++dim; } - std::cout << "obj " << objIndex << " has dimensions " << objDimensions << std::endl; objectiveDimensions.push_back(std::move(objDimensions)); } assert(dim == dimensions.size()); @@ -172,14 +172,7 @@ namespace storm { template void MultiDimensionalRewardUnfolding::initializeMemoryProduct(std::vector const& epochSteps) { - - // build the memory structure - auto memoryStructure = computeMemoryStructure(); - - // build a mapping between the different representations of memory states - auto memoryStateMap = computeMemoryStateMap(memoryStructure); - - productModel = std::make_unique>(model, memoryStructure, dimensions, objectiveDimensions, epochManager, std::move(memoryStateMap), epochSteps); + productModel = std::make_unique>(model, objectives, dimensions, objectiveDimensions, epochManager, epochSteps); } template @@ -205,6 +198,7 @@ namespace storm { } STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::NotSupportedException, "The bound " << bound << " contains undefined constants."); ValueType discretizedBound = storm::utility::convertNumber(bound.evaluateAsRational()); + STORM_LOG_THROW(dimensions[dim].isUpperBounded || isStrict || !storm::utility::isZero(discretizedBound), storm::exceptions::NotSupportedException, "Lower bounds need to be either strict or greater than zero."); discretizedBound /= dimensions[dim].scalingFactor; if (storm::utility::isInteger(discretizedBound)) { if (isStrict == dimensions[dim].isUpperBounded) { @@ -296,18 +290,17 @@ namespace storm { uint64_t productChoice = epochModelToProductChoiceMap[reducedChoice]; uint64_t productState = productModel->getProductStateFromChoice(productChoice); auto const& memoryState = productModel->getMemoryState(productState); - auto const& memoryStateBv = productModel->convertMemoryState(memoryState); Epoch successorEpoch = epochManager.getSuccessorEpoch(epoch, productModel->getSteps()[productChoice]); EpochClass successorEpochClass = epochManager.getEpochClass(successorEpoch); // Find out whether objective reward is earned for the current 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 + // 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) { 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) && memoryStateBv.get(dim)) { + if (dimensions[dim].isUpperBounded == epochManager.isBottomDimension(successorEpoch, dim) && productModel->getMemoryStateManager().isRelevantDimension(memoryState, dim)) { rewardEarned = false; break; } @@ -583,129 +576,15 @@ namespace storm { template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch) { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "The model has multiple initial states."); - STORM_LOG_ASSERT(productModel->getProduct().getInitialStates().getNumberOfSetBits() == 1, "The product has multiple initial states."); - return getStateSolution(epoch, *productModel->getProduct().getInitialStates().begin()); + STORM_LOG_ASSERT(!epochManager.hasBottomDimension(epoch), "Tried to get the initial state result in an epoch that still contains at least one bottom dimension."); + return getStateSolution(epoch, productModel->getInitialProductState(*model.getInitialStates().begin(), model.getInitialStates())); } template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex) { STORM_LOG_ASSERT(model.getInitialStates().get(initialStateIndex), "The given model state is not an initial state."); - for (uint64_t memState = 0; memState < productModel->getNumberOfMemoryState(); ++memState) { - uint64_t productState = productModel->getProductState(initialStateIndex, memState); - if (productModel->getProduct().getInitialStates().get(productState)) { - return getStateSolution(epoch, productState); - } - } - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not find the initial product state corresponding to the given initial model state."); - return getStateSolution(epoch, -1ull); - } - - template - storm::storage::MemoryStructure MultiDimensionalRewardUnfolding::computeMemoryStructure() const { - - storm::modelchecker::SparsePropositionalModelChecker> mc(model); - - // Create a memory structure that remembers whether (sub)objectives are satisfied - storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); - for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - if (!objectives[objIndex].formula->isProbabilityOperatorFormula()) { - continue; - } - - std::vector dimensionIndexMap; - for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { - dimensionIndexMap.push_back(globalDimensionIndex); - } - - // collect the memory states for this objective - std::vector objMemStates; - storm::storage::BitVector m(dimensionIndexMap.size(), false); - for (; !m.full(); m.increment()) { - objMemStates.push_back(~m); - } - objMemStates.push_back(~m); - assert(objMemStates.size() == 1ull << dimensionIndexMap.size()); - - // build objective memory - auto objMemoryBuilder = storm::storage::MemoryStructureBuilder(objMemStates.size(), model); - - // Get the set of states that for all subobjectives satisfy either the left or the right subformula - storm::storage::BitVector constraintStates(model.getNumberOfStates(), true); - for (auto const& dim : objectiveDimensions[objIndex]) { - auto const& dimension = dimensions[dim]; - STORM_LOG_ASSERT(dimension.formula->isBoundedUntilFormula(), "Unexpected Formula type"); - constraintStates &= - (mc.check(dimension.formula->asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector() | - mc.check(dimension.formula->asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); - } - - // Build the transitions between the memory states - for (uint64_t memState = 0; memState < objMemStates.size(); ++memState) { - auto const& memStateBV = objMemStates[memState]; - for (uint64_t memStatePrime = 0; memStatePrime < objMemStates.size(); ++memStatePrime) { - auto const& memStatePrimeBV = objMemStates[memStatePrime]; - if (memStatePrimeBV.isSubsetOf(memStateBV)) { - - std::shared_ptr transitionFormula = storm::logic::Formula::getTrueFormula(); - for (auto const& subObjIndex : memStateBV) { - std::shared_ptr subObjFormula = dimensions[dimensionIndexMap[subObjIndex]].formula->asBoundedUntilFormula().getRightSubformula().asSharedPointer(); - if (memStatePrimeBV.get(subObjIndex)) { - subObjFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subObjFormula); - } - transitionFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, transitionFormula, subObjFormula); - } - - storm::storage::BitVector transitionStates = mc.check(*transitionFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - if (memStatePrimeBV.empty()) { - transitionStates |= ~constraintStates; - } else { - transitionStates &= constraintStates; - } - objMemoryBuilder.setTransition(memState, memStatePrime, transitionStates); - - // Set the initial states - if (memStateBV.full()) { - storm::storage::BitVector initialTransitionStates = model.getInitialStates() & transitionStates; - // At this point we can check whether there is an initial state that already satisfies all subObjectives. - // Such a situation is not supported as we can not reduce this (easily) to an expected reward computation. - STORM_LOG_THROW(!memStatePrimeBV.empty() || initialTransitionStates.empty() || initialTransitionStates.isDisjointFrom(constraintStates), storm::exceptions::NotSupportedException, "The objective " << *objectives[objIndex].formula << " is already satisfied in an initial state. This special case is not supported."); - for (auto const& initState : initialTransitionStates) { - objMemoryBuilder.setInitialMemoryState(initState, memStatePrime); - } - } - } - } - } - - // Build the memory labels - for (uint64_t memState = 0; memState < objMemStates.size(); ++memState) { - auto const& memStateBV = objMemStates[memState]; - for (auto const& subObjIndex : memStateBV) { - objMemoryBuilder.setLabel(memState, dimensions[dimensionIndexMap[subObjIndex]].memoryLabel.get()); - } - } - auto objMemory = objMemoryBuilder.build(); - memory = memory.product(objMemory); - } - return memory; - } - - template - std::vector MultiDimensionalRewardUnfolding::computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const { - // Compute a mapping between the different representations of memory states - std::vector result; - result.reserve(memory.getNumberOfStates()); - for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { - storm::storage::BitVector relevantSubObjectives(epochManager.getDimensionCount(), false); - std::set stateLabels = memory.getStateLabeling().getLabelsOfState(memState); - for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { - if (dimensions[dim].memoryLabel && stateLabels.find(dimensions[dim].memoryLabel.get()) != stateLabels.end()) { - relevantSubObjectives.set(dim, true); - } - } - result.push_back(std::move(relevantSubObjectives)); - } - return result; + STORM_LOG_ASSERT(!epochManager.hasBottomDimension(epoch), "Tried to get the initial state result in an epoch that still contains at least one bottom dimension."); + return getStateSolution(epoch, productModel->getInitialProductState(initialStateIndex, model.getInitialStates())); } template class MultiDimensionalRewardUnfolding; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index 377a99a9b..a8f06178e 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -90,8 +90,6 @@ namespace storm { void initializeMemoryProduct(std::vector const& epochSteps); - storm::storage::MemoryStructure computeMemoryStructure() const; - std::vector computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; template::type = 0> SolutionType getScaledSolution(SolutionType const& solution, ValueType const& scalingFactor) const; diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp index fd42f6112..f5e8409f9 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp @@ -5,6 +5,7 @@ #include "storm/logic/Formulas.h" #include "storm/logic/CloneVisitor.h" #include "storm/storage/memorystructure/SparseModelMemoryProduct.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -17,15 +18,19 @@ namespace storm { namespace multiobjective { template - ProductModel::ProductModel(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector&& memoryStateMap, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateMap(std::move(memoryStateMap)) { + ProductModel::ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) { + + storm::storage::MemoryStructure memory = computeMemoryStructure(model, objectives); + assert(memoryStateManager.getMemoryStateCount() == memory.getNumberOfStates()); + std::vector memoryStateMap = computeMemoryStateMap(memory); storm::storage::SparseModelMemoryProduct productBuilder(memory.product(model)); - setReachableProductStates(productBuilder, originalModelSteps); + setReachableProductStates(productBuilder, originalModelSteps, memoryStateMap); product = productBuilder.build()->template as>(); uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates(); - uint64_t numMemoryStates = productBuilder.getMemory().getNumberOfStates(); + uint64_t numMemoryStates = memoryStateManager.getMemoryStateCount(); uint64_t numProductStates = getProduct().getNumberOfStates(); // Compute a mappings from product states to model/memory states and back @@ -33,12 +38,12 @@ namespace storm { productToModelStateMap.resize(numProductStates, std::numeric_limits::max()); productToMemoryStateMap.resize(numProductStates, std::numeric_limits::max()); for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { - for (uint64_t memoryState = 0; memoryState < numMemoryStates; ++memoryState) { - if (productBuilder.isStateReachable(modelState, memoryState)) { - uint64_t productState = productBuilder.getResultState(modelState, memoryState); - modelMemoryToProductStateMap[modelState * numMemoryStates + memoryState] = productState; + for (uint64_t memoryStateIndex = 0; memoryStateIndex < numMemoryStates; ++memoryStateIndex) { + if (productBuilder.isStateReachable(modelState, memoryStateIndex)) { + uint64_t productState = productBuilder.getResultState(modelState, memoryStateIndex); + modelMemoryToProductStateMap[modelState * numMemoryStates + memoryStateMap[memoryStateIndex]] = productState; productToModelStateMap[productState] = modelState; - productToMemoryStateMap[productState] = memoryState; + productToMemoryStateMap[productState] = memoryStateMap[memoryStateIndex]; } } } @@ -60,9 +65,9 @@ namespace storm { for (uint64_t choiceOffset = 0; choiceOffset < numChoices; ++choiceOffset) { Epoch const& step = originalModelSteps[firstChoice + choiceOffset]; if (step != 0) { - for (uint64_t memState = 0; memState < numMemoryStates; ++memState) { - if (productStateExists(modelState, memState)) { - uint64_t productState = getProductState(modelState, memState); + for (MemoryState const& memoryState : memoryStateMap) { + if (productStateExists(modelState, memoryState)) { + uint64_t productState = getProductState(modelState, memoryState); uint64_t productChoice = getProduct().getTransitionMatrix().getRowGroupIndices()[productState] + choiceOffset; assert(productChoice < getProduct().getTransitionMatrix().getRowGroupIndices()[productState + 1]); steps[productChoice] = step; @@ -71,24 +76,150 @@ namespace storm { } } } + + // getProduct().writeDotToStream(std::cout); + computeReachableStatesInEpochClasses(); } + + template + storm::storage::MemoryStructure ProductModel::computeMemoryStructure(storm::models::sparse::Mdp const& model, std::vector> const& objectives) const { + + storm::modelchecker::SparsePropositionalModelChecker> mc(model); + + // Create a memory structure that remembers whether (sub)objectives are satisfied + storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model); + for (uint64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { + if (!objectives[objIndex].formula->isProbabilityOperatorFormula()) { + continue; + } + + std::vector dimensionIndexMap; + for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { + dimensionIndexMap.push_back(globalDimensionIndex); + } + + bool objectiveContainsLowerBound = false; + for (auto const& globalDimensionIndex : objectiveDimensions[objIndex]) { + if (!dimensions[globalDimensionIndex].isUpperBounded) { + objectiveContainsLowerBound = true; + break; + } + } + + // collect the memory states for this objective + std::vector objMemStates; + storm::storage::BitVector m(dimensionIndexMap.size(), false); + for (; !m.full(); m.increment()) { + objMemStates.push_back(~m); + } + objMemStates.push_back(~m); + assert(objMemStates.size() == 1ull << dimensionIndexMap.size()); + + // build objective memory + auto objMemoryBuilder = storm::storage::MemoryStructureBuilder(objMemStates.size(), model); + + // Get the set of states that for all subobjectives satisfy either the left or the right subformula + storm::storage::BitVector constraintStates(model.getNumberOfStates(), true); + for (auto const& dim : objectiveDimensions[objIndex]) { + auto const& dimension = dimensions[dim]; + STORM_LOG_ASSERT(dimension.formula->isBoundedUntilFormula(), "Unexpected Formula type"); + constraintStates &= + (mc.check(dimension.formula->asBoundedUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector() | + mc.check(dimension.formula->asBoundedUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector()); + } + + // Build the transitions between the memory states + for (uint64_t memState = 0; memState < objMemStates.size(); ++memState) { + auto const& memStateBV = objMemStates[memState]; + for (uint64_t memStatePrime = 0; memStatePrime < objMemStates.size(); ++memStatePrime) { + auto const& memStatePrimeBV = objMemStates[memStatePrime]; + if (memStatePrimeBV.isSubsetOf(memStateBV)) { + + std::shared_ptr transitionFormula = storm::logic::Formula::getTrueFormula(); + for (auto const& subObjIndex : memStateBV) { + std::shared_ptr subObjFormula = dimensions[dimensionIndexMap[subObjIndex]].formula->asBoundedUntilFormula().getRightSubformula().asSharedPointer(); + if (memStatePrimeBV.get(subObjIndex)) { + subObjFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, subObjFormula); + } + transitionFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, transitionFormula, subObjFormula); + } + + storm::storage::BitVector transitionStates = mc.check(*transitionFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + if (memStatePrimeBV.empty()) { + transitionStates |= ~constraintStates; + } else { + transitionStates &= constraintStates; + } + objMemoryBuilder.setTransition(memState, memStatePrime, transitionStates); + + // Set the initial states + if (memStateBV.full()) { + storm::storage::BitVector initialTransitionStates = model.getInitialStates() & transitionStates; + // At this point we can check whether there is an initial state that already satisfies all subObjectives. + // Such a situation is not supported as we can not reduce this (easily) to an expected reward computation. + STORM_LOG_THROW(!memStatePrimeBV.empty() || initialTransitionStates.empty() || objectiveContainsLowerBound || initialTransitionStates.isDisjointFrom(constraintStates), storm::exceptions::NotSupportedException, "The objective " << *objectives[objIndex].formula << " is already satisfied in an initial state. This special case is not supported."); + for (auto const& initState : initialTransitionStates) { + objMemoryBuilder.setInitialMemoryState(initState, memStatePrime); + } + } + } + } + } + + // Build the memory labels + for (uint64_t memState = 0; memState < objMemStates.size(); ++memState) { + auto const& memStateBV = objMemStates[memState]; + for (auto const& subObjIndex : memStateBV) { + objMemoryBuilder.setLabel(memState, dimensions[dimensionIndexMap[subObjIndex]].memoryLabel.get()); + } + } + auto objMemory = objMemoryBuilder.build(); + memory = memory.product(objMemory); + } + return memory; + } + + template + std::vector::MemoryState> ProductModel::computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const { + // Compute a mapping between the different representations of memory states + std::vector result; + result.reserve(memory.getNumberOfStates()); + for (uint64_t memStateIndex = 0; memStateIndex < memory.getNumberOfStates(); ++memStateIndex) { + MemoryState memState = memoryStateManager.getInitialMemoryState(); + std::set stateLabels = memory.getStateLabeling().getLabelsOfState(memStateIndex); + for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) { + if (dimensions[dim].memoryLabel && stateLabels.find(dimensions[dim].memoryLabel.get()) != stateLabels.end()) { + memoryStateManager.setRelevantDimension(memState, dim, true); + } else { + memoryStateManager.setRelevantDimension(memState, dim, false); + } + } + result.push_back(std::move(memState)); + } + return result; + } + template - void ProductModel::setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const { + void ProductModel::setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps, std::vector const& memoryStateMap) const { + std::vector inverseMemoryStateMap(memoryStateMap.size(), std::numeric_limits::max()); + for (uint64_t memStateIndex = 0; memStateIndex < memoryStateMap.size(); ++memStateIndex) { + inverseMemoryStateMap[memoryStateMap[memStateIndex]] = memStateIndex; + } + auto const& memory = productBuilder.getMemory(); auto const& model = productBuilder.getOriginalModel(); auto const& modelTransitions = model.getTransitionMatrix(); - std::vector reachableStates(memory.getNumberOfStates(), storm::storage::BitVector(model.getNumberOfStates(), false)); + std::vector reachableStates(memoryStateManager.getMemoryStateCount(), storm::storage::BitVector(model.getNumberOfStates(), false)); // Initialize the reachable states with the initial states EpochClass initEpochClass = epochManager.getEpochClass(epochManager.getZeroEpoch()); - storm::storage::BitVector initMemState(epochManager.getDimensionCount(), true); auto memStateIt = memory.getInitialMemoryStates().begin(); for (auto const& initState : model.getInitialStates()) { - uint64_t transformedMemoryState = transformMemoryState(*memStateIt, initEpochClass, convertMemoryState(initMemState)); + uint64_t transformedMemoryState = transformMemoryState(memoryStateMap[*memStateIt], initEpochClass, memoryStateManager.getInitialMemoryState()); reachableStates[transformedMemoryState].set(initState, true); ++memStateIt; } @@ -105,8 +236,8 @@ namespace storm { auto const& epochClass = *epochClassIt; // Find the remaining set of reachable states via DFS. - std::vector> dfsStack; - for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++memState) { + std::vector> dfsStack; + for (MemoryState const& memState : memoryStateMap) { for (auto const& modelState : reachableStates[memState]) { dfsStack.emplace_back(modelState, memState); } @@ -114,14 +245,15 @@ namespace storm { while (!dfsStack.empty()) { uint64_t currentModelState = dfsStack.back().first; - uint64_t currentMemoryState = dfsStack.back().second; + MemoryState currentMemoryState = dfsStack.back().second; + uint64_t currentMemoryStateIndex = inverseMemoryStateMap[currentMemoryState]; dfsStack.pop_back(); for (uint64_t choice = modelTransitions.getRowGroupIndices()[currentModelState]; choice != modelTransitions.getRowGroupIndices()[currentModelState + 1]; ++choice) { for (auto transitionIt = modelTransitions.getRow(choice).begin(); transitionIt < modelTransitions.getRow(choice).end(); ++transitionIt) { - uint64_t successorMemoryState = memory.getSuccessorMemoryState(currentMemoryState, transitionIt - modelTransitions.begin()); + MemoryState successorMemoryState = memoryStateMap[memory.getSuccessorMemoryState(currentMemoryStateIndex, transitionIt - modelTransitions.begin())]; successorMemoryState = transformMemoryState(successorMemoryState, epochClass, currentMemoryState); if (!reachableStates[successorMemoryState].get(transitionIt->getColumn())) { reachableStates[successorMemoryState].set(transitionIt->getColumn(), true); @@ -131,9 +263,10 @@ namespace storm { } } } - for (uint64_t memState = 0; memState < memoryStateMap.size(); ++memState) { - for (auto const& modelState : reachableStates[memState]) { - productBuilder.addReachableState(modelState, memState); + + for (uint64_t memStateIndex = 0; memStateIndex < memoryStateManager.getMemoryStateCount(); ++memStateIndex) { + for (auto const& modelState : reachableStates[memoryStateMap[memStateIndex]]) { + productBuilder.addReachableState(modelState, memStateIndex); } } } @@ -149,44 +282,37 @@ namespace storm { } template - bool ProductModel::productStateExists(uint64_t const& modelState, uint64_t const& memoryState) const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve whether a product state exists but the memoryStateMap is not yet initialized."); - return modelMemoryToProductStateMap[modelState * memoryStateMap.size() + memoryState] < getProduct().getNumberOfStates(); + bool ProductModel::productStateExists(uint64_t const& modelState, MemoryState const& memoryState) const { + return modelMemoryToProductStateMap[modelState * memoryStateManager.getMemoryStateCount() + memoryState] < getProduct().getNumberOfStates(); } template - uint64_t ProductModel::getProductState(uint64_t const& modelState, uint64_t const& memoryState) const { + uint64_t ProductModel::getProductState(uint64_t const& modelState, MemoryState const& memoryState) const { STORM_LOG_ASSERT(productStateExists(modelState, memoryState), "Tried to obtain a state in the model-memory-product that does not exist"); - return modelMemoryToProductStateMap[modelState * memoryStateMap.size() + memoryState]; + return modelMemoryToProductStateMap[modelState * memoryStateManager.getMemoryStateCount() + memoryState]; } template - uint64_t ProductModel::getModelState(uint64_t const& productState) const { - return productToModelStateMap[productState]; + uint64_t ProductModel::getInitialProductState(uint64_t const& initialModelState, storm::storage::BitVector const& initialModelStates) const { + auto productInitStateIt = getProduct().getInitialStates().begin(); + productInitStateIt += initialModelStates.getNumberOfSetBitsBeforeIndex(initialModelState); + STORM_LOG_ASSERT(getModelState(*productInitStateIt) == initialModelState, "Could not find the corresponding initial state in the product model."); + return transformProductState(*productInitStateIt, epochManager.getEpochClass(epochManager.getZeroEpoch()), memoryStateManager.getInitialMemoryState()); } template - uint64_t ProductModel::getMemoryState(uint64_t const& productState) const { - return productToMemoryStateMap[productState]; - } - - template - storm::storage::BitVector const& ProductModel::convertMemoryState(uint64_t const& memoryState) const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); - return memoryStateMap[memoryState]; + uint64_t ProductModel::getModelState(uint64_t const& productState) const { + return productToModelStateMap[productState]; } template - uint64_t ProductModel::convertMemoryState(storm::storage::BitVector const& memoryState) const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to convert a memory state, but the memoryStateMap is not yet initialized."); - auto memStateIt = std::find(memoryStateMap.begin(), memoryStateMap.end(), memoryState); - return memStateIt - memoryStateMap.begin(); + typename ProductModel::MemoryState ProductModel::getMemoryState(uint64_t const& productState) const { + return productToMemoryStateMap[productState]; } template - uint64_t ProductModel::getNumberOfMemoryState() const { - STORM_LOG_ASSERT(!memoryStateMap.empty(), "Tried to retrieve the number of memory states but the memoryStateMap is not yet initialized."); - return memoryStateMap.size(); + MemoryStateManager const& ProductModel::getMemoryStateManager() const { + return memoryStateManager; } template @@ -352,9 +478,8 @@ namespace storm { storm::storage::BitVector ecInStates(getProduct().getNumberOfStates(), false); if (!epochManager.hasBottomDimensionEpochClass(epochClass)) { - uint64_t initMemState = convertMemoryState(storm::storage::BitVector(epochManager.getDimensionCount(), true)); for (auto const& initState : getProduct().getInitialStates()) { - uint64_t transformedInitState = transformProductState(initState, epochClass, initMemState); + uint64_t transformedInitState = transformProductState(initState, epochClass, memoryStateManager.getInitialMemoryState()); ecInStates.set(transformedInitState, true); } } @@ -429,30 +554,31 @@ namespace storm { } template - uint64_t ProductModel::transformMemoryState(uint64_t const& memoryState, EpochClass const& epochClass, uint64_t const& predecessorMemoryState) const { - storm::storage::BitVector memoryStateBv = convertMemoryState(memoryState); - storm::storage::BitVector const& predecessorMemoryStateBv = convertMemoryState(predecessorMemoryState); + typename ProductModel::MemoryState ProductModel::transformMemoryState(MemoryState const& memoryState, EpochClass const& epochClass, MemoryState const& predecessorMemoryState) const { + MemoryState memoryStatePrime = memoryState; for (auto const& objDimensions : objectiveDimensions) { for (auto const& dim : objDimensions) { auto const& dimension = dimensions[dim]; bool dimUpperBounded = dimension.isUpperBounded; bool dimBottom = epochManager.isBottomDimensionEpochClass(epochClass, dim); - if (dimUpperBounded && dimBottom && predecessorMemoryStateBv.get(dim)) { + if (dimUpperBounded && dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) { STORM_LOG_ASSERT(objDimensions == dimension.dependentDimensions, "Unexpected set of dependent dimensions"); - memoryStateBv &= ~objDimensions; + memoryStateManager.setRelevantDimensions(memoryStatePrime, objDimensions, false); break; - } else if (!dimUpperBounded && !dimBottom && predecessorMemoryStateBv.get(dim)) { - memoryStateBv |= dimension.dependentDimensions; + } else if (!dimUpperBounded && !dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) { + memoryStateManager.setRelevantDimensions(memoryStatePrime, dimension.dependentDimensions, true); } } } + + // std::cout << "Transformed memory state " << memoryStateManager.toString(memoryState) << " at epoch class " << epochClass << " with predecessor " << memoryStateManager.toString(predecessorMemoryState) << " to " << memoryStateManager.toString(memoryStatePrime) << std::endl; - return convertMemoryState(memoryStateBv); + return memoryStatePrime; } template - uint64_t ProductModel::transformProductState(uint64_t const& productState, EpochClass const& epochClass, uint64_t const& predecessorMemoryState) const { + uint64_t ProductModel::transformProductState(uint64_t const& productState, EpochClass const& epochClass, MemoryState const& predecessorMemoryState) const { return getProductState(getModelState(productState), transformMemoryState(getMemoryState(productState), epochClass, predecessorMemoryState)); } diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h index f030c1812..74918e506 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.h @@ -5,6 +5,7 @@ #include "storm/storage/BitVector.h" #include "storm/modelchecker/multiobjective/Objective.h" #include "storm/modelchecker/multiobjective/rewardbounded/EpochManager.h" +#include "storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h" #include "storm/modelchecker/multiobjective/rewardbounded/Dimension.h" #include "storm/models/sparse/Mdp.h" #include "storm/utility/vector.h" @@ -22,36 +23,38 @@ namespace storm { typedef typename EpochManager::Epoch Epoch; typedef typename EpochManager::EpochClass EpochClass; + typedef typename MemoryStateManager::MemoryState MemoryState; - ProductModel(storm::models::sparse::Mdp const& model, storm::storage::MemoryStructure const& memory, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector&& memoryStateMap, std::vector const& originalModelSteps); + ProductModel(storm::models::sparse::Mdp const& model, std::vector> const& objectives, std::vector> const& dimensions, std::vector const& objectiveDimensions, EpochManager const& epochManager, std::vector const& originalModelSteps); storm::models::sparse::Mdp const& getProduct() const; std::vector const& getSteps() 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 getInitialProductState(uint64_t const& initialModelState, storm::storage::BitVector const& initialModelStates) const; uint64_t getModelState(uint64_t const& productState) const; - uint64_t getMemoryState(uint64_t const& productState) const; - - uint64_t convertMemoryState(storm::storage::BitVector const& memoryState) const; - storm::storage::BitVector const& convertMemoryState(uint64_t const& memoryState) const; - - uint64_t getNumberOfMemoryState() const; + MemoryState getMemoryState(uint64_t const& productState) const; + MemoryStateManager const& getMemoryStateManager() const; uint64_t getProductStateFromChoice(uint64_t const& productChoice) const; std::vector> computeObjectiveRewards(EpochClass const& epochClass, std::vector> const& objectives) const; storm::storage::BitVector const& getInStates(EpochClass const& epochClass) const; - - uint64_t transformMemoryState(uint64_t const& memoryState, EpochClass const& epochClass, uint64_t const& predecessorMemoryState) const; - uint64_t transformProductState(uint64_t const& productState, EpochClass const& epochClass, uint64_t const& predecessorMemoryState) const; + + MemoryState transformMemoryState(MemoryState const& memoryState, EpochClass const& epochClass, MemoryState const& predecessorMemoryState) const; + uint64_t transformProductState(uint64_t const& productState, EpochClass const& epochClass, MemoryState const& predecessorMemoryState) const; private: - void setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps) const; + storm::storage::MemoryStructure computeMemoryStructure(storm::models::sparse::Mdp const& model, std::vector> const& objectives) const; + std::vector computeMemoryStateMap(storm::storage::MemoryStructure const& memory) const; + + + void setReachableProductStates(storm::storage::SparseModelMemoryProduct& productBuilder, std::vector const& originalModelSteps, std::vector const& memoryStateMap) const; void collectReachableEpochClasses(std::set>& reachableEpochClasses, std::set const& possibleSteps) const; @@ -61,6 +64,7 @@ namespace storm { std::vector> const& dimensions; std::vector const& objectiveDimensions; EpochManager const& epochManager; + MemoryStateManager memoryStateManager; std::shared_ptr> product; std::vector steps; @@ -69,9 +73,8 @@ namespace storm { std::vector modelMemoryToProductStateMap; std::vector productToModelStateMap; - std::vector productToMemoryStateMap; + std::vector productToMemoryStateMap; std::vector choiceToStateMap; - std::vector memoryStateMap; }; } diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index ebb126248..025497515 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -213,6 +213,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { std::string formulasAsString = "Pmax=? [ F{\"a\"}>=1.1 x=1 ]"; formulasAsString += "; \n Pmin=? [ F{\"a\"}>=1.1 x=1 ]"; formulasAsString += "; \n Pmax=? [ F{\"b\"}>3 x=1 ]"; + formulasAsString += "; \n Pmax=? [ F{\"b\"}>=2 x=0 ]"; formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}<=0.2 x=1, F{\"b\"}>3 x=1) ]"; formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>0.2 x=1, F{\"b\"}>3 x=1) ]"; formulasAsString += "; \n Pmax=? [ multi(F{\"a\"}>=2/5 x=4, F{\"a\"}<=0 x=4) ]"; @@ -245,16 +246,21 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[3], true)); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - expectedResult = storm::utility::convertNumber("27/64"); + expectedResult = storm::utility::convertNumber("9/16"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[4], true)); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - expectedResult = storm::utility::convertNumber("243/640"); + expectedResult = storm::utility::convertNumber("27/64"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[5], true)); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + expectedResult = storm::utility::convertNumber("243/640"); + EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]); + + result = storm::api::verifyWithSparseEngine(mdp, storm::api::createTask(formulas[6], true)); + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); expectedResult = storm::utility::convertNumber("81/160"); EXPECT_EQ(expectedResult, result->asExplicitQuantitativeCheckResult()[initState]);