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;