diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 869b17c2e..91b4ee670 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -56,7 +56,8 @@ namespace storm {
                 storm::jani::Model const& originalModel = model.asJaniModel();
                 STORM_LOG_THROW(originalModel.getModelType() == storm::jani::ModelType::DTMC || originalModel.getModelType() == storm::jani::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
                 
-                preprocessedModel = model;
+                // Flatten the parallel composition.
+                preprocessedModel = model.flattenComposition();
             }
             
             bool reuseAll = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseAllResultsSet();
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index e2fd73153..2f4873e8d 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -59,7 +59,7 @@ namespace storm {
             return name;
         }
 
-        Variable const& Automaton::addVariable(Variable const &variable) {
+        Variable& Automaton::addVariable(Variable const &variable) {
             if (variable.isBooleanVariable()) {
                 return addVariable(variable.asBooleanVariable());
             } else if (variable.isBoundedIntegerVariable()) {
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index c06a4b232..9337cf09e 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -103,7 +103,7 @@ namespace storm {
             /*!
              * Adds the given variable to this automaton
              */
-            Variable const& addVariable(Variable const& variable);
+            Variable& addVariable(Variable const& variable);
 
             /*!
              * Adds the given Boolean variable to this automaton.
diff --git a/src/storm/storage/jani/BooleanVariable.cpp b/src/storm/storage/jani/BooleanVariable.cpp
index bc7c14e54..72b3567c7 100644
--- a/src/storm/storage/jani/BooleanVariable.cpp
+++ b/src/storm/storage/jani/BooleanVariable.cpp
@@ -11,6 +11,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        std::unique_ptr<Variable> BooleanVariable::clone() const {
+            return std::make_unique<BooleanVariable>(*this);
+        }
+        
         bool BooleanVariable::isBooleanVariable() const {
             return true;
         }
diff --git a/src/storm/storage/jani/BooleanVariable.h b/src/storm/storage/jani/BooleanVariable.h
index 0b34fa55c..d3b2d15c5 100644
--- a/src/storm/storage/jani/BooleanVariable.h
+++ b/src/storm/storage/jani/BooleanVariable.h
@@ -18,6 +18,8 @@ namespace storm {
              */
             BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue, bool transient=false);
             
+            virtual std::unique_ptr<Variable> clone() const override;
+            
             virtual bool isBooleanVariable() const override;
         };
         
diff --git a/src/storm/storage/jani/BoundedIntegerVariable.cpp b/src/storm/storage/jani/BoundedIntegerVariable.cpp
index 7e5fee121..49eee83c7 100644
--- a/src/storm/storage/jani/BoundedIntegerVariable.cpp
+++ b/src/storm/storage/jani/BoundedIntegerVariable.cpp
@@ -13,10 +13,14 @@ namespace storm {
             // Intentionally left empty.
         }
  
-       BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) {
+        BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) {
             // Intentionally left empty.
         }
 
+        std::unique_ptr<Variable> BoundedIntegerVariable::clone() const {
+            return std::make_unique<Variable>(*this);
+        }
+        
         storm::expressions::Expression const& BoundedIntegerVariable::getLowerBound() const {
             return lowerBound;
         }
diff --git a/src/storm/storage/jani/BoundedIntegerVariable.h b/src/storm/storage/jani/BoundedIntegerVariable.h
index 98d240960..1f201ba2e 100644
--- a/src/storm/storage/jani/BoundedIntegerVariable.h
+++ b/src/storm/storage/jani/BoundedIntegerVariable.h
@@ -21,6 +21,8 @@ namespace storm {
              */
             BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound);
 
+            virtual std::unique_ptr<Variable> clone() const override;
+            
             /*!
              * Retrieves the expression defining the lower bound of the variable.
              */
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 8b46c06c8..816cb48e4 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -11,6 +11,8 @@
 #include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/InvalidTypeException.h"
 
+#include "storm/solver/SmtSolver.h"
+
 namespace storm {
     namespace jani {
         
@@ -53,6 +55,266 @@ namespace storm {
             return name;
         }
         
+        void Model::flattenSynchronizationVector(Automaton& newAutomaton, std::unordered_map<std::vector<uint64_t>, uint64_t>& newLocations, std::unordered_map<std::string, uint64_t>& newActionToIndex, std::vector<std::set<uint64_t>>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector<std::reference_wrapper<Automaton const>> const& composedAutomata, storm::solver::SmtSolver& solver) {
+
+            // Gather all participating automata and the corresponding input symbols.
+            std::vector<std::pair<std::reference_wrapper<Automaton const>, uint64_t>> participatingAutomataAndActions;
+            for (uint64_t i = 0; i < composedAutomata.size(); ++i) {
+                std::string const& actionName = vector.getInput(i);
+                if (!SynchronizationVector::isNoActionInput(actionName)) {
+                    uint64_t actionIndex = getActionIndex(actionName);
+                    participatingAutomataAndActions.push_back(std::make_pair(composedAutomata[i], actionIndex));
+                    synchronizingActionIndices[i].insert(actionIndex);
+                }
+            }
+
+        }
+        
+        Model Model::flattenComposition(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) const {
+            // If there is only one automaton and then system composition is the standard one, we don't need to modify
+            // the model.
+            if (this->getNumberOfAutomata() == 1 && this->hasStandardComposition()) {
+                return *this;
+            }
+
+            // Check for current restrictions of flatting process.
+            STORM_LOG_THROW(this->hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Flatting composition is only supported for standard-compliant compositions.");
+            STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException, "Unable to flatten modules for model of type '" << this->getModelType() << "'.");
+            
+            // Otherwise, we need to actually flatten composition.
+            
+            // Get an SMT solver for computing possible guard combinations.
+            std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*expressionManager);
+            
+            Composition const& systemComposition = getSystemComposition();
+            if (systemComposition.isAutomatonComposition()) {
+                AutomatonComposition const& automatonComposition = systemComposition.asAutomatonComposition();
+                STORM_LOG_THROW(automatonComposition.getInputEnabledActions().empty(), storm::exceptions::WrongFormatException, "Flatting does not support input-enabling actions.");
+                return createModelFromAutomaton(getAutomaton(automatonComposition.getAutomatonName()));
+            }
+
+            // Ensure that we have a parallel composition from now on.
+            STORM_LOG_THROW(systemComposition.isParallelComposition(), storm::exceptions::WrongFormatException, "Unknown system composition cannot be flattened.");
+            ParallelComposition const& parallelComposition = systemComposition.asParallelComposition();
+            
+            Automaton newAutomaton(this->getName() + "_flattening");
+            for (auto const & variable : getGlobalVariables()) {
+                std::unique_ptr<Variable> renamedVariable = variable.clone();
+                renamedVariable->setName("global_" + renamedVariable->getName());
+                newAutomaton.addVariable(*renamedVariable);
+            }
+            
+            std::vector<std::reference_wrapper<Automaton const>> composedAutomata;
+            for (auto const& element : parallelComposition.getSubcompositions()) {
+                STORM_LOG_THROW(element->isAutomatonComposition(), storm::exceptions::WrongFormatException, "Cannot flatten recursive (not standard-compliant) composition.");
+                AutomatonComposition const& automatonComposition = element->asAutomatonComposition();
+                STORM_LOG_THROW(automatonComposition.getInputEnabledActions().empty(), storm::exceptions::WrongFormatException, "Flatting does not support input-enabling actions.");
+                Automaton const& oldAutomaton = this->getAutomaton(automatonComposition.getAutomatonName());
+                composedAutomata.push_back(oldAutomaton);
+                
+                // Prefix all variables of this automaton with the automaton's name and add the to the resulting automaton.
+                for (auto const& variable : oldAutomaton.getVariables()) {
+                    std::unique_ptr<Variable> renamedVariable = variable.clone();
+                    renamedVariable->setName(oldAutomaton.getName() + "_" + renamedVariable->getName());
+                    newAutomaton.addVariable(*renamedVariable);
+                }
+            }
+            
+            // Prepare the solver.
+            // Assert the values of the constants.
+            for (auto const& constant : this->getConstants()) {
+                if (constant.isDefined()) {
+                    solver->add(constant.getExpressionVariable() == constant.getExpression());
+                }
+            }
+            // Assert the bounds of the global variables.
+            for (auto const& variable : newAutomaton.getVariables().getBoundedIntegerVariables()) {
+                solver->add(variable.getExpressionVariable() >= variable.getLowerBound());
+                solver->add(variable.getExpressionVariable() <= variable.getUpperBound());
+            }
+
+            // Since we need to reduce a tuple of locations to a single location, we keep a hashmap for this.
+            std::unordered_map<std::vector<uint64_t>, uint64_t> newLocations;
+            std::unordered_map<std::string, uint64_t> newActionToIndex;
+            
+            // Perform all necessary synchronizations and keep track which action indices participate in synchronization.
+            std::vector<std::set<uint64_t>> synchronizingActionIndices;
+            for (auto const& vector : parallelComposition.getSynchronizationVectors()) {
+                // If less then 2 automata participate, there is no need to perform a synchronization.
+                if (vector.getNumberOfActionInputs() <= 1) {
+                    continue;
+                }
+                
+                flattenSynchronizationVector(newAutomaton, newLocations, newActionToIndex, synchronizingActionIndices, vector, composedAutomata, *solver);
+            }
+            
+            // Now add all edges with action indices that were not mentioned in synchronization vectors.
+            for (uint64_t i = 0; i < composedAutomata.size(); ++i) {
+                Automaton const& automaton = composedAutomata[i].get();
+                for (auto const& edge : automaton.getEdges()) {
+                    if (synchronizingActionIndices[i].find(edge.getActionIndex()) == synchronizingActionIndices[i].end()) {
+                        // TODO: create template edge and create all concrete edges.
+                    }
+                }
+            }
+            
+
+            
+//            
+//            
+//            
+//            // Now go through the modules, gather the variables, construct the name of the new module and assert the
+//            // bounds of the discovered variables.
+//            for (auto const& module : this->getModules()) {
+//                newModuleName << module.getName() << "_";
+//                allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
+//                allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
+//                
+//                // The commands without a synchronizing action name, can simply be copied (plus adjusting the global
+//                // indices of the command and its updates).
+//                for (auto const& command : module.getCommands()) {
+//                    if (!command.isLabeled()) {
+//                        std::vector<storm::prism::Update> updates;
+//                        updates.reserve(command.getUpdates().size());
+//                        
+//                        for (auto const& update : command.getUpdates()) {
+//                            updates.push_back(storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
+//                            ++nextUpdateIndex;
+//                        }
+//                        
+//                        newCommands.push_back(storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find("")->second, "", command.getGuardExpression(), updates, command.getFilename(), 0));
+//                        ++nextCommandIndex;
+//                    }
+//                }
+//            }
+//            
+//            // Save state of solver so that we can always restore the point where we have exactly the constant values
+//            // and variables bounds on the assertion stack.
+//            solver->push();
+//            
+//            // Now we need to enumerate all possible combinations of synchronizing commands. For this, we iterate over
+//            // all actions and let the solver enumerate the possible combinations of commands that can be enabled together.
+//            for (auto const& actionIndex : this->getSynchronizingActionIndices()) {
+//                bool noCombinationsForAction = false;
+//                
+//                // Prepare the list that stores for each module the list of commands with the given action.
+//                std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
+//                
+//                for (auto const& module : this->getModules()) {
+//                    // If the module has no command with this action, we can skip it.
+//                    if (!module.hasActionIndex(actionIndex)) {
+//                        continue;
+//                    }
+//                    
+//                    std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex);
+//                    
+//                    // If there is no command even though the module has this action, there is no valid command
+//                    // combination with this action.
+//                    if (commandIndices.empty()) {
+//                        noCombinationsForAction = true;
+//                        break;
+//                    }
+//                    
+//                    // Prepare empty list of commands for this module.
+//                    possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
+//                    
+//                    // Add references to the commands labeled with the current action.
+//                    for (auto const& commandIndex : commandIndices) {
+//                        possibleCommands.back().push_back(module.getCommand(commandIndex));
+//                    }
+//                }
+//                
+//                // If there are no valid combinations for the action, we need to skip the generation of synchronizing
+//                // commands.
+//                if (!noCombinationsForAction) {
+//                    // Save the solver state to be able to restore it when this action index is done.
+//                    solver->push();
+//                    
+//                    // Start by creating a fresh auxiliary variable for each command and link it with the guard.
+//                    std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
+//                    std::vector<storm::expressions::Variable> allCommandVariables;
+//                    for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) {
+//                        // Create auxiliary variables and link them with the guards.
+//                        for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) {
+//                            commandVariables[outerIndex].push_back(manager->declareFreshBooleanVariable());
+//                            allCommandVariables.push_back(commandVariables[outerIndex].back());
+//                            solver->add(implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
+//                        }
+//                        
+//                        storm::expressions::Expression atLeastOneCommandFromModule = manager->boolean(false);
+//                        for (auto const& commandVariable : commandVariables[outerIndex]) {
+//                            atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
+//                        }
+//                        solver->add(atLeastOneCommandFromModule);
+//                    }
+//                    
+//                    // Now we are in a position to start the enumeration over all command variables. While doing so, we
+//                    // keep track of previously seen command combinations, because the AllSat procedures are not
+//                    // always guaranteed to only provide distinct models.
+//                    std::unordered_set<std::vector<uint_fast64_t>, storm::utility::vector::VectorHash<uint_fast64_t>> seenCommandCombinations;
+//                    solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool {
+//                        // Now we need to reconstruct the chosen commands from the valuation of the command variables.
+//                        std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
+//                        
+//                        for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
+//                            for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
+//                                if (modelReference.getBooleanValue(commandVariables[outerIndex][innerIndex])) {
+//                                    chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]);
+//                                }
+//                            }
+//                        }
+//                        
+//                        // Now that we have retrieved the commands, we need to build their synchronizations and add them
+//                        // to the flattened module.
+//                        std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
+//                        for (auto const& element : chosenCommands) {
+//                            iterators.push_back(element.begin());
+//                        }
+//                        
+//                        bool movedAtLeastOneIterator = false;
+//                        std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
+//                        std::vector<uint_fast64_t> commandCombinationIndices(iterators.size());
+//                        do {
+//                            for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
+//                                commandCombination[index] = *iterators[index];
+//                                commandCombinationIndices[index] = commandCombination[index].get().getGlobalIndex();
+//                            }
+//                            
+//                            // Only add the command combination if it was not previously seen.
+//                            auto seenIt = seenCommandCombinations.find(commandCombinationIndices);
+//                            if (seenIt == seenCommandCombinations.end()) {
+//                                newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second, commandCombination));
+//                                seenCommandCombinations.insert(commandCombinationIndices);
+//                                
+//                                // Move the counters appropriately.
+//                                ++nextCommandIndex;
+//                                nextUpdateIndex += newCommands.back().getNumberOfUpdates();
+//                            }
+//                            
+//                            movedAtLeastOneIterator = false;
+//                            for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
+//                                ++iterators[index];
+//                                if (iterators[index] != chosenCommands[index].cend()) {
+//                                    movedAtLeastOneIterator = true;
+//                                    break;
+//                                } else {
+//                                    iterators[index] = chosenCommands[index].cbegin();
+//                                }
+//                            }
+//                        } while (movedAtLeastOneIterator);
+//                        
+//                        return true;
+//                    });
+//                    
+//                    solver->pop();
+//                }
+//            }
+//            
+//            // Finally, we can create the module and the program and return it.
+//            storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
+//            return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), this->getFilename(), 0, true);
+        }
+        
         uint64_t Model::addAction(Action const& action) {
             auto it = actionToIndex.find(action.getName());
             STORM_LOG_THROW(it == actionToIndex.end(), storm::exceptions::WrongFormatException, "Action with name '" << action.getName() << "' already exists");
@@ -609,5 +871,18 @@ namespace storm {
             }
             return false;
         }
+        
+        Model Model::createModelFromAutomaton(Automaton const& automaton) const {
+            // Copy the full model
+            Model newModel(*this);
+            
+            // Replace the automata by the one single selected automaton.
+            newModel.automata = std::vector<Automaton>({automaton});
+            
+            // Set the standard composition for the new model to the default one.
+            newModel.setSystemComposition(newModel.getStandardSystemComposition());
+            
+            return newModel;
+        }
     }
 }
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 2fbe8e8b8..df370409e 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -8,6 +8,8 @@
 #include "storm/storage/jani/Constant.h"
 #include "storm/storage/jani/Composition.h"
 
+#include "storm/utility/solver.h"
+
 namespace storm {
     namespace expressions {
         class ExpressionManager;
@@ -16,6 +18,7 @@ namespace storm {
     namespace jani {
         
         class Exporter;
+        class SynchronizationVector;
         
         class Model {
         public:
@@ -51,6 +54,14 @@ namespace storm {
              */
             std::string const& getName() const;
             
+            /*!
+             * Flatten the composition to obtain an equivalent model that contains exactly one automaton that has the
+             * standard composition.
+             *
+             * @param smtSolverFactory A factory that can be used to create new SMT solvers.
+             */
+            Model flattenComposition(std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::SmtSolverFactory>()) const;
+            
             /**
              * Checks whether the model has an action with the given name.
              *
@@ -377,6 +388,16 @@ namespace storm {
             static const uint64_t SILENT_ACTION_INDEX;
             
         private:
+            /*!
+             * Creates a new model from the given automaton (which must be contained in the current model).
+             */
+            Model createModelFromAutomaton(Automaton const& automaton) const;
+            
+            /*!
+             * Flattens the actions of the automata into new edges in the provided automaton.
+             */
+            void flattenSynchronizationVector(Automaton& newAutomaton, std::unordered_map<std::vector<uint64_t>, uint64_t>& newLocations, std::unordered_map<std::string, uint64_t>& newActionToIndex, std::vector<std::set<uint64_t>>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector<std::reference_wrapper<Automaton const>> const& composedAutomata, storm::solver::SmtSolver& solver);
+            
             /// The model name.
             std::string name;
             
diff --git a/src/storm/storage/jani/RealVariable.cpp b/src/storm/storage/jani/RealVariable.cpp
index 88367f713..29543978b 100644
--- a/src/storm/storage/jani/RealVariable.cpp
+++ b/src/storm/storage/jani/RealVariable.cpp
@@ -11,6 +11,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        std::unique_ptr<Variable> RealVariable::clone() const {
+            return std::make_unique<RealVariable>(*this);
+        }
+        
         bool RealVariable::isRealVariable() const {
             return true;
         }
diff --git a/src/storm/storage/jani/RealVariable.h b/src/storm/storage/jani/RealVariable.h
index 8d966f356..f6513463d 100644
--- a/src/storm/storage/jani/RealVariable.h
+++ b/src/storm/storage/jani/RealVariable.h
@@ -17,6 +17,8 @@ namespace storm {
              */
             RealVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient=false);
             
+            virtual std::unique_ptr<Variable> clone() const override;
+            
             virtual bool isRealVariable() const override;
         };
 
diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp
new file mode 100644
index 000000000..fd88f83c3
--- /dev/null
+++ b/src/storm/storage/jani/TemplateEdge.cpp
@@ -0,0 +1,9 @@
+#include "storm/storage/jani/TemplateEdge.h"
+
+namespace storm {
+    namespace jani {
+        
+        
+        
+    }
+}
diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h
new file mode 100644
index 000000000..b03d9d043
--- /dev/null
+++ b/src/storm/storage/jani/TemplateEdge.h
@@ -0,0 +1,26 @@
+#pragma once
+
+#include <vector>
+
+#include "storm/storage/expressions/Expression.h"
+
+#include "storm/storage/jani/EdgeDestination.h"
+
+namespace storm {
+    namespace jani {
+        
+        class TemplateEdge {
+        public:
+            TemplateEdge() = default;
+            TemplateEdge(storm::expressions::Expression const& guard, std::vector<EdgeDestination> destinations = {});
+            
+        private:
+            // The guard of the template edge.
+            storm::expressions::Expression guard;
+            
+            // The destinations of the template edge.
+            std::vector<EdgeDestination> destinations;
+        };
+        
+    }
+}
diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.cpp b/src/storm/storage/jani/UnboundedIntegerVariable.cpp
index 8cc8ede9f..a57d3acde 100644
--- a/src/storm/storage/jani/UnboundedIntegerVariable.cpp
+++ b/src/storm/storage/jani/UnboundedIntegerVariable.cpp
@@ -11,6 +11,10 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        std::unique_ptr<Variable> UnboundedIntegerVariable::clone() const {
+            return std::make_unique<UnboundedIntegerVariable>(*this);
+        }
+        
         bool UnboundedIntegerVariable::isUnboundedIntegerVariable() const {
             return true;
         }
diff --git a/src/storm/storage/jani/UnboundedIntegerVariable.h b/src/storm/storage/jani/UnboundedIntegerVariable.h
index 16f54b723..fe0649ce5 100644
--- a/src/storm/storage/jani/UnboundedIntegerVariable.h
+++ b/src/storm/storage/jani/UnboundedIntegerVariable.h
@@ -16,6 +16,8 @@ namespace storm {
              */
             UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const&, bool transient=false);
             
+            virtual std::unique_ptr<Variable> clone() const override;
+            
             virtual bool isUnboundedIntegerVariable() const override;
         };
         
diff --git a/src/storm/storage/jani/Variable.cpp b/src/storm/storage/jani/Variable.cpp
index a30742b54..a4184b5a0 100644
--- a/src/storm/storage/jani/Variable.cpp
+++ b/src/storm/storage/jani/Variable.cpp
@@ -28,6 +28,10 @@ namespace storm {
             return name;
         }
         
+        void Variable::setName(std::string const& newName) {
+            name = newName;
+        }
+        
         bool Variable::isBooleanVariable() const {
             return false;
         }
diff --git a/src/storm/storage/jani/Variable.h b/src/storm/storage/jani/Variable.h
index 1d5425ac2..9e403828a 100644
--- a/src/storm/storage/jani/Variable.h
+++ b/src/storm/storage/jani/Variable.h
@@ -29,6 +29,11 @@ namespace storm {
             
             virtual ~Variable();
             
+            /*!
+             * Clones the variable.
+             */
+            virtual std::unique_ptr<Variable> clone() const = 0;
+            
             /*!
              * Retrieves the associated expression variable
              */
@@ -39,6 +44,11 @@ namespace storm {
              */
             std::string const& getName() const;
 
+            /*!
+             * Sets the name of the variable.
+             */
+            void setName(std::string const& newName);
+            
             /*!
              * Retrieves whether an initial expression is set.
              */
diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp
index c13555540..0fa697b9c 100644
--- a/src/storm/storage/jani/VariableSet.cpp
+++ b/src/storm/storage/jani/VariableSet.cpp
@@ -3,6 +3,7 @@
 #include "storm/utility/macros.h"
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/InvalidTypeException.h"
 
 namespace storm {
     namespace jani {
@@ -43,6 +44,19 @@ namespace storm {
             return detail::ConstVariables<RealVariable>(realVariables.begin(), realVariables.end());
         }
         
+        Variable const& VariableSet::addVariable(Variable const& variable) {
+            if (variable.isBooleanVariable()) {
+                return addVariable(variable.asBooleanVariable());
+            } else if (variable.isBoundedIntegerVariable()) {
+                return addVariable(variable.asBoundedIntegerVariable());
+            } else if (variable.isUnboundedIntegerVariable()) {
+                return addVariable(variable.asUnboundedIntegerVariable());
+            } else if (variable.isRealVariable()) {
+                return addVariable(variable.asRealVariable());
+            }
+            STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type.");
+        }
+        
         BooleanVariable const& VariableSet::addVariable(BooleanVariable const& variable) {
             STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
             std::shared_ptr<BooleanVariable> newVariable = std::make_shared<BooleanVariable>(variable);
diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h
index c02c018ef..1da930022 100644
--- a/src/storm/storage/jani/VariableSet.h
+++ b/src/storm/storage/jani/VariableSet.h
@@ -67,7 +67,12 @@ namespace storm {
              * Retrieves the real variables in this set.
              */
             detail::ConstVariables<RealVariable> getRealVariables() const;
-            
+
+            /*!
+             * Adds the given variable to this set.
+             */
+            Variable const& addVariable(Variable const& variable);
+
             /*!
              * Adds the given boolean variable to this set.
              */