From 6af15f3a0d32f17dd624a7486989e52d9557a98a Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@cs.rwth-aachen.de> Date: Tue, 18 Jul 2017 11:29:34 +0200 Subject: [PATCH] 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 <typename ValueType> - SparseModelMemoryProduct<ValueType> MemoryStructure::product(storm::models::sparse::Model<ValueType> const& sparseModel) const { - return SparseModelMemoryProduct<ValueType>(sparseModel, *this); + template <typename ValueType, typename RewardModelType> + SparseModelMemoryProduct<ValueType, RewardModelType> MemoryStructure::product(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel) const { + return SparseModelMemoryProduct<ValueType, RewardModelType>(sparseModel, *this); } std::string MemoryStructure::toString() const { @@ -143,7 +143,9 @@ namespace storm { } template SparseModelMemoryProduct<double> MemoryStructure::product(storm::models::sparse::Model<double> const& sparseModel) const; + template SparseModelMemoryProduct<double, storm::models::sparse::StandardRewardModel<storm::Interval>> MemoryStructure::product(storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& sparseModel) const; template SparseModelMemoryProduct<storm::RationalNumber> MemoryStructure::product(storm::models::sparse::Model<storm::RationalNumber> const& sparseModel) const; + template SparseModelMemoryProduct<storm::RationalFunction> MemoryStructure::product(storm::models::sparse::Model<storm::RationalFunction> 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 <typename ValueType> + template <typename ValueType, typename RewardModelType> 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 <typename ValueType> - SparseModelMemoryProduct<ValueType> product(storm::models::sparse::Model<ValueType> const& sparseModel) const; + template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> + SparseModelMemoryProduct<ValueType, RewardModelType> product(storm::models::sparse::Model<ValueType, RewardModelType> 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<double>; + template class MemoryStructureBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>>; template class MemoryStructureBuilder<storm::RationalNumber>; template class MemoryStructureBuilder<storm::RationalFunction>; 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 <typename ValueType> - SparseModelMemoryProduct<ValueType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { + template <typename ValueType, typename RewardModelType> + SparseModelMemoryProduct<ValueType, RewardModelType>::SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure) : model(sparseModel), memory(memoryStructure) { reachableStates = storm::storage::BitVector(model.getNumberOfStates() * memory.getNumberOfStates(), false); } - template <typename ValueType> - void SparseModelMemoryProduct<ValueType>::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { + template <typename ValueType, typename RewardModelType> + void SparseModelMemoryProduct<ValueType, RewardModelType>::addReachableState(uint64_t const& modelState, uint64_t const& memoryState) { reachableStates.set(modelState * memory.getNumberOfStates() + memoryState, true); } - template <typename ValueType> - void SparseModelMemoryProduct<ValueType>::setBuildFullProduct() { + template <typename ValueType, typename RewardModelType> + void SparseModelMemoryProduct<ValueType, RewardModelType>::setBuildFullProduct() { reachableStates.clear(); reachableStates.complement(); } - template <typename ValueType> - std::shared_ptr<storm::models::sparse::Model<ValueType>> SparseModelMemoryProduct<ValueType>::build(boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) { + template <typename ValueType, typename RewardModelType> + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> SparseModelMemoryProduct<ValueType, RewardModelType>::build(boost::optional<storm::storage::Scheduler<ValueType>> 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<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels = buildRewardModels(transitionMatrix, memorySuccessors, scheduler); + std::unordered_map<std::string, RewardModelType> 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 <typename ValueType> - uint64_t const& SparseModelMemoryProduct<ValueType>::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { + template <typename ValueType, typename RewardModelType> + uint64_t const& SparseModelMemoryProduct<ValueType, RewardModelType>::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const { return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState]; } - template <typename ValueType> - std::vector<uint64_t> SparseModelMemoryProduct<ValueType>::computeMemorySuccessors() const { + template <typename ValueType, typename RewardModelType> + std::vector<uint64_t> SparseModelMemoryProduct<ValueType, RewardModelType>::computeMemorySuccessors() const { uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount(); uint64_t memoryStateCount = memory.getNumberOfStates(); std::vector<uint64_t> result(modelTransitionCount * memoryStateCount, std::numeric_limits<uint64_t>::max()); @@ -104,8 +104,8 @@ namespace storm { return result; } - template <typename ValueType> - void SparseModelMemoryProduct<ValueType>::computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) { + template <typename ValueType, typename RewardModelType> + void SparseModelMemoryProduct<ValueType, RewardModelType>::computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::Scheduler<ValueType>> 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 <typename ValueType> - storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildDeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const { + template <typename ValueType, typename RewardModelType> + storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildDeterministicTransitionMatrix(std::vector<uint64_t> 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 <typename ValueType> - storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildNondeterministicTransitionMatrix(std::vector<uint64_t> const& memorySuccessors) const { + template <typename ValueType, typename RewardModelType> + storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildNondeterministicTransitionMatrix(std::vector<uint64_t> 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 <typename ValueType> - storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildTransitionMatrixForScheduler(std::vector<uint64_t> const& memorySuccessors, storm::storage::Scheduler<ValueType> const& scheduler) const { + template <typename ValueType, typename RewardModelType> + storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildTransitionMatrixForScheduler(std::vector<uint64_t> const& memorySuccessors, storm::storage::Scheduler<ValueType> 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 <typename ValueType> - storm::models::sparse::StateLabeling SparseModelMemoryProduct<ValueType>::buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const { + template <typename ValueType, typename RewardModelType> + storm::models::sparse::StateLabeling SparseModelMemoryProduct<ValueType, RewardModelType>::buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const { uint64_t modelStateCount = model.getNumberOfStates(); uint64_t memoryStateCount = memory.getNumberOfStates(); @@ -351,16 +351,19 @@ namespace storm { return resultLabeling; } - template <typename ValueType> - std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> SparseModelMemoryProduct<ValueType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const { - std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> result; + template <typename ValueType, typename RewardModelType> + std::unordered_map<std::string, RewardModelType> SparseModelMemoryProduct<ValueType, RewardModelType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const { + + typedef typename RewardModelType::ValueType RewardValueType; + + std::unordered_map<std::string, RewardModelType> result; uint64_t memoryStateCount = memory.getNumberOfStates(); uint64_t numResStates = resultTransitionMatrix.getRowGroupCount(); for (auto const& rewardModel : model.getRewardModels()) { - boost::optional<std::vector<ValueType>> stateRewards; + boost::optional<std::vector<RewardValueType>> stateRewards; if (rewardModel.second.hasStateRewards()) { - stateRewards = std::vector<ValueType>(numResStates, storm::utility::zero<ValueType>()); + stateRewards = std::vector<RewardValueType>(numResStates, storm::utility::zero<RewardValueType>()); 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<std::vector<ValueType>> stateActionRewards; + boost::optional<std::vector<RewardValueType>> stateActionRewards; if (rewardModel.second.hasStateActionRewards()) { - stateActionRewards = std::vector<ValueType>(resultTransitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); + stateActionRewards = std::vector<RewardValueType>(resultTransitionMatrix.getRowCount(), storm::utility::zero<RewardValueType>()); uint64_t modelState = 0; uint64_t modelRow = 0; for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) { @@ -402,9 +405,9 @@ namespace storm { ++modelRow; } } - boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards; + boost::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards; if (rewardModel.second.hasTransitionRewards()) { - storm::storage::SparseMatrixBuilder<ValueType> builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount()); + storm::storage::SparseMatrixBuilder<RewardValueType> 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<uint64_t, ValueType> rewards; + std::map<uint64_t, RewardValueType> 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<ValueType>(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 <typename ValueType> - std::shared_ptr<storm::models::sparse::Model<ValueType>> SparseModelMemoryProduct<ValueType>::buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>>&& rewardModels, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const { - storm::storage::sparse::ModelComponents<ValueType, storm::models::sparse::StandardRewardModel<ValueType>> components (std::move(matrix), std::move(labeling), std::move(rewardModels)); + template <typename ValueType, typename RewardModelType> + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> SparseModelMemoryProduct<ValueType, RewardModelType>::buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const { + storm::storage::sparse::ModelComponents<ValueType, RewardModelType> 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<ValueType> resultExitRates; resultExitRates.reserve(components.transitionMatrix.getRowGroupCount()); storm::storage::BitVector resultMarkovianStates(numResStates, false); - auto const& modelExitRates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getExitRates(); - auto const& modelMarkovianStates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getMarkovianStates(); + auto const& modelExitRates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const&>(model).getExitRates(); + auto const& modelMarkovianStates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> 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<double>; - template class SparseModelMemoryProduct<storm::RationalNumber>; - template class SparseModelMemoryProduct<storm::RationalFunction>; + template class SparseModelMemoryProduct<double>; + template class SparseModelMemoryProduct<double, storm::models::sparse::StandardRewardModel<storm::Interval>>; + template class SparseModelMemoryProduct<storm::RationalNumber>; + template class SparseModelMemoryProduct<storm::RationalFunction>; } } 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 <typename ValueType> + template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> class SparseModelMemoryProduct { public: - SparseModelMemoryProduct(storm::models::sparse::Model<ValueType> const& sparseModel, storm::storage::MemoryStructure const& memoryStructure); + SparseModelMemoryProduct(storm::models::sparse::Model<ValueType, RewardModelType> 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<storm::models::sparse::Model<ValueType>> build(boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler = boost::none); + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build(boost::optional<storm::storage::Scheduler<ValueType>> 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<ValueType> const& resultTransitionMatrix) const; // Reward models - std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const; + std::unordered_map<std::string, RewardModelType> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const; // Builds the resulting model - std::shared_ptr<storm::models::sparse::Model<ValueType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>>&& rewardModels, boost::optional<storm::storage::Scheduler<ValueType>> const& scheduler) const; + std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, RewardModelType>&& rewardModels, boost::optional<storm::storage::Scheduler<ValueType>> 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<ValueType> const& model; + storm::models::sparse::Model<ValueType, RewardModelType> const& model; storm::storage::MemoryStructure const& memory; };