diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp
index 25fa036af..747679385 100644
--- a/src/storm/storage/jani/Assignment.cpp
+++ b/src/storm/storage/jani/Assignment.cpp
@@ -37,7 +37,7 @@ namespace storm  {
         }
         
         void Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
-            this->setAssignedExpression(this->getAssignedExpression().substitute(substitution));
+            this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify());
         }
         
         int64_t Assignment::getLevel() const {
diff --git a/src/storm/storage/jani/Assignment.h b/src/storm/storage/jani/Assignment.h
index a4e2dbd23..3ab3b5581 100644
--- a/src/storm/storage/jani/Assignment.h
+++ b/src/storm/storage/jani/Assignment.h
@@ -14,7 +14,8 @@ namespace storm {
              * Creates an assignment of the given expression to the given variable.
              */
             Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t index = 0);
-            
+
+            Assignment(Assignment const&) = default;
             bool operator==(Assignment const& other) const;
             
             /*!
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index f4c65c759..da0d0a91c 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -53,6 +53,10 @@ namespace storm {
             return variables.addVariable(variable);
         }
 
+        bool Automaton::hasVariable(std::string const& name) const {
+            return variables.hasVariable(name);
+        }
+
         VariableSet& Automaton::getVariables() {
             return variables;
         }
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index c549ecca8..986ea794d 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -79,6 +79,8 @@ namespace storm {
              * Retrieves the variables of this automaton.
              */
             VariableSet const& getVariables() const;
+
+            bool hasVariable(std::string const& name) const;
             
             /*!
              * Retrieves all expression variables used by this automaton.
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 0c0c212a0..435da6818 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -35,6 +35,7 @@ namespace storm {
 
 
         modernjson::json buildExpression(storm::expressions::Expression const& exp,  std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) {
+            STORM_LOG_TRACE("Exporting " << exp);
             return ExpressionToJson::translate(exp,  constants, globalVariables, localVariables);
         }
 
diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp
index b957d5e9a..5ab431734 100644
--- a/src/storm/storage/jani/Location.cpp
+++ b/src/storm/storage/jani/Location.cpp
@@ -10,6 +10,10 @@ namespace storm {
         Location::Location(std::string const& name, std::vector<Assignment> const& transientAssignments) : name(name), assignments(transientAssignments) {
             // Intentionally left empty.
         }
+
+        Location::Location(std::string const& name, OrderedAssignments const& assignments) : name(name), assignments(assignments) {
+            // Intentionally left empty.
+        }
         
         std::string const& Location::getName() const {
             return name;
diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h
index b2bda7b23..75e53d575 100644
--- a/src/storm/storage/jani/Location.h
+++ b/src/storm/storage/jani/Location.h
@@ -18,7 +18,8 @@ namespace storm {
              * Creates a new location.
              */
             Location(std::string const& name, std::vector<Assignment> const& transientAssignments = {});
-            
+
+            Location(std::string const& name, OrderedAssignments const& assignments);
             /*!
              * Retrieves the name of the location.
              */
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 47533126c..2d51910cc 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -711,7 +711,15 @@ namespace storm {
         std::vector<Automaton> const& Model::getAutomata() const {
             return automata;
         }
-        
+
+        bool Model::hasAutomaton(std::string const& name) const {
+            return automatonToIndex.find(name) != automatonToIndex.end();
+        }
+
+        void Model::replaceAutomaton(uint64_t index, Automaton const& automaton) {
+            automata[index] = automaton;
+        }
+
         Automaton& Model::getAutomaton(std::string const& name) {
             auto it = automatonToIndex.find(name);
             STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'.");
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 2dc69d147..86555a2d4 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -245,6 +245,19 @@ namespace storm {
              */
             std::vector<Automaton> const& getAutomata() const;
 
+            /**
+             * Replaces the automaton at index with a new automaton.
+             * @param index
+             * @param newAutomaton
+             */
+            void replaceAutomaton(uint64_t index, Automaton const& newAutomaton);
+
+            /*!
+             * Rerieves whether there exists an automaton with the given name.
+             * @param name
+             * @return
+             */
+            bool hasAutomaton(std::string const& name) const;
             /*!
              * Retrieves the automaton with the given name.
              */
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 99eb415a8..68ae7f7c7 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -16,6 +16,14 @@ namespace storm {
         OrderedAssignments::OrderedAssignments(Assignment const& assignment) {
             add(assignment);
         }
+
+        OrderedAssignments OrderedAssignments::clone() const {
+            OrderedAssignments result;
+            for (auto const& assignment : allAssignments) {
+                result.add(Assignment(*assignment));
+            }
+            return result;
+        }
         
         bool OrderedAssignments::add(Assignment const& assignment) {
             // If the element is contained in this set of assignment, nothing needs to be added.
diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h
index 8e307e6e0..9d5a6a7b5 100644
--- a/src/storm/storage/jani/OrderedAssignments.h
+++ b/src/storm/storage/jani/OrderedAssignments.h
@@ -140,7 +140,9 @@ namespace storm {
             bool areLinear() const;
             
             friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
-            
+
+            OrderedAssignments clone() const;
+
         private:
             uint64_t isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const;
             uint64_t isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const;