From c5f29c37618d8ab74c19db41cf0380aad9a00682 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 26 Apr 2017 10:54:47 +0200 Subject: [PATCH] Fixes and improvements for memory structure --- .../memorystructure/MemoryStructure.cpp | 6 +- .../storage/memorystructure/MemoryStructure.h | 1 + .../SparseModelMemoryProduct.cpp | 93 ++++++++++--------- .../SparseModelMemoryProduct.h | 11 ++- 4 files changed, 62 insertions(+), 49 deletions(-) diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index bbf3137f5..559677ea5 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -18,12 +18,16 @@ namespace storm { } MemoryStructure::TransitionMatrix const& MemoryStructure::getTransitionMatrix() const { - return this->transitions; + return transitions; } storm::models::sparse::StateLabeling const& MemoryStructure::getStateLabeling() const { return stateLabeling; } + + uint_fast64_t MemoryStructure::getNumberOfStates() const { + return transitions.size(); + } MemoryStructure MemoryStructure::product(MemoryStructure const& rhs) const { uint_fast64_t lhsNumStates = this->getTransitionMatrix().size(); diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index 651a54de7..1085b3b5d 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -39,6 +39,7 @@ namespace storm { TransitionMatrix const& getTransitionMatrix() const; storm::models::sparse::StateLabeling const& getStateLabeling() const; + uint_fast64_t getNumberOfStates() const; /*! * Builds the product of this memory structure and the given memory structure. diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 949781c92..f37e380f7 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -23,13 +23,21 @@ namespace storm { template std::shared_ptr> SparseModelMemoryProduct::build() { + uint_fast64_t modelStateCount = model.getNumberOfStates(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); std::vector memorySuccessors = computeMemorySuccessors(); - storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors); + // Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) + storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false); + for (auto const& modelInit : model.getInitialStates()) { + // Note: The initial state of a memory structure is always 0. + initialStates.set(modelInit * memoryStateCount + memorySuccessors[modelInit * memoryStateCount], true); + } + storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates); // Compute the mapping to the states of the result uint_fast64_t reachableStateCount = 0; - toResultStateMapping = std::vector (model.getNumberOfStates() * memory.getTransitionMatrix().size(), std::numeric_limits::max()); + toResultStateMapping = std::vector (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits::max()); for (auto const& reachableState : reachableStates) { toResultStateMapping[reachableState] = reachableStateCount; ++reachableStateCount; @@ -42,20 +50,23 @@ namespace storm { storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); + // Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states. + labeling.addLabel("init", initialStates % reachableStates); + return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); } template - uint_fast64_t const& SparseModelMemoryProduct::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) { - return toResultStateMapping[modelState * memory.getTransitionMatrix().size() + memoryState]; + uint_fast64_t const& SparseModelMemoryProduct::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const { + return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } template std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { uint_fast64_t modelStateCount = model.getNumberOfStates(); - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); std::vector result(modelStateCount * memoryStateCount, std::numeric_limits::max()); storm::modelchecker::SparsePropositionalModelChecker> mc(model); @@ -63,8 +74,8 @@ namespace storm { for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { auto const& transition = memory.getTransitionMatrix()[memoryState][transitionGoal]; if (transition) { - storm::storage::BitVector const& modelStates = mc.check(*transition)->asExplicitQualitativeCheckResult().getTruthValuesVector(); - for (auto const& modelState : modelStates) { + auto mcResult = mc.check(*transition); + for (auto const& modelState : mcResult->asExplicitQualitativeCheckResult().getTruthValuesVector()) { result[modelState * memoryStateCount + memoryState] = transitionGoal; } } @@ -74,19 +85,12 @@ namespace storm { } template - storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors) const { - uint_fast64_t modelStateCount = model.getNumberOfStates(); - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); - // Explore the reachable states via with DFS. + storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + // Explore the reachable states via DFS. // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) - storm::storage::BitVector reachableStates(modelStateCount * memoryStateCount, false); - std::vector stack; - for (auto const& modelInit : model.getInitialStates()) { - // Note: 0 is always the initial state of a memory structure. - uint_fast64_t stateIndex = modelInit * memoryStateCount + memorySuccessors[modelInit * memoryStateCount]; - reachableStates.set(stateIndex, true); - stack.push_back(stateIndex); - } + storm::storage::BitVector reachableStates = initialStates; + std::vector stack(reachableStates.begin(), reachableStates.end()); while (!stack.empty()) { uint_fast64_t stateIndex = stack.back(); stack.pop_back(); @@ -110,7 +114,7 @@ namespace storm { template storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); uint_fast64_t numResTransitions = 0; for (auto const& stateIndex : reachableStates) { @@ -124,8 +128,7 @@ namespace storm { uint_fast64_t memoryState = stateIndex % memoryStateCount; for (auto const& entry : model.getTransitionMatrix().getRow(modelState)) { uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; - uint_fast64_t transitionTargetStateIndex = entry.getColumn() * memoryStateCount + successorMemoryState; - builder.addNextValue(currentRow, toResultStateMapping[transitionTargetStateIndex], entry.getValue()); + builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); } ++currentRow; } @@ -135,7 +138,7 @@ namespace storm { template storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); uint_fast64_t numResChoices = 0; uint_fast64_t numResTransitions = 0; @@ -156,8 +159,7 @@ namespace storm { for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { for (auto const& entry : model.getTransitionMatrix().getRow(modelRow)) { uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; - uint_fast64_t transitionTargetStateIndex = entry.getColumn() * memoryStateCount + successorMemoryState; - builder.addNextValue(currentRow, toResultStateMapping[transitionTargetStateIndex], entry.getValue()); + builder.addNextValue(currentRow, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); } ++currentRow; } @@ -169,32 +171,32 @@ namespace storm { template storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { uint_fast64_t modelStateCount = model.getNumberOfStates(); - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); storm::models::sparse::StateLabeling resultLabeling(numResStates); for (std::string modelLabel : model.getStateLabeling().getLabels()) { - storm::storage::BitVector const& modelLabeledStates = model.getStateLabeling().getStates(modelLabel); - storm::storage::BitVector resLabeledStates(numResStates, false); - for (auto const& modelState : modelLabeledStates) { - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = toResultStateMapping[modelState * memoryStateCount + memoryState]; - // Check if the state exists in the result (i.e. if it is reachable) - if (resState < numResStates) { - resLabeledStates.set(resState, true); + if (modelLabel != "init") { + storm::storage::BitVector resLabeledStates(numResStates, false); + for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) { + for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { + uint_fast64_t const& resState = getResultState(modelState, memoryState); + // Check if the state exists in the result (i.e. if it is reachable) + if (resState < numResStates) { + resLabeledStates.set(resState, true); + } } } + resultLabeling.addLabel(modelLabel, std::move(resLabeledStates)); } - resultLabeling.addLabel(modelLabel, std::move(resLabeledStates)); } for (std::string memoryLabel : memory.getStateLabeling().getLabels()) { STORM_LOG_THROW(!resultLabeling.containsLabel(memoryLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " << memoryLabel << "."); - storm::storage::BitVector const& memoryLabeledStates = memory.getStateLabeling().getStates(memoryLabel); storm::storage::BitVector resLabeledStates(numResStates, false); - for (auto const& memoryState : memoryLabeledStates) { + for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { for (uint_fast64_t modelState = 0; modelState < modelStateCount; ++modelState) { - uint_fast64_t const& resState = toResultStateMapping[modelState * memoryStateCount + memoryState]; + uint_fast64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { resLabeledStates.set(resState, true); @@ -209,7 +211,7 @@ namespace storm { template std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { std::unordered_map> result; - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); for (auto const& rewardModel : model.getRewardModels()) { @@ -220,7 +222,7 @@ namespace storm { for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { if (!storm::utility::isZero(modelStateReward)) { for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = toResultStateMapping[modelState * memoryStateCount + memoryState]; + uint_fast64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { stateRewards.get()[resState] = modelStateReward; @@ -242,7 +244,7 @@ namespace storm { } uint_fast64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = toResultStateMapping[modelState * memoryStateCount + memoryState]; + uint_fast64_t const& resState = getResultState(modelState, memoryState); // Check if the state exists in the result (i.e. if it is reachable) if (resState < numResStates) { stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; @@ -266,8 +268,7 @@ namespace storm { uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; for (auto const& entry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { uint_fast64_t const& successorMemoryState = memorySuccessors[entry.getColumn() * memoryStateCount + memoryState]; - uint_fast64_t transitionTargetStateIndex = entry.getColumn() * memoryStateCount + successorMemoryState; - builder.addNextValue(resRowIndex, toResultStateMapping[transitionTargetStateIndex], entry.getValue()); + builder.addNextValue(resRowIndex, getResultState(entry.getColumn(), successorMemoryState), entry.getValue()); } } } @@ -293,7 +294,7 @@ namespace storm { { // We also need to translate the exit rates and the Markovian states uint_fast64_t numResStates = matrix.getRowGroupCount(); - uint_fast64_t memoryStateCount = memory.getTransitionMatrix().size(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); std::vector resultExitRates; resultExitRates.reserve(matrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); @@ -310,10 +311,12 @@ namespace storm { resultMarkovianStates.set(resState, true); } } + ++stateIndex; } - ++stateIndex; return std::make_shared> (std::move(matrix), std::move(labeling), std::move(resultMarkovianStates), std::move(resultExitRates), true, std::move(rewardModels)); } + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Memory Structure Product for Model Type " << model.getType() << " is not supported"); } } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 92baea200..170efba3f 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -31,8 +31,9 @@ namespace storm { // Invokes the building of the product std::shared_ptr> build(); - // Retrieves the state of the resulting model that represents the given memory and model state - uint_fast64_t const& getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState); + // Retrieves the state of the resulting model that represents the given memory and model state. + // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable). + uint_fast64_t const& getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const; private: @@ -41,12 +42,16 @@ namespace storm { std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model - storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors) const; + storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const; // Methods that build the model components + // Matrix for deterministic models storm::storage::SparseMatrix buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + // Matrix for nondeterministic models storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; + // Reward models std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; // Builds the resulting model