Some simplifications for memory structure.

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<uint_fast64_t> const& initialMemoryStates) : transitions(transitionMatrix), stateLabeling(memoryStateLabeling), initialMemoryStates(initialMemoryStates), onlyInitialStatesRelevant(true) {
-            // intentionally left empty
-        }
-        
-        MemoryStructure::MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& 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<uint_fast64_t> 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;
         }
 

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<uint_fast64_t> const& initialMemoryStates);
-            MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates);
-            MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant);
-            MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates, bool onlyInitialStatesRelevant);
+            MemoryStructure(TransitionMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& memoryStateLabeling, std::vector<uint_fast64_t> const& initialMemoryStates, bool onlyInitialStatesRelevant = true);
+            MemoryStructure(TransitionMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& memoryStateLabeling, std::vector<uint_fast64_t>&& initialMemoryStates, bool onlyInitialStatesRelevant = true);
 
-            bool IsOnlyInitialStatesRelevantSet () const;
+            bool isOnlyInitialStatesRelevantSet () const;
             TransitionMatrix const& getTransitionMatrix() const;
             storm::models::sparse::StateLabeling const& getStateLabeling() const;
             std::vector<uint_fast64_t> const& getInitialMemoryStates() const;

src/storm/storage/memorystructure/MemoryStructureBuilder.cpp

@@ -9,18 +9,13 @@
 namespace storm {
     namespace storage {
         
-        template <typename ValueType, typename RewardModelType>
-        MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(model.getInitialStates().getNumberOfSetBits(), 0), onlyInitialStatesRelevant(true) {
-            // Intentionally left empty
-        }
-
         template <typename ValueType, typename RewardModelType>
         MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> const& model, bool onlyInitialStatesRelevant) : model(model), transitions(numberOfMemoryStates, std::vector<boost::optional<storm::storage::BitVector>>(numberOfMemoryStates)), stateLabeling(numberOfMemoryStates), initialMemoryStates(onlyInitialStatesRelevant ? model.getInitialStates().getNumberOfSetBits() :  model.getNumberOfStates(), 0), onlyInitialStatesRelevant(onlyInitialStatesRelevant) {
             // Intentionally left empty
         }
         
         template <typename ValueType, typename RewardModelType>
-        MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(true) {
+        MemoryStructureBuilder<ValueType, RewardModelType>::MemoryStructureBuilder(MemoryStructure const& memoryStructure, storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), transitions(memoryStructure.getTransitionMatrix()), stateLabeling(memoryStructure.getStateLabeling()), initialMemoryStates(memoryStructure.getInitialMemoryStates()), onlyInitialStatesRelevant(memoryStructure.isOnlyInitialStatesRelevantSet()) {
             // Intentionally left empty
         }
 

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<ValueType, RewardModelType> 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<ValueType, RewardModelType> const& model, bool onlyInitialStatesRelevant);
+            MemoryStructureBuilder(uint_fast64_t numberOfMemoryStates, storm::models::sparse::Model<ValueType, RewardModelType> 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<ValueType, RewardModelType> 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);

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;