From 9bccae9c5c6e8e548903997d167fa6346e51d6d5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 15:59:31 +0200 Subject: [PATCH 1/9] uint_fast64_t -> uint64_t --- .../SparseModelMemoryProduct.cpp | 150 +++++++++--------- .../SparseModelMemoryProduct.h | 14 +- 2 files changed, 82 insertions(+), 82 deletions(-) diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 56b3a6aa0..2ad64c746 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -24,10 +24,10 @@ namespace storm { template std::shared_ptr> SparseModelMemoryProduct::build() { - uint_fast64_t modelStateCount = model.getNumberOfStates(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t modelStateCount = model.getNumberOfStates(); + uint64_t memoryStateCount = memory.getNumberOfStates(); - std::vector memorySuccessors = computeMemorySuccessors(); + std::vector memorySuccessors = 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); @@ -41,8 +41,8 @@ namespace storm { 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.getNumberOfStates(), std::numeric_limits::max()); + uint64_t reachableStateCount = 0; + toResultStateMapping = std::vector (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits::max()); for (auto const& reachableState : reachableStates) { toResultStateMapping[reachableState] = reachableStateCount; ++reachableStateCount; @@ -64,18 +64,18 @@ namespace storm { } template - uint_fast64_t const& SparseModelMemoryProduct::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const { + uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } template - std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { - uint_fast64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); + std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { + uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); + uint64_t memoryStateCount = memory.getNumberOfStates(); + std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) { + 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()) { @@ -88,25 +88,25 @@ namespace storm { } template - storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + storm::storage::BitVector SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) const { + 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()); + std::vector stack(reachableStates.begin(), reachableStates.end()); while (!stack.empty()) { - uint_fast64_t stateIndex = stack.back(); + uint64_t stateIndex = stack.back(); stack.pop_back(); - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; + 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())) { - uint_fast64_t successorModelState = modelTransitionIt->getColumn(); - uint_fast64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin(); - uint_fast64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState]; - uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState; + 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); @@ -118,23 +118,23 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); - uint_fast64_t numResTransitions = 0; + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = reachableStates.getNumberOfSetBits(); + uint64_t numResTransitions = 0; for (auto const& stateIndex : reachableStates) { numResTransitions += model.getTransitionMatrix().getRow(stateIndex / memoryStateCount).getNumberOfEntries(); } storm::storage::SparseMatrixBuilder builder(numResStates, numResStates, numResTransitions, true); - uint_fast64_t currentRow = 0; + uint64_t currentRow = 0; for (auto const& stateIndex : reachableStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; auto const& modelRow = model.getTransitionMatrix().getRow(modelState); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { - uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -144,30 +144,30 @@ namespace storm { } template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = reachableStates.getNumberOfSetBits(); - uint_fast64_t numResChoices = 0; - uint_fast64_t numResTransitions = 0; + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector const& memorySuccessors) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = reachableStates.getNumberOfSetBits(); + uint64_t numResChoices = 0; + uint64_t numResTransitions = 0; for (auto const& stateIndex : reachableStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { + uint64_t modelState = stateIndex / memoryStateCount; + for (uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) { ++numResChoices; numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); } } storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, true, numResStates); - uint_fast64_t currentRow = 0; + uint64_t currentRow = 0; for (auto const& stateIndex : reachableStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; builder.newRowGroup(currentRow); - for (uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { + for (uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex); for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) { - uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin(); - uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t transitionId = entryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } ++currentRow; @@ -179,18 +179,18 @@ 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.getNumberOfStates(); + uint64_t modelStateCount = model.getNumberOfStates(); + uint64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); + uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); storm::models::sparse::StateLabeling resultLabeling(numResStates); for (std::string modelLabel : model.getStateLabeling().getLabels()) { 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); + 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); @@ -204,8 +204,8 @@ namespace storm { 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 resLabeledStates(numResStates, false); for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) { - for (uint_fast64_t modelState = 0; modelState < modelStateCount; ++modelState) { - uint_fast64_t const& resState = getResultState(modelState, memoryState); + 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); @@ -218,20 +218,20 @@ namespace storm { } template - std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { + std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { std::unordered_map> result; - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount(); + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); for (auto const& rewardModel : model.getRewardModels()) { boost::optional> stateRewards; if (rewardModel.second.hasStateRewards()) { stateRewards = std::vector(numResStates, storm::utility::zero()); - uint_fast64_t modelState = 0; + uint64_t modelState = 0; 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 = getResultState(modelState, memoryState); + 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; @@ -244,16 +244,16 @@ namespace storm { boost::optional> stateActionRewards; if (rewardModel.second.hasStateActionRewards()) { stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); - uint_fast64_t modelState = 0; - uint_fast64_t modelRow = 0; + uint64_t modelState = 0; + uint64_t modelRow = 0; for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { if (!storm::utility::isZero(modelStateActionReward)) { while (modelRow >= model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]) { ++modelState; } - uint_fast64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState]; - for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) { - uint_fast64_t const& resState = getResultState(modelState, memoryState); + 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) { stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; @@ -266,19 +266,19 @@ namespace storm { boost::optional> transitionRewards; if (rewardModel.second.hasTransitionRewards()) { storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); - uint_fast64_t stateIndex = 0; + uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { if (resState < numResStates) { - uint_fast64_t modelState = stateIndex / memoryStateCount; - uint_fast64_t memoryState = stateIndex % memoryStateCount; - uint_fast64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); - for (uint_fast64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { - uint_fast64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; - uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); + for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex); for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) { - uint_fast64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); - uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + uint64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); } } @@ -300,19 +300,19 @@ namespace storm { components.rateTransitions = true; } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { // We also need to translate the exit rates and the Markovian states - uint_fast64_t numResStates = components.transitionMatrix.getRowGroupCount(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = components.transitionMatrix.getRowGroupCount(); + uint64_t memoryStateCount = memory.getNumberOfStates(); std::vector resultExitRates; resultExitRates.reserve(components.transitionMatrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); - uint_fast64_t stateIndex = 0; + uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { if (resState < numResStates) { assert(resState == resultExitRates.size()); - uint_fast64_t modelState = stateIndex / memoryStateCount; + uint64_t modelState = stateIndex / memoryStateCount; resultExitRates.push_back(modelExitRates[modelState]); if (modelMarkovianStates.get(modelState)) { resultMarkovianStates.set(resState, true); diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 0c60923e7..b5faf2ab4 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -33,33 +33,33 @@ namespace storm { // 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; + uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const; private: // 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; + 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; + 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; + 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; + 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; + std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; // Builds the resulting model std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) - std::vector toResultStateMapping; + std::vector toResultStateMapping; storm::models::sparse::Model const& model; From 43642fef847959dbdb7cb293aa5f468508be4116 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 16:41:28 +0200 Subject: [PATCH 2/9] Improved product of model and memory structure: We can now enforce that certain states are considered reachable. --- .../SparseModelMemoryProduct.cpp | 69 +++++++++++-------- .../SparseModelMemoryProduct.h | 23 ++++--- 2 files changed, 56 insertions(+), 36 deletions(-) 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; From 4351be551210a03147e4f60fd511a2b50d79b23e Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 10:43:34 +0200 Subject: [PATCH 3/9] Allowed building memory product with respect to a scheduler --- src/storm/storage/Distribution.cpp | 12 + src/storm/storage/Distribution.h | 10 +- .../SparseModelMemoryProduct.cpp | 224 +++++++++++++++--- .../SparseModelMemoryProduct.h | 13 +- 4 files changed, 222 insertions(+), 37 deletions(-) diff --git a/src/storm/storage/Distribution.cpp b/src/storm/storage/Distribution.cpp index 0c2ac73db..9d0d89d19 100644 --- a/src/storm/storage/Distribution.cpp +++ b/src/storm/storage/Distribution.cpp @@ -156,6 +156,18 @@ namespace storm { return false; } + template + ValueType Distribution::getProbability(StateType const& state) const { + auto it = this->distribution.find(state); + if (it == this->distribution.end()) { + return storm::utility::zero(); + } else { + return it->second; + } + } + + + template class Distribution; template std::ostream& operator<<(std::ostream& out, Distribution const& distribution); template class Distribution; diff --git a/src/storm/storage/Distribution.h b/src/storm/storage/Distribution.h index ff4b0689b..328e87f98 100644 --- a/src/storm/storage/Distribution.h +++ b/src/storm/storage/Distribution.h @@ -73,7 +73,7 @@ namespace storm { * entry is removed. */ void shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); - + /*! * Retrieves an iterator to the elements in this distribution. * @@ -132,6 +132,14 @@ namespace storm { bool less(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const; + + /*! + * Returns the probability of the given state + * @param state The state for which the probability is returned. + * @return The probability of the given state. + */ + ValueType getProbability(StateType const& state) const; + private: // A list of states and the probabilities that are assigned to them. container_type distribution; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 7e7c4af5b..97e601f52 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -32,10 +32,10 @@ namespace storm { reachableStates.clear(); reachableStates.complement(); } - template - std::shared_ptr> SparseModelMemoryProduct::build() { + std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { + uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -50,7 +50,7 @@ namespace storm { } STORM_LOG_ASSERT(memoryInitIt == memory.getInitialMemoryStates().end(), "Unexpected number of initial states."); - computeReachableStates(memorySuccessors, initialStates); + computeReachableStates(memorySuccessors, initialStates, scheduler); // Compute the mapping to the states of the result uint64_t reachableStateCount = 0; @@ -61,17 +61,22 @@ namespace storm { } // Build the model components - storm::storage::SparseMatrix transitionMatrix = model.getTransitionMatrix().hasTrivialRowGrouping() ? - buildDeterministicTransitionMatrix(memorySuccessors) : - buildNondeterministicTransitionMatrix(memorySuccessors); + storm::storage::SparseMatrix transitionMatrix; + if (scheduler) { + transitionMatrix = buildTransitionMatrixForScheduler(memorySuccessors, scheduler.get()); + } else if (model.getTransitionMatrix().hasTrivialRowGrouping()) { + transitionMatrix = buildDeterministicTransitionMatrix(memorySuccessors); + } else { + transitionMatrix = buildNondeterministicTransitionMatrix(memorySuccessors); + } storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); - std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors); + std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); // 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)); + return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels), scheduler); } @@ -100,7 +105,7 @@ namespace storm { } template - void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates) { + void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { 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) @@ -113,16 +118,37 @@ namespace storm { 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); + if (scheduler) { + auto choices = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution(); + uint64_t groupStart = model.getTransitionMatrix().getRowGroupIndices()[modelState]; + for (auto const& choice : choices) { + STORM_LOG_ASSERT(groupStart + choice.first < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1], "Invalid choice " << choice.first << " at model state " << modelState << "."); + auto const& row = model.getTransitionMatrix().getRow(groupStart + choice.first); + for (auto modelTransitionIt = row.begin(); modelTransitionIt != row.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); + } + } + } + } + } else { + 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); + } } } } @@ -190,6 +216,101 @@ namespace storm { return builder.build(); } + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { + uint64_t memoryStateCount = memory.getNumberOfStates(); + uint64_t numResStates = reachableStates.getNumberOfSetBits(); + uint64_t numResChoices = 0; + uint64_t numResTransitions = 0; + bool hasTrivialNondeterminism = true; + for (auto const& stateIndex : reachableStates) { + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + storm::storage::SchedulerChoice choice = scheduler.getChoice(modelState, memoryState); + if (choice.isDefined()) { + ++numResChoices; + if (choice.isDeterministic()) { + uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choice.getDeterministicChoice(); + numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); + } else { + std::set successors; + for (auto const& choiceIndex : choice.getChoiceAsDistribution()) { + if (!storm::utility::isZero(choiceIndex.second)) { + uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choiceIndex.first; + for (auto const& entry : model.getTransitionMatrix().getRow(modelRow)) { + successors.insert(entry.getColumn()); + } + } + } + numResTransitions += successors.size(); + } + } else { + uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; + uint64_t groupEnd = model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; + hasTrivialNondeterminism = hasTrivialNondeterminism && (groupEnd == modelRow + 1); + for (; groupEnd; ++modelRow) { + ++numResChoices; + numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries(); + } + } + } + + storm::storage::SparseMatrixBuilder builder(numResChoices, numResStates, numResTransitions, true, !hasTrivialNondeterminism, hasTrivialNondeterminism ? 0 : numResStates); + uint64_t currentRow = 0; + for (auto const& stateIndex : reachableStates) { + uint64_t modelState = stateIndex / memoryStateCount; + uint64_t memoryState = stateIndex % memoryStateCount; + if (!hasTrivialNondeterminism) { + builder.newRowGroup(currentRow); + } + 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]; + builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); + } + } else { + std::map transitions; + for (auto const& choiceIndex : choice.getChoiceAsDistribution()) { + if (!storm::utility::isZero(choiceIndex.second)) { + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + choiceIndex.first; + 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]; + ValueType transitionValue = choiceIndex.second * entryIt->getValue(); + auto insertionRes = transitions.insert(std::make_pair(getResultState(entryIt->getColumn(), successorMemoryState), transitionValue)); + if (!insertionRes.second) { + insertionRes.first->second += transitionValue; + } + } + } + } + for (auto const& transition : transitions) { + builder.addNextValue(currentRow, transition.first, transition.second); + } + } + ++currentRow; + } else { + for (uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) { + 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]; + builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); + } + ++currentRow; + } + } + } + + return builder.build(); + } + template storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { uint64_t modelStateCount = model.getNumberOfStates(); @@ -231,7 +352,7 @@ namespace storm { } template - std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const { + std::unordered_map> SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const { std::unordered_map> result; uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); @@ -269,7 +390,12 @@ namespace storm { uint64_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; + if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { + ValueType factor = scheduler->getChoice(modelState, memoryState).getChoiceAsDistribution().getProbability(rowOffset); + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState]] = factor * modelStateActionReward; + } else { + stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward; + } } } } @@ -285,14 +411,42 @@ namespace storm { uint64_t modelState = stateIndex / memoryStateCount; uint64_t memoryState = stateIndex % memoryStateCount; uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); - for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { - uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; - uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; - auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex); - for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) { - uint64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin(); - uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; - builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue()); + if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { + std::map rewards; + for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + auto transitionEntryIt = model.getTransitionMatrix().getRow(modelRowIndex).begin(); + for (auto const& rewardEntry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { + while (transitionEntryIt->getColumn() != rewardEntry.getColumn()) { + STORM_LOG_ASSERT(transitionEntryIt != model.getTransitionMatrix().getRow(modelRowIndex).end(), "The reward transition matrix is not a submatrix of the model transition matrix."); + ++transitionEntryIt; + } + uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin(); + uint64_t const& 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(); + } + } + } + uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState]; + for (auto& reward : rewards) { + builder.addNextValue(resRowIndex, reward.first, reward.second); + } + } else { + for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { + uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset; + uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; + auto transitionEntryIt = model.getTransitionMatrix().getRow(modelRowIndex).begin(); + for (auto const& rewardEntry : rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex)) { + while (transitionEntryIt->getColumn() != rewardEntry.getColumn()) { + STORM_LOG_ASSERT(transitionEntryIt != model.getTransitionMatrix().getRow(modelRowIndex).end(), "The reward transition matrix is not a submatrix of the model transition matrix."); + ++transitionEntryIt; + } + uint64_t transitionId = transitionEntryIt - model.getTransitionMatrix().begin(); + uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState]; + builder.addNextValue(resRowIndex, getResultState(rewardEntry.getColumn(), successorMemoryState), rewardEntry.getValue()); + } } } } @@ -306,7 +460,7 @@ namespace storm { } template - std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const { + std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const { storm::storage::sparse::ModelComponents> components (std::move(matrix), std::move(labeling), std::move(rewardModels)); if (model.isOfType(storm::models::ModelType::Ctmc)) { @@ -337,7 +491,15 @@ namespace storm { components.exitRates = std::move(resultExitRates); } - return storm::utility::builder::buildModelFromComponents(model.getType(), std::move(components)); + storm::models::ModelType resultType = model.getType(); + if (scheduler && !scheduler->isPartialScheduler()) { + if (model.isOfType(storm::models::ModelType::Mdp)) { + resultType = storm::models::ModelType::Dtmc; + } + // Note that converting deterministic MAs to CTMCs via state elimination does not preserve all properties (e.g. step bounded) + } + + return storm::utility::builder::buildModelFromComponents(resultType, std::move(components)); } template class SparseModelMemoryProduct; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index 55a72172d..b37527542 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -8,6 +8,7 @@ #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/storage/Scheduler.h" namespace storm { namespace storage { @@ -32,8 +33,8 @@ namespace storm { // 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(); + // Invokes the building of the product under the specified scheduler (if given). + std::shared_ptr> build(boost::optional> const& scheduler = boost::none); // Retrieves the state of the resulting model that represents the given memory and model state. // Should only be called AFTER calling build(); @@ -47,20 +48,22 @@ namespace storm { std::vector computeMemorySuccessors() const; // Computes the reachable states of the resulting model - void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates); + void computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler); // Methods that build the model components // Matrix for deterministic models storm::storage::SparseMatrix buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const; // Matrix for nondeterministic models storm::storage::SparseMatrix buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const; + // 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; // Reward models - std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors) const; + std::unordered_map> buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const; // Builds the resulting model - std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const; + std::shared_ptr> buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) From 4251c9f5252508e9ed8fa4a4907ff263dcad74e4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 10:56:28 +0200 Subject: [PATCH 4/9] added function to build a trivial memory structure --- .../multiobjective/SparseMultiObjectivePreprocessor.cpp | 4 +--- .../storage/memorystructure/MemoryStructureBuilder.cpp | 7 +++++++ src/storm/storage/memorystructure/MemoryStructureBuilder.h | 5 +++++ 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index 0596303c8..09f0fdc6a 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -69,9 +69,7 @@ namespace storm { template SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { - storm::storage::MemoryStructureBuilder memoryBuilder(1, model); - memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); - memory = std::make_shared(memoryBuilder.build()); + memory = std::make_shared(storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(model)); // The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names memoryLabelPrefix = "mem"; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 9ee23eaa6..696e9662a 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -83,6 +83,13 @@ namespace storm { return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates)); } + template + MemoryStructure MemoryStructureBuilder::buildTrivialMemoryStructure(storm::models::sparse::Model const& model) { + MemoryStructureBuilder memoryBuilder(1, model); + memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); + return memoryBuilder.build(); + } + template class MemoryStructureBuilder; template class MemoryStructureBuilder; template class MemoryStructureBuilder; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index 9fbe65c78..1cb51f384 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -57,6 +57,11 @@ namespace storm { */ MemoryStructure build(); + /*! + * Builds a trivial memory structure for the given model (consisting of a single memory state) + */ + static MemoryStructure buildTrivialMemoryStructure(storm::models::sparse::Model const& model); + private: storm::models::sparse::Model const& model; From 7bd9ef798f827e2f0c48305295b0dd6189d87cc9 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 10:57:07 +0200 Subject: [PATCH 5/9] returning the memory structure of a scheduler --- src/storm/storage/Scheduler.cpp | 5 +++++ src/storm/storage/Scheduler.h | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index a1dc1ecbd..7ddc7e457 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -86,6 +86,11 @@ namespace storm { return memoryStructure ? memoryStructure->getNumberOfStates() : 1; } + template + boost::optional const& Scheduler::getMemoryStructure() const { + return memoryStructure; + } + template void Scheduler::printToStream(std::ostream& out, std::shared_ptr> model, bool skipUniqueChoices) const { STORM_LOG_THROW(model == nullptr || model->getNumberOfStates() == schedulerChoices.front().size(), storm::exceptions::InvalidOperationException, "The given model is not compatible with this scheduler."); diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index c1c3a5f88..b51e308b9 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -70,6 +70,11 @@ namespace storm { * Retrieves the number of memory states this scheduler considers. */ uint_fast64_t getNumberOfMemoryStates() const; + + /*! + * Retrieves the memory structure associated with this scheduler + */ + boost::optional const& getMemoryStructure() const; /*! * Returns a copy of this scheduler with the new value type From a348f6ea8e828aa7de690250c157d45b9bc6caed Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 11:24:24 +0200 Subject: [PATCH 6/9] function to apply a given scheduler to a nondeterministic model --- .../models/sparse/NondeterministicModel.cpp | 20 +++++++++++++++++++ .../models/sparse/NondeterministicModel.h | 14 +++++++++++++ 2 files changed, 34 insertions(+) diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index e823d455a..5b5aebe89 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -2,6 +2,9 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/storage/Scheduler.h" +#include "storm/storage/memorystructure/MemoryStructureBuilder.h" +#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -46,6 +49,23 @@ namespace storm { } } + template + std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { + boost::optional> memoryProduct; + if (scheduler.isMemorylessScheduler()) { + storm::storage::MemoryStructure memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); + memoryProduct = memStruct.product(*this); + } else { + boost::optional const& memStruct = scheduler.getMemoryStructure(); + STORM_LOG_ASSERT(memStruct, "Memoryless scheduler without memory structure."); + memoryProduct = memStruct->product(*this); + } + if (!dropUnreachableStates) { + memoryProduct->setBuildFullProduct(); + } + return memoryProduct->build(scheduler); + } + template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 1f2bd157a..ab0a21a04 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -5,6 +5,13 @@ #include "storm/utility/OsDetection.h" namespace storm { + + // Forward declare Scheduler class. + namespace storage { + template + class Scheduler; + } + namespace models { namespace sparse { @@ -48,6 +55,13 @@ namespace storm { virtual void reduceToStateBasedRewards() override; + /*! + * Applies the given scheduler to this model. + * @param scheduler the considered scheduler. + * @param dropUnreachableStates if set, the resulting model only considers the states that are reachable from an initial state + */ + std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates = true); + virtual void printModelInformationToStream(std::ostream& out) const override; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; From 6af15f3a0d32f17dd624a7486989e52d9557a98a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 11:29:34 +0200 Subject: [PATCH 7/9] Memory Structure Product with custom reward model type --- .../memorystructure/MemoryStructure.cpp | 8 +- .../storage/memorystructure/MemoryStructure.h | 7 +- .../MemoryStructureBuilder.cpp | 1 + .../SparseModelMemoryProduct.cpp | 88 ++++++++++--------- .../SparseModelMemoryProduct.h | 12 +-- 5 files changed, 62 insertions(+), 54 deletions(-) diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index 3d9348c44..499bc4db6 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -106,9 +106,9 @@ namespace storm { return MemoryStructure(std::move(resultTransitions), std::move(resultLabeling), std::move(resultInitialMemoryStates)); } - template - SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const { - return SparseModelMemoryProduct(sparseModel, *this); + template + SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const { + return SparseModelMemoryProduct(sparseModel, *this); } std::string MemoryStructure::toString() const { @@ -143,7 +143,9 @@ namespace storm { } template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; + template SparseModelMemoryProduct> MemoryStructure::product(storm::models::sparse::Model> const& sparseModel) const; template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; + template SparseModelMemoryProduct MemoryStructure::product(storm::models::sparse::Model const& sparseModel) const; } } diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index 9df320fd3..64bd7aaa9 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -6,11 +6,12 @@ #include "storm/logic/Formula.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/Model.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace storage { - template + template class SparseModelMemoryProduct; /*! @@ -53,8 +54,8 @@ namespace storm { * Builds the product of this memory structure and the given sparse model. * An exception is thrown if the state labelings of this memory structure and the given model are not disjoint. */ - template - SparseModelMemoryProduct product(storm::models::sparse::Model const& sparseModel) const; + template > + SparseModelMemoryProduct product(storm::models::sparse::Model const& sparseModel) const; std::string toString() const; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 696e9662a..148cbf2ca 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -91,6 +91,7 @@ namespace storm { } template class MemoryStructureBuilder; + template class MemoryStructureBuilder>; template class MemoryStructureBuilder; template class MemoryStructureBuilder; diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index 97e601f52..58f773cfe 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -17,24 +17,24 @@ namespace storm { namespace storage { - template - SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { + template + SparseModelMemoryProduct::SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memory.getNumberOfStates(), false); } - template - void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { + template + void SparseModelMemoryProduct::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { reachableStates.set(modelState * memory.getNumberOfStates() + memoryState, true); } - template - void SparseModelMemoryProduct::setBuildFullProduct() { + template + void SparseModelMemoryProduct::setBuildFullProduct() { reachableStates.clear(); reachableStates.complement(); } - template - std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { + template + std::shared_ptr> SparseModelMemoryProduct::build(boost::optional> const& scheduler) { uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -70,7 +70,7 @@ namespace storm { transitionMatrix = buildNondeterministicTransitionMatrix(memorySuccessors); } storm::models::sparse::StateLabeling labeling = buildStateLabeling(transitionMatrix); - std::unordered_map> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); + std::unordered_map rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); // 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); @@ -80,13 +80,13 @@ namespace storm { } - template - uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { + template + uint64_t const& SparseModelMemoryProduct::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } - template - std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { + template + std::vector SparseModelMemoryProduct::computeMemorySuccessors() const { uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); uint64_t memoryStateCount = memory.getNumberOfStates(); std::vector result(modelTransitionCount * memoryStateCount, std::numeric_limits::max()); @@ -104,8 +104,8 @@ namespace storm { return result; } - template - void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { + template + void SparseModelMemoryProduct::computeReachableStates(std::vector const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional> const& scheduler) { 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) @@ -156,8 +156,8 @@ namespace storm { } } - template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildDeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResTransitions = 0; @@ -182,8 +182,8 @@ namespace storm { return builder.build(); } - template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildNondeterministicTransitionMatrix(std::vector const& memorySuccessors) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; @@ -216,8 +216,8 @@ namespace storm { return builder.build(); } - template - storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { + template + storm::storage::SparseMatrix SparseModelMemoryProduct::buildTransitionMatrixForScheduler(std::vector const& memorySuccessors, storm::storage::Scheduler const& scheduler) const { uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = reachableStates.getNumberOfSetBits(); uint64_t numResChoices = 0; @@ -311,8 +311,8 @@ namespace storm { return builder.build(); } - template - storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { + template + storm::models::sparse::StateLabeling SparseModelMemoryProduct::buildStateLabeling(storm::storage::SparseMatrix const& resultTransitionMatrix) const { uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -351,16 +351,19 @@ namespace storm { 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> result; + template + std::unordered_map SparseModelMemoryProduct::buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const { + + typedef typename RewardModelType::ValueType RewardValueType; + + std::unordered_map result; uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); for (auto const& rewardModel : model.getRewardModels()) { - boost::optional> stateRewards; + boost::optional> stateRewards; if (rewardModel.second.hasStateRewards()) { - stateRewards = std::vector(numResStates, storm::utility::zero()); + stateRewards = std::vector(numResStates, storm::utility::zero()); uint64_t modelState = 0; for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) { if (!storm::utility::isZero(modelStateReward)) { @@ -375,9 +378,9 @@ namespace storm { ++modelState; } } - boost::optional> stateActionRewards; + boost::optional> stateActionRewards; if (rewardModel.second.hasStateActionRewards()) { - stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); + stateActionRewards = std::vector(resultTransitionMatrix.getRowCount(), storm::utility::zero()); uint64_t modelState = 0; uint64_t modelRow = 0; for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { @@ -402,9 +405,9 @@ namespace storm { ++modelRow; } } - boost::optional> transitionRewards; + boost::optional> transitionRewards; if (rewardModel.second.hasTransitionRewards()) { - storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); + storm::storage::SparseMatrixBuilder builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { if (resState < numResStates) { @@ -412,7 +415,7 @@ namespace storm { uint64_t memoryState = stateIndex % memoryStateCount; uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState); if (scheduler && scheduler->getChoice(modelState, memoryState).isDefined()) { - std::map rewards; + std::map rewards; for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) { uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset; auto transitionEntryIt = model.getTransitionMatrix().getRow(modelRowIndex).begin(); @@ -454,14 +457,14 @@ namespace storm { } transitionRewards = builder.build(); } - result.insert(std::make_pair(rewardModel.first, storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); + result.insert(std::make_pair(rewardModel.first, RewardModelType(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards)))); } return result; } - template - std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels, boost::optional> const& scheduler) const { - storm::storage::sparse::ModelComponents> components (std::move(matrix), std::move(labeling), std::move(rewardModels)); + template + std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels, boost::optional> const& scheduler) const { + storm::storage::sparse::ModelComponents components (std::move(matrix), std::move(labeling), std::move(rewardModels)); if (model.isOfType(storm::models::ModelType::Ctmc)) { components.rateTransitions = true; @@ -472,8 +475,8 @@ namespace storm { std::vector resultExitRates; resultExitRates.reserve(components.transitionMatrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); - auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); - auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); + auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); + auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); uint64_t stateIndex = 0; for (auto const& resState : toResultStateMapping) { @@ -502,9 +505,10 @@ namespace storm { return storm::utility::builder::buildModelFromComponents(resultType, std::move(components)); } - template class SparseModelMemoryProduct; - template class SparseModelMemoryProduct; - template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct>; + template class SparseModelMemoryProduct; + template class SparseModelMemoryProduct; } } diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h index b37527542..fb959daa5 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h @@ -21,11 +21,11 @@ namespace storm { * memory structure. * An exception is thrown if the state labelings are not disjoint. */ - template + template > class SparseModelMemoryProduct { public: - SparseModelMemoryProduct(storm::models::sparse::Model const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + 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); @@ -34,7 +34,7 @@ namespace storm { void setBuildFullProduct(); // Invokes the building of the product under the specified scheduler (if given). - std::shared_ptr> build(boost::optional> const& scheduler = boost::none); + std::shared_ptr> build(boost::optional> const& scheduler = boost::none); // Retrieves the state of the resulting model that represents the given memory and model state. // Should only be called AFTER calling build(); @@ -60,10 +60,10 @@ namespace storm { // 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, boost::optional> const& scheduler) const; + std::unordered_map buildRewardModels(storm::storage::SparseMatrix const& resultTransitionMatrix, std::vector const& memorySuccessors, boost::optional> const& scheduler) const; // 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, boost::optional> const& scheduler) const; // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState) @@ -72,7 +72,7 @@ namespace storm { // 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::models::sparse::Model const& model; storm::storage::MemoryStructure const& memory; }; From 5651b237714e705aee4912a216be53d398cdb227 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 11:58:07 +0200 Subject: [PATCH 8/9] fixing minor compiling issue --- .../models/sparse/NondeterministicModel.cpp | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 5b5aebe89..32839a630 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -51,19 +51,21 @@ namespace storm { template std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { - boost::optional> memoryProduct; if (scheduler.isMemorylessScheduler()) { - storm::storage::MemoryStructure memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); - memoryProduct = memStruct.product(*this); + auto memoryProduct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this).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."); - memoryProduct = memStruct->product(*this); - } - if (!dropUnreachableStates) { - memoryProduct->setBuildFullProduct(); + auto memoryProduct = memStruct->product(*this); + if (!dropUnreachableStates) { + memoryProduct.setBuildFullProduct(); + } + return memoryProduct.build(scheduler); } - return memoryProduct->build(scheduler); } template From e8e189723fe6c6e1e7db182ad83f21065981fdc2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Jul 2017 13:06:05 +0200 Subject: [PATCH 9/9] fixed applying memoryless schedulers --- src/storm/models/sparse/NondeterministicModel.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 32839a630..3382bfd95 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -52,7 +52,8 @@ namespace storm { template std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { if (scheduler.isMemorylessScheduler()) { - auto memoryProduct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this).product(*this); + auto memStruct = storm::storage::MemoryStructureBuilder::buildTrivialMemoryStructure(*this); + auto memoryProduct = memStruct.product(*this); if (!dropUnreachableStates) { memoryProduct.setBuildFullProduct(); }