From 4ddb9c43376acc978ab19c030719d38f0c0ef143 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 10 Aug 2021 14:30:19 +0200 Subject: [PATCH] Some simplifications for memory structure. --- .../storage/memorystructure/MemoryStructure.cpp | 10 +--------- .../storage/memorystructure/MemoryStructure.h | 11 +++++------ .../memorystructure/MemoryStructureBuilder.cpp | 7 +------ .../memorystructure/MemoryStructureBuilder.h | 16 +++++----------- .../memorystructure/SparseModelMemoryProduct.cpp | 2 +- 5 files changed, 13 insertions(+), 33 deletions(-) diff --git a/src/storm/storage/memorystructure/MemoryStructure.cpp b/src/storm/storage/memorystructure/MemoryStructure.cpp index 6103c05dd..1bcded410 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.cpp +++ b/src/storm/storage/memorystructure/MemoryStructure.cpp @@ -11,14 +11,6 @@ namespace storm { namespace storage { - MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(true) { - // intentionally left empty - } - - MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates) : transitions(std::move(transitionMatrix)), stateLabeling(std::move(memoryStateLabeling)), initialMemoryStates(std::move(initialMemoryStates)), onlyInitialStatesRelevant(true) { - // intentionally left empty - } - MemoryStructure::MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates, bool onlyInitialStatesRelevant) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(onlyInitialStatesRelevant) { // intentionally left empty } @@ -27,7 +19,7 @@ namespace storm { // intentionally left empty } - bool MemoryStructure::IsOnlyInitialStatesRelevantSet() const { + bool MemoryStructure::isOnlyInitialStatesRelevantSet() const { return onlyInitialStatesRelevant; } diff --git a/src/storm/storage/memorystructure/MemoryStructure.h b/src/storm/storage/memorystructure/MemoryStructure.h index 2476a4e63..e831b58cf 100644 --- a/src/storm/storage/memorystructure/MemoryStructure.h +++ b/src/storm/storage/memorystructure/MemoryStructure.h @@ -33,14 +33,13 @@ namespace storm { * * @param transitionMatrix The transition matrix * @param memoryStateLabeling A labeling of the memory states to specify, e.g., accepting states - * @param initialMemoryStates assigns an initial memory state to each initial state of the model. + * @param initialMemoryStates assigns an initial memory state to each (initial?) state of the model. + * @param onlyInitialStatesRelevant if true, initial memory states are only provided for each initial model state. Otherwise, an initial memory state is provided for *every* model state. */ - MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates); - MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates); - MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates, bool onlyInitialStatesRelevant); - MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates, bool onlyInitialStatesRelevant); + MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector const& initialMemoryStates, bool onlyInitialStatesRelevant = true); + MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector&& initialMemoryStates, bool onlyInitialStatesRelevant = true); - bool IsOnlyInitialStatesRelevantSet () const; + bool isOnlyInitialStatesRelevantSet () const; TransitionMatrix const& getTransitionMatrix() const; storm::models::sparse::StateLabeling const& getStateLabeling() const; std::vector const& getInitialMemoryStates() const; diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp index 859a92635..54accf38a 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp @@ -9,18 +9,13 @@ namespace storm { namespace storage { - template - MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0), onlyInitialStatesRelevant(true) { - // Intentionally left empty - } - template MemoryStructureBuilder::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant) : model(model), transitions(numberOfMemoryStates, std::vector>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(onlyInitialStatesRelevant ? model.getInitialStates().getNumberOfSetBits() : model.getNumberOfStates(), 0), onlyInitialStatesRelevant(onlyInitialStatesRelevant) { // Intentionally left empty } template - MemoryStructureBuilder::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(true) { + MemoryStructureBuilder::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(memoryStructure.isOnlyInitialStatesRelevantSet()) { // Intentionally left empty } diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h index 1d067a4bc..b038fb98f 100644 --- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h +++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h @@ -14,18 +14,12 @@ namespace storm { class MemoryStructureBuilder { public: - /*! - * Initializes a new builder for a memory structure - * @param numberOfMemoryStates The number of states the resulting memory structure should have - */ - MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model); - - /*! + /*! * Initializes a new builder with the data from the provided memory structure * @param numberOfMemoryStates The number of states the resulting memory structure should have - * @param allModelStatesRelevant Consider non-initial model states + * @param onlyInitialStatesRelevant If true, assume that we only consider the fragment reachable from initial model states. If false, initial memory states need to be provided for *all* model states. */ - MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant); + MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model const& model, bool onlyInitialStatesRelevant = true); /*! * Initializes a new builder with the data from the provided memory structure @@ -33,11 +27,11 @@ namespace storm { MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model const& model); /*! - * Specifies for the given initial state of the model the corresponding initial memory state. + * Specifies for the given state of the model the corresponding initial memory state. * * @note The default initial memory state is 0. * - * @param initialModelState the index of an initial state of the model. + * @param initialModelState the index of a state of the model. Has to be an initial state iff `onlyInitialStatesRelevant` is true. * @param initialMemoryState the initial memory state associated to the corresponding model state. */ void setInitialMemoryState(uint_fast64_t initialModelState, uint_fast64_t initialMemoryState); diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index b80910704..76fa593ba 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -38,7 +38,7 @@ namespace storm { // Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount) storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false); auto memoryInitIt = memory.getInitialMemoryStates().begin(); - if (memory.IsOnlyInitialStatesRelevantSet()) { + if (memory.isOnlyInitialStatesRelevantSet()) { for (auto modelInit : model.getInitialStates()) { initialStates.set(modelInit * memoryStateCount + *memoryInitIt, true); ++memoryInitIt;