diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 479286ad2..04c099e6e 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -484,8 +484,8 @@ namespace storm { productToMemoryStateMap.resize(numProductStates, std::numeric_limits::max()); for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) { for (uint64_t memoryState = 0; memoryState < numMemoryStates; ++memoryState) { - uint64_t productState = productBuilder.getResultState(modelState, memoryState); - if (productState < numProductStates) { + if (productBuilder.isStateReachable(modelState, memoryState)) { + uint64_t productState = productBuilder.getResultState(modelState, memoryState); modelMemoryToProductStateMap[modelState * numMemoryStates + memoryState] = productState; productToModelStateMap[productState] = modelState; productToMemoryStateMap[productState] = memoryState; diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index acdbd3885..cd67e384f 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -51,22 +51,11 @@ namespace storm { template std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { - if (scheduler.isMemorylessScheduler()) { - auto memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); - auto memoryProduct = memStruct.product(*this); - if (!dropUnreachableStates) { - memoryProduct.setBuildFullProduct(); - } - return memoryProduct.build(scheduler); - } else { - boost::optional const& memStruct = scheduler.getMemoryStructure(); - STORM_LOG_ASSERT(memStruct, "Memoryless scheduler without memory structure."); - auto memoryProduct = memStruct->product(*this); - if (!dropUnreachableStates) { - memoryProduct.setBuildFullProduct(); - } - return memoryProduct.build(scheduler); + storm::storage::SparseModelMemoryProduct memoryProduct(*this, scheduler); + if (!dropUnreachableStates) { + memoryProduct.setBuildFullProduct(); } + return memoryProduct.build(); } template diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 49d69e240..3907f0625 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -9,6 +9,7 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" #include "storm/utility/macros.h" #include "storm/utility/builder.h" @@ -18,91 +19,113 @@ namespace storm { namespace storage { template - SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : memoryStateCount(memoryStructure.getNumberOfStates()), model(sparseModel), memory(memoryStructure) { + SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : isInitialized(false), memoryStateCount(memoryStructure.getNumberOfStates()), model(sparseModel), memory(memoryStructure), scheduler(boost::none) { reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memoryStateCount, false); } + template + SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::Scheduler const& scheduler) : isInitialized(false), memoryStateCount(scheduler.getNumberOfMemoryStates()), model(sparseModel), localMemory(scheduler.getMemoryStructure() ? boost::optional() : boost::optional(storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model))), memory(scheduler.getMemoryStructure() ? scheduler.getMemoryStructure().get() : localMemory.get()), scheduler(scheduler) { + reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memoryStateCount, false); + } + + template + void SparseModelMemoryProduct::initialize() { + if (!isInitialized) { + uint64_t modelStateCount = model.getNumberOfStates(); + + computeMemorySuccessors(); + + // 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); + auto memoryInitIt = memory.getInitialMemoryStates().begin(); + for (auto const& modelInit : model.getInitialStates()) { + initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); + ++memoryInitIt; + } + STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); + + computeReachableStates(initialStates); + + // Compute the mapping to the states of the result + uint64_t reachableStateCount = 0; + toResultStateMapping = std::vector (model.getNumberOfStates() * memoryStateCount, std::numeric_limits::max()); + for (auto const& reachableState : reachableStates) { + toResultStateMapping[reachableState] = reachableStateCount; + ++reachableStateCount; + } + + isInitialized = true; + } + } + template void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { + isInitialized = false; reachableStates.set(modelState * memoryStateCount + memoryState, true); } template void SparseModelMemoryProduct::setBuildFullProduct() { + isInitialized = false; reachableStates.fill(); } template - std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { - - uint64_t modelStateCount = model.getNumberOfStates(); + std::shared_ptr> SparseModelMemoryProduct::build() { - std::vector memorySuccessors = computeMemorySuccessors(); + initialize(); - // 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); - auto memoryInitIt = memory.getInitialMemoryStates().begin(); - for (auto const& modelInit : model.getInitialStates()) { - initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); - ++memoryInitIt; - } - STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); - - computeReachableStates(memorySuccessors, initialStates, scheduler); - - // Compute the mapping to the states of the result - uint64_t reachableStateCount = 0; - toResultStateMapping = std::vector (model.getNumberOfStates() * memoryStateCount, std::numeric_limits::max()); - for (auto const& reachableState : reachableStates) { - toResultStateMapping[reachableState] = reachableStateCount; - ++reachableStateCount; - } - // Build the model components storm::storage::SparseMatrix transitionMatrix; if (scheduler) { - transitionMatrix = buildTransitionMatrixForScheduler(memorySuccessors, scheduler.get()); + transitionMatrix = buildTransitionMatrixForScheduler(); } else if (model.getTransitionMatrix().hasTrivialRowGrouping()) { - transitionMatrix = buildDeterministicTransitionMatrix(memorySuccessors); + transitionMatrix = buildDeterministicTransitionMatrix(); } else { - transitionMatrix = buildNondeterministicTransitionMatrix(memorySuccessors); + transitionMatrix = buildNondeterministicTransitionMatrix(); } storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); - std::unordered_map rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); + std::unordered_map rewardModels = buildRewardModels(transitionMatrix); - // 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), scheduler); + return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); } template - uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { - return toResultStateMapping[modelState * memoryStateCount + memoryState]; + bool SparseModelMemoryProduct::isStateReachable(uint64_t const& modelState, uint64_t const& memoryState) { + STORM_LOG_ASSERT(modelState < getOriginalModel().getNumberOfStates(), "Invalid model state: " << modelState << "."); + STORM_LOG_ASSERT(memoryState < memoryStateCount, "Invalid memory state: " << memoryState << "."); + initialize(); + return reachableStates.get(modelState * memoryStateCount + memoryState); + } + + template + uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) { + initialize(); + STORM_LOG_ASSERT(isStateReachable(modelState, memoryState), "Tried to get unreachable product state (" << modelState << "," << memoryState << ")"); + return toResultStateMapping[modelState * memoryStateCount + memoryState]; } template - std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { + void SparseModelMemoryProduct::computeMemorySuccessors() { uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); - std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); + memorySuccessors = std::vector(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { for (uint64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal]; if (memoryTransition) { for (auto const& modelTransitionIndex : memoryTransition.get()) { - result[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal; + memorySuccessors[modelTransitionIndex * memoryStateCount + memoryState] = transitionGoal; } } } } - return result; } template - void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { + void SparseModelMemoryProduct::computeReachableStates(storm::storage::BitVector const& initialStates) { // Explore the reachable states via DFS. // A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) reachableStates |= initialStates; @@ -153,7 +176,7 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix() { uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResTransitions = 0; for (auto const& stateIndex : reachableStates) { @@ -168,7 +191,7 @@ namespace storm { auto const& modelRow = model.getTransitionMatrix().getRow(modelState); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -178,7 +201,7 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix() { uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; uint64_t numResTransitions = 0; @@ -200,7 +223,7 @@ namespace storm { auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -211,7 +234,7 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { + storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler() { uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; uint64_t numResTransitions = 0; @@ -219,7 +242,7 @@ namespace storm { for (auto const& stateIndex : reachableStates) { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; - storm::storage::SchedulerChoice choice = scheduler.getChoice(modelState, memoryState); + storm::storage::SchedulerChoice choice = scheduler->getChoice(modelState, memoryState); if (choice.isDefined()) { ++numResChoices; if (choice.isDeterministic()) { @@ -256,14 +279,14 @@ namespace storm { if (!hasTrivialNondeterminism) { builder.newRowGroup(currentRow); } - storm::storage::SchedulerChoice choice = scheduler.getChoice(modelState, memoryState); + storm::storage::SchedulerChoice choice = scheduler->getChoice(modelState, memoryState); if (choice.isDefined()) { if (choice.isDeterministic()) { uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choice.getDeterministicChoice(); auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } } else { @@ -274,7 +297,7 @@ namespace storm { auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; ValueType transitionValue = choiceIndex.second * entryIt->getValue(); auto insertionRes = transitions.insert(std::make_pair(getResultState(entryIt->getColumn(), successorMemoryState), transitionValue)); if (!insertionRes.second) { @@ -293,7 +316,7 @@ namespace storm { auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -305,7 +328,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { + storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) { uint64_t modelStateCount = model.getNumberOfStates(); uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); @@ -316,10 +339,8 @@ namespace storm { storm::storage::BitVector resLabeledStates(numResStates, false); for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) { for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint64_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); + if (isStateReachable(modelState, memoryState)) { + resLabeledStates.set(getResultState(modelState, memoryState), true); } } } @@ -331,20 +352,27 @@ namespace storm { storm::storage::BitVector resLabeledStates(numResStates, false); for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { for (uint64_t modelState = 0; modelState < modelStateCount; ++modelState) { - uint64_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); + if (isStateReachable(modelState, memoryState)) { + resLabeledStates.set(getResultState(modelState, memoryState), true); } } } resultLabeling.addLabel(memoryLabel, std::move(resLabeledStates)); } + + storm::storage::BitVector initialStates(numResStates, false); + auto memoryInitIt = memory.getInitialMemoryStates().begin(); + for (auto const& modelInit : model.getInitialStates()) { + initialStates.set(getResultState(modelInit, *memoryInitIt), true); + ++memoryInitIt; + } + resultLabeling.addLabel("init", std::move(initialStates)); + return resultLabeling; } template - std::unordered_map SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const { + std::unordered_map SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix) { typedef typename RewardModelType::ValueType RewardValueType; @@ -359,10 +387,8 @@ namespace storm { for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { if (!storm::utility::isZero(modelStateReward)) { for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint64_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; + if (isStateReachable(modelState, memoryState)) { + stateRewards.get()[getResultState(modelState, memoryState)] = modelStateReward; } } } @@ -381,14 +407,12 @@ namespace storm { } uint64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint64_t const& resState = getResultState(modelState, memoryState); - // Check if the state exists in the result (i.e. if it is reachable) - if (resState < numResStates) { + if (isStateReachable(modelState, memoryState)) { if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { ValueType factor = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution().getProbability(rowOffset); - stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState]] = factor * modelStateActionReward; + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)]] = factor * modelStateActionReward; } else { - stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[getResultState(modelState, memoryState)] + rowOffset] = modelStateActionReward; } } } @@ -416,7 +440,7 @@ namespace storm { ++transitionEntryIt; } uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; auto insertionRes = rewards.insert(std::make_pair(getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue())); if (!insertionRes.second) { insertionRes.first->second += rewardEntry.getValue(); @@ -438,7 +462,7 @@ namespace storm { ++transitionEntryIt; } uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(resRowIndex, getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue()); } } @@ -454,7 +478,7 @@ namespace storm { } template - std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels, boost::optional> const& scheduler) const { + std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels) { storm::storage::sparse::ModelComponents components (std::move(matrix), std::move(labeling), std::move(rewardModels)); if (model.isOfType(storm::models::ModelType::Ctmc)) { diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index f32f092d1..45f4d2525 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -25,48 +25,63 @@ namespace storm { class SparseModelMemoryProduct { public: + // Constructs the product w.r.t. the given model and the given memory structure SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + // Constructs the product w.r.t. the given model and the given (finite memory) scheduler. + SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::Scheduler const& scheduler); + // 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 under the specified scheduler (if given). - std::shared_ptr> build(boost::optional> const& scheduler = boost::none); + // Returns true iff the given model and memory state is reachable in the product + bool isStateReachable(uint64_t const& modelState, uint64_t const& memoryState); // Retrieves the state of the resulting model that represents the given memory and model state. - // 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; + // This method should only be called if the given state is reachable. + uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState); + + // Invokes the building of the product under the specified scheduler (if given). + std::shared_ptr> build(); storm::models::sparse::Model const& getOriginalModel() const; storm::storage::MemoryStructure const& getMemory() const; + private: + // Initializes auxiliary data for building the product + void initialize(); + // Computes for each pair of memory state and model transition index the successor memory state // The resulting vector maps (modelTransition * memoryStateCount) + memoryState to the corresponding successor state of the memory structure - std::vector computeMemorySuccessors() const; + void computeMemorySuccessors(); // Computes the reachable states of the resulting model - void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler); + void computeReachableStates(storm::storage::BitVector const& initialStates); // Methods that build the model components // Matrix for deterministic models - storm::storage::SparseMatrix buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildDeterministicTransitionMatrix(); // Matrix for nondeterministic models - storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const; + storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(); // Matrix for models that consider a scheduler - storm::storage::SparseMatrix buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const; - // State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES - storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const; + storm::storage::SparseMatrix buildTransitionMatrixForScheduler(); + // State labeling. + storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix); // Reward models - std::unordered_map buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const; + std::unordered_map buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix); // Builds the resulting model - std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels, boost::optional> const& scheduler) const; + std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels); + + // Stores whether this builder has already been initialized. + bool isInitialized; + // stores the successor memory states for each transition in the product + std::vector memorySuccessors; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) std::vector toResultStateMapping; @@ -77,7 +92,9 @@ namespace storm { uint64_t const memoryStateCount; storm::models::sparse::Model const& model; + boost::optional localMemory; storm::storage::MemoryStructure const& memory; + boost::optional const&> scheduler; }; }