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 SparseMultiObjectivePreprocessor::PreprocessorData::PreprocessorData(SparseModelType const& model) : originalModel(model) { - storm::storage::MemoryStructureBuilder memoryBuilder(1, model); - memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); - memory = std::make_shared(memoryBuilder.build()); + memory = std::make_shared(storm::storage::MemoryStructureBuilder::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 + MemoryStructure MemoryStructureBuilder::buildTrivialMemoryStructure(storm::models::sparse::Model const& model) { + MemoryStructureBuilder memoryBuilder(1, model); + memoryBuilder.setTransition(0,0, storm::storage::BitVector(model.getNumberOfStates(), true)); + return memoryBuilder.build(); + } + template class MemoryStructureBuilder; template class MemoryStructureBuilder; template class MemoryStructureBuilder; 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 const& model); + private: storm::models::sparse::Model const& model;