From 1e4b81812cc40aedd022a2ce5a37afbb3af8dc07 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 29 May 2018 16:47:39 +0200
Subject: [PATCH] Environment does no longer require that unused setting
 modules still have to be registered.

---
 src/storm/environment/SubEnvironment.cpp | 19 ++++++++++++++++---
 src/storm/environment/SubEnvironment.h   |  4 ++--
 2 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp
index 920a06049..5226fdca4 100644
--- a/src/storm/environment/SubEnvironment.cpp
+++ b/src/storm/environment/SubEnvironment.cpp
@@ -16,31 +16,44 @@
 namespace storm {
     
     template<typename EnvironmentType>
-    SubEnvironment<EnvironmentType>::SubEnvironment() : subEnv(std::make_unique<EnvironmentType>()) {
+    SubEnvironment<EnvironmentType>::SubEnvironment() : subEnv(nullptr) {
         // Intentionally left empty
     }
     
     template<typename EnvironmentType>
-    SubEnvironment<EnvironmentType>::SubEnvironment(SubEnvironment const& other) : subEnv(new EnvironmentType(*other.subEnv)) {
+    SubEnvironment<EnvironmentType>::SubEnvironment(SubEnvironment const& other) : subEnv(other.subEnv ? new EnvironmentType(*other.subEnv) : nullptr) {
         // Intentionally left empty
     }
     
     template<typename EnvironmentType>
     SubEnvironment<EnvironmentType>& SubEnvironment<EnvironmentType>::operator=(SubEnvironment const& other) {
-        subEnv = std::make_unique<EnvironmentType>(*other.subEnv);
+        if (other.subEnv) {
+            subEnv = std::make_unique<EnvironmentType>(*other.subEnv);
+        } else {
+            subEnv.reset();
+        }
         return *this;
     }
     
     template<typename EnvironmentType>
     EnvironmentType const& SubEnvironment<EnvironmentType>::get() const {
+        assertInitialized();
         return *subEnv;
     }
     
     template<typename EnvironmentType>
     EnvironmentType& SubEnvironment<EnvironmentType>::get() {
+        assertInitialized();
         return *subEnv;
     }
     
+    template<typename EnvironmentType>
+    void SubEnvironment<EnvironmentType>::assertInitialized() const {
+        if (!subEnv) {
+            subEnv = std::make_unique<EnvironmentType>();
+        }
+    }
+    
     template class SubEnvironment<InternalEnvironment>;
     
     template class SubEnvironment<MultiObjectiveModelCheckerEnvironment>;
diff --git a/src/storm/environment/SubEnvironment.h b/src/storm/environment/SubEnvironment.h
index 2b6ecbf87..b1858936d 100644
--- a/src/storm/environment/SubEnvironment.h
+++ b/src/storm/environment/SubEnvironment.h
@@ -16,8 +16,8 @@ namespace storm {
         EnvironmentType& get();
     
     private:
-        std::unique_ptr<EnvironmentType> subEnv;
+        void assertInitialized() const;
+        mutable std::unique_ptr<EnvironmentType> subEnv;
         
     };
 }
-