From 0e9880c9f8122eb567a095386fbfaffab7f3e7ec Mon Sep 17 00:00:00 2001 From: radioGiorgio Date: Fri, 21 Jun 2019 07:01:23 -0700 Subject: [PATCH] non deterministic transitions based memory structure --- ...rministicTransitionsBasedMemoryProduct.cpp | 282 ++++++++++++++++++ ...terministicTransitionsBasedMemoryProduct.h | 54 ++++ 2 files changed, 336 insertions(+) create mode 100644 src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.cpp create mode 100644 src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.h diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.cpp new file mode 100644 index 000000000..bac35724c --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.cpp @@ -0,0 +1,282 @@ +// +// Created by Florent Delgrange on 2019-05-28. +// + +#include "SparseModelNondeterministicTransitionsBasedMemoryProduct.h" + +namespace storm { + namespace storage { + + template + SparseModelNondeterministicTransitionsBasedMemoryProduct::SparseModelNondeterministicTransitionsBasedMemoryProduct(SparseModelType const& model, storm::storage::NondeterministicMemoryStructure const& memory, bool forceLabeling) + : model(model), memory(memory), productStates(model.getNumberOfStates()), forceLabeling(forceLabeling) + {} + + template + std::shared_ptr SparseModelNondeterministicTransitionsBasedMemoryProduct::build() { + // For simplicity we first build the 'full' product of model and memory (with model.numStates * memory.numStates states). + storm::storage::sparse::ModelComponents components; + components.transitionMatrix = buildTransitions(); + components.stateLabeling = buildStateLabeling(); + // Now delete unreachable states. + storm::storage::BitVector allStates(components.transitionMatrix.getRowGroupCount(), true); + auto reachableStates = storm::utility::graph::getReachableStates(components.transitionMatrix, components.stateLabeling.getStates("init"), allStates, ~allStates); + components.transitionMatrix = components.transitionMatrix.getSubmatrix(true, reachableStates, reachableStates); + components.stateLabeling = components.stateLabeling.getSubLabeling(reachableStates); + + // build the remaining components + for (auto const& rewModel : model.getRewardModels()) { + components.rewardModels.emplace(rewModel.first, + buildRewardModel(rewModel.second, reachableStates, components.transitionMatrix)); + } + + // build the offset vector, that allows to maintain getter indices + fullProductStatesOffset = std::move(generateOffsetVector(reachableStates)); + + return std::make_shared(std::move(components)); + } + + template + storm::storage::SparseMatrix::ValueType> SparseModelNondeterministicTransitionsBasedMemoryProduct::buildTransitions() { + storm::storage::SparseMatrix const& origTransitions = model.getTransitionMatrix(); + uint64_t numRows = 0; + uint64_t numEntries = 0; + uint64_t numberOfStates = model.getNumberOfStates() * memory.getNumberOfStates() * (1 + model.getNumberOfTransitions()); + productStates[0] = 0; + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++ modelState) { + if (modelState < model.getNumberOfStates() - 1) { + productStates[modelState + 1] = productStates[modelState] + memory.getNumberOfStates() * ( 1 + origTransitions.getRowGroupEntryCount(modelState) ); + } + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++ memState) { + for (uint64_t row = origTransitions.getRowGroupIndices()[modelState]; + row < origTransitions.getRowGroupIndices()[modelState + 1]; + ++ row) { + numRows += 1 + origTransitions.getRow(row).getNumberOfEntries() * memory.getNumberOfOutgoingTransitions(memState); + numEntries += origTransitions.getRow(row).getNumberOfEntries() * (1 + memory.getNumberOfOutgoingTransitions(memState)); + } + } + } + storm::storage::SparseMatrixBuilder builder(numRows, + numberOfStates, + numEntries, + true, + true, + numberOfStates); + + uint64_t row = 0; + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++ modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++ memState) { + builder.newRowGroup(row); + uint64_t entryCount = 0; + for (uint64_t origRow = origTransitions.getRowGroupIndices()[modelState]; origRow < origTransitions.getRowGroupIndices()[modelState + 1]; ++origRow) { + for (auto const& entry : origTransitions.getRow(origRow)) { + uint64_t productState = getProductState(modelState, memState); + builder.addNextValue(row, productState + 1 + entryCount, entry.getValue()); + ++ entryCount; + } + ++row; + } + // transition states + for (uint64_t origRow = origTransitions.getRowGroupIndices()[modelState]; origRow < origTransitions.getRowGroupIndices()[modelState + 1]; ++origRow) { + for (auto const& entry : origTransitions.getRow(origRow)) { + builder.newRowGroup(row); + for (auto const& memStatePrime : memory.getTransitions(memState)) { + builder.addNextValue(row, getProductState(entry.getColumn(), memStatePrime), storm::utility::one()); + ++row; + } + } + } + } + } + return builder.build(); + } + + template + storm::models::sparse::StateLabeling SparseModelNondeterministicTransitionsBasedMemoryProduct::buildStateLabeling() const { + storm::storage::SparseMatrix const& origTransitions = model.getTransitionMatrix(); + // storm::storage::SparseMatrix backwardTransitions = origTransitions.transpose(true); + uint64_t numberOfStates = model.getNumberOfStates() * memory.getNumberOfStates() * (1 + model.getNumberOfTransitions()); + storm::models::sparse::StateLabeling labeling(numberOfStates); + for (auto const& labelName : model.getStateLabeling().getLabels()) { + storm::storage::BitVector newStates(numberOfStates, false); + + // The init label is only assigned to Product states with the initial memory state + if (labelName == "init") { + for (auto const& modelState : model.getStateLabeling().getStates(labelName)) { + uint64_t nextProductState = getProductState(modelState, memory.getInitialState() + 1); //memory.getInitialState() < memory.getNumberOfStates() - 1 ? getProductState(modelState, memory.getInitialState() + 1) : getProductState(modelState + 1, 0); + // by assuming that all states between (s, m) and (s, m + 1) are labeled with s + for (uint64_t productState = getProductState(modelState, memory.getInitialState()); productState < nextProductState; ++ productState) { + newStates.set(productState); + } + } + } else { + for (auto const& modelState : model.getStateLabeling().getStates(labelName)) { + // by assuming that all states between (s, 0) and (s + 1, 0) are labeled with labels of s + for (uint64_t productState = getProductState(modelState, 0); productState < getProductState(modelState, memory.getNumberOfStates()); ++ productState) { + newStates.set(productState); + } + } + } + labeling.addLabel(labelName, std::move(newStates)); + } + + auto addLabel = [&] (std::string const& labelName, uint64_t state) -> void { + if (not labeling.containsLabel(labelName)) { + labeling.addLabel(labelName); + } + labeling.addLabelToState(labelName, state); + }; + + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++ modelState) { + if (forceLabeling) { + for (uint64_t memoryState = 0; memoryState < memory.getNumberOfStates(); ++ memoryState) { + std::ostringstream stream; + stream << "m" << memoryState; + std::string labelName = stream.str(); + addLabel(labelName, getProductState(modelState, memoryState)); + } + } + uint64_t entryCount = 0; + for (uint64_t row = origTransitions.getRowGroupIndices()[modelState]; row < origTransitions.getRowGroupIndices()[modelState + 1]; ++ row) { + for (auto const& entry : origTransitions.getRow(row)) { + uint64_t const& successor = entry.getColumn(); + for (uint64_t memoryState = 0; memoryState < memory.getNumberOfStates(); ++ memoryState) { + uint64_t productState = getProductState(modelState, memoryState) + 1 + entryCount; + // origin state + if (model.getStateLabeling().getLabelsOfState(modelState).empty()) { + if (forceLabeling) { + std::ostringstream stream; + stream << "s" << modelState; + std::string labelName = stream.str(); + addLabel(labelName, productState); + } + } else { + for (auto const& labelName : model.getStateLabeling().getLabelsOfState(modelState)) { + addLabel(labelName, productState); + } + } + // memory labeling + if (forceLabeling) { + std::ostringstream stream; + stream << "m" << memoryState; + std::string labelName = stream.str(); + addLabel(labelName, productState); + } + // action labeling + if (forceLabeling and (not model.getOptionalChoiceLabeling() + or model.getChoiceLabeling().getLabelsOfChoice(row).empty())) { + std::ostringstream stream; + stream << "a" << row; + std::string labelName = stream.str(); + addLabel(labelName, productState); + } else if (model.getOptionalChoiceLabeling()) { + for (auto const &labelName : model.getChoiceLabeling().getLabelsOfChoice(row)) { + addLabel(labelName, productState); + } + } + // arrival state + if (model.getStateLabeling().getLabelsOfState(successor).empty()) { + if (forceLabeling) { + std::ostringstream stream; + stream << "s" << successor; + std::string labelName = stream.str(); + addLabel(labelName, productState); + } + } else { + for (auto const& labelName : model.getStateLabeling().getLabelsOfState(successor)) { + addLabel(labelName, productState); + } + } + } + ++ entryCount; + } + } + } + return labeling; + } + + template + storm::models::sparse::StandardRewardModel::ValueType> SparseModelNondeterministicTransitionsBasedMemoryProduct::buildRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& reachableStates, storm::storage::SparseMatrix const& resultTransitionMatrix) const { + boost::optional> stateRewards, actionRewards; + if (rewardModel.hasStateRewards()) { + stateRewards = std::vector(); + stateRewards->reserve(resultTransitionMatrix.getRowGroupCount()); + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++ modelState) { + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++ memState) { + if (reachableStates.get(getProductState(modelState, memState))) { + stateRewards->push_back(rewardModel.getStateReward(modelState)); + } + } + } + } + if (rewardModel.hasStateActionRewards()) { + actionRewards = std::vector(); + actionRewards->reserve(resultTransitionMatrix.getRowCount()); + for (uint64_t modelState = 0; modelState < model.getNumberOfStates(); ++ modelState) { + uint64_t numberOfModelOutgoingTransitions = model.getTransitionMatrix().getRowGroupEntryCount(modelState); + for (uint64_t memState = 0; memState < memory.getNumberOfStates(); ++ memState) { + uint64_t numberOfMemoryOutgoingTransitions = memory.getNumberOfOutgoingTransitions(memState); + if (reachableStates.get(getProductState(modelState, memState))) { + for (uint64_t origRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; origRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++ origRow) { + ValueType const& actionReward = rewardModel.getStateActionReward(origRow); + // push the reward of choosing a in (s, m) + actionRewards->push_back(actionReward); + } + // note that all outgoing model states are reachable by definition + actionRewards->insert(actionRewards->end(), numberOfModelOutgoingTransitions * numberOfMemoryOutgoingTransitions, storm::utility::zero()); + } + } + } + } + STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported."); + return storm::models::sparse::StandardRewardModel(std::move(stateRewards), std::move(actionRewards)); + } + + template + std::vector SparseModelNondeterministicTransitionsBasedMemoryProduct::generateOffsetVector(storm::storage::BitVector const& reachableStates) { + uint64_t numberOfStates = model.getNumberOfStates() * memory.getNumberOfStates() * (1 + model.getNumberOfTransitions()); + uint64_t offset = 0; + std::vector offsetVector(numberOfStates); + for (uint64_t state = 0; state < numberOfStates; ++ state) { + if (not reachableStates[state]) { + ++ offset; + } + offsetVector[state] = offset; + } + + return std::move(offsetVector); + } + + template + uint64_t SparseModelNondeterministicTransitionsBasedMemoryProduct::getProductState(uint64_t modelState, uint64_t memoryState) const { + uint64_t index = productStates[modelState] + memoryState * (1 + model.getTransitionMatrix().getRowGroupEntryCount(modelState)); + return index - (fullProductStatesOffset.empty() ? 0 : fullProductStatesOffset[index]); + } + + template + bool SparseModelNondeterministicTransitionsBasedMemoryProduct::isProductStateReachable(uint64_t modelState, uint64_t memoryState) const { + STORM_LOG_ASSERT(not fullProductStatesOffset.empty(), "Model not built"); + uint64_t index = productStates[modelState] + memoryState * (1 + model.getTransitionMatrix().getRowGroupEntryCount(modelState)); + return ( index == 0 and fullProductStatesOffset[index] == 0 ) or ( index > 0 and fullProductStatesOffset[index] == fullProductStatesOffset[index - 1] ); + } + + template + uint64_t SparseModelNondeterministicTransitionsBasedMemoryProduct::getModelState(uint64_t productState) const { + // binary search in the vector containing the product states indices + auto search = std::upper_bound(productStates.begin(), productStates.end(), productState); + uint64_t index = search - productStates.begin() - 1; + return index - (fullProductStatesOffset.empty() ? 0 : fullProductStatesOffset[index]); + } + + template + uint64_t SparseModelNondeterministicTransitionsBasedMemoryProduct::getMemoryState(uint64_t productState) const { + uint64_t modelState = getModelState(productState); + uint64_t offset = productState - productStates[modelState]; + uint64_t index = offset / (1 + model.getTransitionMatrix().getRowGroupEntryCount(modelState)); + return index - (fullProductStatesOffset.empty() ? 0 : fullProductStatesOffset[index]); + } + + template class SparseModelNondeterministicTransitionsBasedMemoryProduct>; + template class SparseModelNondeterministicTransitionsBasedMemoryProduct>; + } +} diff --git a/src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.h new file mode 100644 index 000000000..7f2335593 --- /dev/null +++ b/src/storm/storage/memorystructure/SparseModelNondeterministicTransitionsBasedMemoryProduct.h @@ -0,0 +1,54 @@ +// +// Created by Florent Delgrange on 2019-05-28. +// + +#ifndef STORM_SPARSEMODELNONDETERMINISTICTRANSITIONSBASEDMEMORYPRODUCT_H +#define STORM_SPARSEMODELNONDETERMINISTICTRANSITIONSBASEDMEMORYPRODUCT_H + +#include +#include +#include +#include +#include +#include +#include +#include + +namespace storm { + namespace storage { + + + template + class SparseModelNondeterministicTransitionsBasedMemoryProduct { + public: + + typedef typename SparseModelType::ValueType ValueType; + + SparseModelNondeterministicTransitionsBasedMemoryProduct(SparseModelType const& model, storm::storage::NondeterministicMemoryStructure const& memory, bool forceLabeling = false); + + std::shared_ptr build(); + + uint64_t getProductState(uint64_t modelState, uint64_t memoryState) const; + uint64_t getModelState(uint64_t productState) const; + uint64_t getMemoryState(uint64_t productState) const; + bool isProductStateReachable(uint64_t modelState, uint64_t memoryState) const; + + private: + storm::storage::SparseMatrix buildTransitions(); + storm::models::sparse::StateLabeling buildStateLabeling() const; + storm::models::sparse::StandardRewardModel buildRewardModel(storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& reachableStates, storm::storage::SparseMatrix const& resultTransitionMatrix) const; + + std::vector generateOffsetVector(storm::storage::BitVector const& reachableStates); + + SparseModelType const& model; + storm::storage::NondeterministicMemoryStructure const& memory; + std::vector productStates; // has a size equals to the number of states of the original model + std::vector fullProductStatesOffset; // has a size equal to the number of states of the full product + bool forceLabeling; + }; + + } +} + + +#endif //STORM_SPARSEMODELNONDETERMINISTICTRANSITIONSBASEDMEMORYPRODUCT_H