diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
index f1450d004..8ad36776b 100644
--- a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
@@ -9,7 +9,7 @@ namespace storm {
             res.hasLocationAssignment = false;
             res.hasEdgeAssignment = false;
             res.hasEdgeDestinationAssignment = false;
-            JaniTraverser::traverse(model, std::make_pair(&variable, &res));
+            ConstJaniTraverser::traverse(model, std::make_pair(&variable, &res));
             return res;
         }
         
@@ -20,7 +20,7 @@ namespace storm {
                     resVar.second->hasLocationAssignment = true;
                 }
             }
-            JaniTraverser::traverse(location, data);
+            ConstJaniTraverser::traverse(location, data);
         }
         
         void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
@@ -30,7 +30,7 @@ namespace storm {
                     resVar.second->hasEdgeAssignment = true;
                 }
             }
-            JaniTraverser::traverse(templateEdge, data);
+            ConstJaniTraverser::traverse(templateEdge, data);
         }
         
         void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
@@ -40,7 +40,7 @@ namespace storm {
                     resVar.second->hasEdgeDestinationAssignment = true;
                 }
             }
-            JaniTraverser::traverse(templateEdgeDestination, data);
+            ConstJaniTraverser::traverse(templateEdgeDestination, data);
         }
     }
 }
diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.h b/src/storm/storage/jani/traverser/AssignmentsFinder.h
index 2a2d2cdd0..b6bcd376e 100644
--- a/src/storm/storage/jani/traverser/AssignmentsFinder.h
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.h
@@ -7,7 +7,7 @@
 
 namespace storm {
     namespace jani {
-        class AssignmentsFinder : public JaniTraverser {
+        class AssignmentsFinder : public ConstJaniTraverser {
         public:
             
             struct ResultType {
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp
index eb60a9358..bd1b9bbf1 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.cpp
+++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp
@@ -3,7 +3,159 @@
 
 namespace storm {
     namespace jani {
-        void JaniTraverser::traverse(Model const& model, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(Model& model, boost::any const& data) const {
+            for (auto& act : model.getActions()) {
+                traverse(act, data);
+            }
+            for (auto& c : model.getConstants()) {
+                traverse(c, data);
+            }
+            traverse(model.getGlobalVariables(), data);
+            for (auto& aut : model.getAutomata()) {
+                traverse(aut, data);
+            }
+            if (model.hasInitialStatesRestriction()) {
+                traverse(model.getInitialStatesRestriction(), data);
+            }
+        }
+        
+        void JaniTraverser::traverse(Action const& action, boost::any const& data) const {
+            // Intentionally left empty.
+        }
+            
+        void JaniTraverser::traverse(Automaton& automaton, boost::any const& data) const {
+            traverse(automaton.getVariables(), data);
+            for (auto& loc : automaton.getLocations()) {
+                traverse(loc, data);
+            }
+            traverse(automaton.getEdgeContainer(), data);
+            if (automaton.hasInitialStatesRestriction()) {
+                traverse(automaton.getInitialStatesRestriction(), data);
+            }
+        }
+            
+        void JaniTraverser::traverse(Constant& constant, boost::any const& data) const {
+            if (constant.isDefined()) {
+                traverse(constant.getExpression(), data);
+            }
+        }
+            
+        void JaniTraverser::traverse(VariableSet& variableSet, boost::any const& data) const {
+            for (auto& v : variableSet.getBooleanVariables()) {
+                traverse(v, data);
+            }
+            for (auto& v : variableSet.getBoundedIntegerVariables()) {
+                traverse(v, data);
+            }
+            for (auto& v : variableSet.getUnboundedIntegerVariables()) {
+                traverse(v, data);
+            }
+            for (auto& v : variableSet.getRealVariables()) {
+                traverse(v, data);
+            }
+            for (auto& v : variableSet.getArrayVariables()) {
+                traverse(v, data);
+            }
+        }
+            
+        void JaniTraverser::traverse(Location& location, boost::any const& data) const {
+            traverse(location.getAssignments(), data);
+        }
+            
+        void JaniTraverser::traverse(BooleanVariable& variable, boost::any const& data) const {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+        }
+        
+        void JaniTraverser::traverse(BoundedIntegerVariable& variable, boost::any const& data) const {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+            traverse(variable.getLowerBound(), data);
+            traverse(variable.getUpperBound(), data);
+        }
+        
+        void JaniTraverser::traverse(UnboundedIntegerVariable& variable, boost::any const& data) const {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+        }
+        
+        void JaniTraverser::traverse(RealVariable& variable, boost::any const& data) const {
+             if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+        }
+        
+        void JaniTraverser::traverse(ArrayVariable& variable, boost::any const& data) const {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+            if (variable.hasElementTypeBounds()) {
+                traverse(variable.getElementTypeBounds().first, data);
+                traverse(variable.getElementTypeBounds().second, data);
+            }
+        }
+        
+        void JaniTraverser::traverse(EdgeContainer& edgeContainer, boost::any const& data) const {
+            for (auto& templateEdge : edgeContainer.getTemplateEdges()) {
+                traverse(*templateEdge, data);
+            }
+            for (auto& concreteEdge : edgeContainer.getConcreteEdges()) {
+                traverse(concreteEdge, data);
+            }
+        }
+        
+        void JaniTraverser::traverse(TemplateEdge& templateEdge, boost::any const& data) const {
+            traverse(templateEdge.getGuard(), data);
+            for (auto& dest : templateEdge.getDestinations()) {
+                traverse(dest, data);
+            }
+            traverse(templateEdge.getAssignments(), data);
+        }
+            
+        void JaniTraverser::traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) const {
+            traverse(templateEdgeDestination.getOrderedAssignments(), data);
+        }
+            
+        void JaniTraverser::traverse(Edge& edge, boost::any const& data) const {
+            if (edge.hasRate()) {
+                traverse(edge.getRate(), data);
+            }
+            for (auto& dest : edge.getDestinations()) {
+                traverse(dest, data);
+            }
+        }
+            
+        void JaniTraverser::traverse(EdgeDestination& edgeDestination, boost::any const& data) const {
+            traverse(edgeDestination.getProbability(), data);
+        }
+            
+        void JaniTraverser::traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const {
+            for (auto& assignment : orderedAssignments) {
+                traverse(assignment, data);
+            }
+            STORM_LOG_ASSERT(orderedAssignments.checkOrder(), "Order of ordered assignment has been violated.");
+        }
+            
+        void JaniTraverser::traverse(Assignment& assignment, boost::any const& data) const {
+            traverse(assignment.getAssignedExpression(), data);
+            traverse(assignment.getLValue(), data);
+        }
+        
+        void JaniTraverser::traverse(LValue& lValue, boost::any const& data) const {
+            if (lValue.isArrayAccess()) {
+                traverse(lValue.getArrayIndex(), data);
+            }
+        }
+        
+        void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
+            // intentionally left empty.
+        }
+        
+        void ConstJaniTraverser::traverse(Model const& model, boost::any const& data) const {
             for (auto const& act : model.getActions()) {
                 traverse(act, data);
             }
@@ -19,11 +171,11 @@ namespace storm {
             }
         }
         
-        void JaniTraverser::traverse(Action const& action, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Action const& action, boost::any const& data) const {
             // Intentionally left empty.
         }
             
-        void JaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const {
             traverse(automaton.getVariables(), data);
             for (auto const& loc : automaton.getLocations()) {
                 traverse(loc, data);
@@ -34,13 +186,13 @@ namespace storm {
             }
         }
             
-        void JaniTraverser::traverse(Constant const& constant, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Constant const& constant, boost::any const& data) const {
             if (constant.isDefined()) {
                 traverse(constant.getExpression(), data);
             }
         }
             
-        void JaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const {
             for (auto const& v : variableSet.getBooleanVariables()) {
                 traverse(v, data);
             }
@@ -53,19 +205,22 @@ namespace storm {
             for (auto const& v : variableSet.getRealVariables()) {
                 traverse(v, data);
             }
+            for (auto const& v : variableSet.getArrayVariables()) {
+                traverse(v, data);
+            }
         }
             
-        void JaniTraverser::traverse(Location const& location, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Location const& location, boost::any const& data) const {
             traverse(location.getAssignments(), data);
         }
             
-        void JaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
@@ -73,19 +228,29 @@ namespace storm {
             traverse(variable.getUpperBound(), data);
         }
         
-        void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void JaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const {
              if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(ArrayVariable const& variable, boost::any const& data) const {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+            if (variable.hasElementTypeBounds()) {
+                traverse(variable.getElementTypeBounds().first, data);
+                traverse(variable.getElementTypeBounds().second, data);
+            }
+        }
+        
+        void ConstJaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const {
             for (auto const& templateEdge : edgeContainer.getTemplateEdges()) {
                 traverse(*templateEdge, data);
             }
@@ -94,7 +259,7 @@ namespace storm {
             }
         }
         
-        void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
             traverse(templateEdge.getGuard(), data);
             for (auto const& dest : templateEdge.getDestinations()) {
                 traverse(dest, data);
@@ -102,11 +267,11 @@ namespace storm {
             traverse(templateEdge.getAssignments(), data);
         }
             
-        void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
             traverse(templateEdgeDestination.getOrderedAssignments(), data);
         }
             
-        void JaniTraverser::traverse(Edge const& edge, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Edge const& edge, boost::any const& data) const {
             if (edge.hasRate()) {
                 traverse(edge.getRate(), data);
             }
@@ -115,27 +280,28 @@ namespace storm {
             }
         }
             
-        void JaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const {
             traverse(edgeDestination.getProbability(), data);
         }
             
-        void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const {
             for (auto const& assignment : orderedAssignments) {
                 traverse(assignment, data);
             }
         }
             
-        void JaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const {
             traverse(assignment.getAssignedExpression(), data);
+            traverse(assignment.getLValue(), data);
         }
             
-        void JaniTraverser::traverse(LValue const& lValue, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(LValue const& lValue, boost::any const& data) const {
             if (lValue.isArrayAccess()) {
                 traverse(lValue.getArrayIndex(), data);
             }
         }
         
-        void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
             // intentionally left empty.
         }
         
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h
index 9cef29afc..25cc4530d 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.h
+++ b/src/storm/storage/jani/traverser/JaniTraverser.h
@@ -11,6 +11,33 @@ namespace storm {
         public:
             virtual ~JaniTraverser() = default;
             
+            virtual void traverse(Model& model, boost::any const& data) const;
+            
+            virtual void traverse(Action const& action, boost::any const& data) const;
+            virtual void traverse(Automaton& automaton, boost::any const& data) const;
+            virtual void traverse(Constant& constant, boost::any const& data) const;
+            virtual void traverse(VariableSet& variableSet, boost::any const& data) const;
+            virtual void traverse(Location& location, boost::any const& data) const;
+            virtual void traverse(BooleanVariable& variable, boost::any const& data) const;
+            virtual void traverse(BoundedIntegerVariable& variable, boost::any const& data) const;
+            virtual void traverse(UnboundedIntegerVariable& variable, boost::any const& data) const;
+            virtual void traverse(RealVariable& variable, boost::any const& data) const;
+            virtual void traverse(ArrayVariable& variable, boost::any const& data) const;
+            virtual void traverse(EdgeContainer& edgeContainer, boost::any const& data) const;
+            virtual void traverse(TemplateEdge& templateEdge, boost::any const& data) const;
+            virtual void traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) const;
+            virtual void traverse(Edge& edge, boost::any const& data) const;
+            virtual void traverse(EdgeDestination& edgeDestination, boost::any const& data) const;
+            virtual void traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const;
+            virtual void traverse(Assignment& assignment, boost::any const& data) const;
+            virtual void traverse(LValue& lValue, boost::any const& data) const;
+            virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const;
+        };
+        
+        class ConstJaniTraverser {
+        public:
+            virtual ~ConstJaniTraverser() = default;
+            
             virtual void traverse(Model const& model, boost::any const& data) const;
             
             virtual void traverse(Action const& action, boost::any const& data) const;
@@ -22,6 +49,7 @@ namespace storm {
             virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data) const;
             virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const;
             virtual void traverse(RealVariable const& variable, boost::any const& data) const;
+            virtual void traverse(ArrayVariable const& variable, boost::any const& data) const;
             virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data) const;
             virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const;
             virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const;