diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 2ad64c746..7e7c4af5b 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -19,9 +19,21 @@ namespace storm { template SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { - // intentionally left empty + reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memory.getNumberOfStates(), false); } - + + template + void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { + reachableStates.set(modelState * memory.getNumberOfStates() + memoryState, true); + } + + template + void SparseModelMemoryProduct::setBuildFullProduct() { + reachableStates.clear(); + reachableStates.complement(); + } + + template std::shared_ptr> SparseModelMemoryProduct::build() { uint64_t modelStateCount = model.getNumberOfStates(); @@ -38,7 +50,7 @@ namespace storm { } STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); - storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates); + computeReachableStates(memorySuccessors, initialStates); // Compute the mapping to the states of the result uint64_t reachableStateCount = 0; @@ -50,8 +62,8 @@ namespace storm { // Build the model components storm::storage::SparseMatrix transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ? - buildDeterministicTransitionMatrix(reachableStates, memorySuccessors) : - buildNondeterministicTransitionMatrix(reachableStates, memorySuccessors); + buildDeterministicTransitionMatrix(memorySuccessors) : + buildNondeterministicTransitionMatrix(memorySuccessors); storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); @@ -88,37 +100,38 @@ namespace storm { } template - storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { + void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) { uint64_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 = initialStates; - std::vector stack(reachableStates.begin(), reachableStates.end()); - while (!stack.empty()) { - uint64_t stateIndex = stack.back(); - stack.pop_back(); - uint64_t modelState = stateIndex / memoryStateCount; - uint64_t memoryState = stateIndex % memoryStateCount; - - auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); - for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { - if (!storm::utility::isZero(modelTransitionIt->getValue())) { - uint64_t successorModelState = modelTransitionIt->getColumn(); - uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); - uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; - uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; - if (!reachableStates.get(successorStateIndex)) { - reachableStates.set(successorStateIndex, true); - stack.push_back(successorStateIndex); + reachableStates |= initialStates; + if (!reachableStates.full()) { + std::vector stack(reachableStates.begin(), reachableStates.end()); + while (!stack.empty()) { + uint64_t stateIndex = stack.back(); + stack.pop_back(); + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + + auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState); + for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) { + if (!storm::utility::isZero(modelTransitionIt->getValue())) { + uint64_t successorModelState = modelTransitionIt->getColumn(); + uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); + uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; + uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + if (!reachableStates.get(successorStateIndex)) { + reachableStates.set(successorStateIndex, true); + stack.push_back(successorStateIndex); + } } } } } - return reachableStates; } - + template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResTransitions = 0; @@ -144,7 +157,7 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index b5faf2ab4..55a72172d 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -14,9 +14,7 @@ namespace storm { /*! * This class builds the product of the given sparse model and the given memory structure. * This is similar to the well-known product of a model with a deterministic rabin automaton. - * Note: we already do one memory-structure-step for the initial state, i.e., if s is an initial state of - * the given model and s satisfies memoryStructure.getTransitionMatrix[0][n], then (s,n) will be the corresponding - * initial state of the resulting model. + * The product contains only the reachable states of the product * * The states of the resulting sparse model will have the original state labels plus the labels of this * memory structure. @@ -28,11 +26,18 @@ namespace storm { SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + // Enforces that the given model and memory state as well as the successor(s) are considered reachable -- even if they are not reachable from an initial state. + void addReachableState(uint64_t const& modelState, uint64_t const& memoryState); + + // Enforces that every state is considered reachable. If this is set, the result has size #modelStates * #memoryStates + void setBuildFullProduct(); + // 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. - // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable). + // Should only be called AFTER calling build(); + // An invalid index is returned, if the specifyied state does not exist (i.e., if it is not part of product). uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const; private: @@ -42,13 +47,13 @@ namespace storm { std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model - storm::storage::BitVector computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const; + void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates); // Methods that build the model components // Matrix for deterministic models - storm::storage::SparseMatrix buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const; // Matrix for nondeterministic models - storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(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 @@ -61,7 +66,9 @@ namespace storm { // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) std::vector toResultStateMapping; - + // Indicates which states are considered reachable. (s, m) is reachable if this BitVector is true at (s * memoryStateCount) + m + storm::storage::BitVector reachableStates; + storm::models::sparse::Model const& model; storm::storage::MemoryStructure const& memory;