From 4251c9f5252508e9ed8fa4a4907ff263dcad74e4 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 18 Jul 2017 10:56:28 +0200
Subject: [PATCH] added function to build a trivial memory structure

---
 .../multiobjective/SparseMultiObjectivePreprocessor.cpp    | 4 +---
 .../storage/memorystructure/MemoryStructureBuilder.cpp     | 7 +++++++
 src/storm/storage/memorystructure/MemoryStructureBuilder.h | 5 +++++
 3 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
index 0596303c8..09f0fdc6a 100644
--- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
+++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
@@ -69,9 +69,7 @@ namespace storm {
             
             template <typename SparseModelType>
             SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) {
-                storm::storage::MemoryStructureBuilder<ValueType, RewardModelType> memoryBuilder(1, model);
-                memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true));
-                memory = std::make_shared<storm::storage::MemoryStructure>(memoryBuilder.build());
+                memory = std::make_shared<storm::storage::MemoryStructure>(storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(model));
                 
                 // The memoryLabelPrefix should not be a prefix of a state label of the given model to ensure uniqueness of label names
                 memoryLabelPrefix = "mem";
diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
index 9ee23eaa6..696e9662a 100644
--- a/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
+++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.cpp
@@ -83,6 +83,13 @@ namespace storm {
             return MemoryStructure(std::move(transitions), std::move(stateLabeling), std::move(initialMemoryStates));
         }
         
+        template <typename ValueType, typename RewardModelType>
+        MemoryStructure MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(storm::models::sparse::Model<ValueType, RewardModelType> const& model) {
+            MemoryStructureBuilder<ValueType, RewardModelType> memoryBuilder(1, model);
+            memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true));
+            return memoryBuilder.build();
+        }
+
         template class MemoryStructureBuilder<double>;
         template class MemoryStructureBuilder<storm::RationalNumber>;
         template class MemoryStructureBuilder<storm::RationalFunction>;
diff --git a/src/storm/storage/memorystructure/MemoryStructureBuilder.h b/src/storm/storage/memorystructure/MemoryStructureBuilder.h
index 9fbe65c78..1cb51f384 100644
--- a/src/storm/storage/memorystructure/MemoryStructureBuilder.h
+++ b/src/storm/storage/memorystructure/MemoryStructureBuilder.h
@@ -57,6 +57,11 @@ namespace storm {
              */
             MemoryStructure build();
             
+            /*!
+             * Builds a trivial memory structure for the given model (consisting of a single memory state)
+             */
+            static MemoryStructure buildTrivialMemoryStructure(storm::models::sparse::Model<ValueType, RewardModelType> const& model);
+            
 
         private:
             storm::models::sparse::Model<ValueType, RewardModelType> const& model;