more work on JANI model generation

Former-commit-id: c5a5df87ee
9 years ago · 9c75e9dbd7
13 changed files with 846 additions and 565 deletions
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@ -6,6 +6,15 @@

 #include "src/logic/Formulas.h"

+#include "src/storage/jani/Model.h"
+#include "src/storage/jani/RenameComposition.h"
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
+
+#include "src/storage/dd/Add.h"
+#include "src/storage/dd/Bdd.h"
+#include "src/adapters/AddExpressionAdapter.h"
+
 #include "src/utility/macros.h"
 #include "src/utility/jani.h"
 #include "src/exceptions/InvalidArgumentException.h"
@ -119,34 +128,521 @@ namespace storm {
            this->model = this->model->substituteConstants();
        }
        
-        /*!
-         * This structure represents a subcomponent of a composition.
-         */
+        template <storm::dd::DdType Type, typename ValueType>
+        struct CompositionVariables {
+            CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()) {
+                // Intentionally left empty.
+            }
+            
+            std::shared_ptr<storm::dd::DdManager<Type>> manager;
+            
+            // The meta variables for the row encoding.
+            std::set<storm::expressions::Variable> rowMetaVariables;
+            std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
+            std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
+            
+            // The meta variables for the column encoding.
+            std::set<storm::expressions::Variable> columnMetaVariables;
+            std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
+            std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
+            
+            // All pairs of row/column meta variables.
+            std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
+
+            // A mapping from automata to the meta variable encoding their location.
+            std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
+            
+            // The meta variables used to encode the actions.
+            std::vector<storm::expressions::Variable> actionVariables;
+            
+            // The meta variables used to encode the remaining nondeterminism.
+            std::vector<storm::expressions::Variable> nondeterminismVariables;
+            
+            // DDs representing the identity for each variable.
+            std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap;
+            
+            // A set of all meta variables that correspond to global variables.
+            std::set<storm::expressions::Variable> allGlobalVariables;
+            
+            // DDs representing the identity for each automaton.
+            std::map<std::string, storm::dd::Add<Type, ValueType>> automatonToIdentityMap;
+            
+            // DDs representing the valid ranges of the variables of each automaton.
+            std::map<std::string, storm::dd::Add<Type, ValueType>> automatonToRangeMap;
+        };
+        
+        // A class responsible for creating the necessary variables for a subsequent composition of automata.
+        template <storm::dd::DdType Type, typename ValueType>
+        class CompositionVariableCreator : public storm::jani::CompositionVisitor {
+        public:
+            CompositionVariableCreator(storm::jani::Model const& model) : model(model) {
+                // Intentionally left empty.
+            }
+            
+            CompositionVariables<Type, ValueType> create() {
+                // First, check whether every automaton appears exactly once in the system composition.
+                automata.clear();
+                this->model.getSystemComposition().accept(*this, boost::none);
+                STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
+                
+                // Then, check that the model does not contain unbounded integer variables.
+                STORM_LOG_THROW(!this->model.getGlobalVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global unbounded integer variables.");
+                for (auto const& automaton : this->model.getAutomata()) {
+                    STORM_LOG_THROW(!automaton.getVariables().containsUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains unbounded integer variables in automaton '" << automaton.getName() << "'.");
+                }
+                
+                // Based on this assumption, we create the variables.
+                return createVariables();
+            }
+            
+            boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
+                auto it = automata.find(composition.getAutomatonName());
+                STORM_LOG_THROW(it != automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the same automaton multiple times.");
+                automata.insert(it, composition.getAutomatonName());
+                return boost::none;
+            }
+            
+            boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
+                composition.getSubcomposition().accept(*this, boost::none);
+                return boost::none;
+            }
+            
+            boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
+                composition.getLeftSubcomposition().accept(*this, boost::none);
+                composition.getRightSubcomposition().accept(*this, boost::none);
+                return boost::none;
+            }
+            
+        private:
+            CompositionVariables<Type, ValueType> createVariables() {
+                CompositionVariables<Type, ValueType> result;
+                
+                for (auto const& action : this->model.getActions()) {
+                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(action.getName());
+                    result.actionVariables.push_back(variablePair.first);
+                }
+                
+                // FIXME: check how many nondeterminism variables we should actually allocate.
+                uint64_t numberOfNondeterminismVariables = this->model.getNumberOfAutomata();
+                for (auto const& automaton : this->model.getAutomata()) {
+                    numberOfNondeterminismVariables *= automaton.getNumberOfEdges();
+                }
+                for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) {
+                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("nondet" + std::to_string(i));
+                    result.nondeterminismVariables.push_back(variablePair.first);
+                }
+                
+                // Create global variables.
+                for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) {
+                    createVariable(variable, result);
+                }
+                for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) {
+                    createVariable(variable, result);
+                }
+
+                // Create the variables for the individual automata.
+                for (auto const& automaton : this->model.getAutomata()) {
+                    storm::dd::Bdd<Type> identity = result.manager->getBddOne();
+                    storm::dd::Bdd<Type> range = result.manager->getBddOne();
+                    
+                    // Start by creating a meta variable for the location of the automaton.
+                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations());
+                    result.automatonToLocationVariableMap[automaton.getName()] = variablePair.first;
+                    storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
+                    identity &= variableIdentity.toBdd();
+                    range &= result.manager->getRange(variablePair.first);
+                    
+                    // Then create variables for the variables of the automaton.
+                    for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                        createVariable(variable, result);
+                        identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
+                        range &= result.manager->getRange(result.variableToRowMetaVariableMap.at(variable.getExpressionVariable()));
+                    }
+                    for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
+                        createVariable(variable, result);
+                        identity &= result.variableToIdentityMap.at(variable.getExpressionVariable()).toBdd();
+                        range &= result.manager->getRange(result.variableToRowMetaVariableMap.at(variable.getExpressionVariable()));
+                    }
+                    
+                    result.automatonToIdentityMap[automaton.getName()] = identity.template toAdd<ValueType>();
+                    result.automatonToRangeMap[automaton.getName()] = range.template toAdd<ValueType>();
+                }
+                
+                return result;
+            }
+            
+            void createVariable(storm::jani::BoundedIntegerVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+                int_fast64_t low = variable.getLowerBound().evaluateAsInt();
+                int_fast64_t high = variable.getUpperBound().evaluateAsInt();
+                std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName(), low, high);
+                
+                STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "] and " << variablePair.second.getName() << ".");
+                
+                result.rowMetaVariables.insert(variablePair.first);
+                result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first);
+                
+                result.columnMetaVariables.insert(variablePair.second);
+                result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second);
+                
+                storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * result.manager->getRange(variablePair.first).template toAdd<ValueType>() * result.manager->getRange(variablePair.second).template toAdd<ValueType>();
+                result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+                result.rowColumnMetaVariablePairs.push_back(variablePair);
+                
+                result.allGlobalVariables.insert(variable.getExpressionVariable());
+            }
+            
+            void createVariable(storm::jani::BooleanVariable const& variable, CompositionVariables<Type, ValueType>& result) {
+                std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName());
+                
+                STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
+                
+                result.rowMetaVariables.insert(variablePair.first);
+                result.variableToRowMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.first);
+                
+                result.columnMetaVariables.insert(variablePair.second);
+                result.variableToColumnMetaVariableMap.emplace(variable.getExpressionVariable(), variablePair.second);
+                
+                storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(variablePair.first).equals(result.manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
+                result.variableToIdentityMap.emplace(variable.getExpressionVariable(), variableIdentity);
+                
+                result.rowColumnMetaVariablePairs.push_back(variablePair);
+                result.allGlobalVariables.insert(variable.getExpressionVariable());
+            }
+            
+            storm::jani::Model const& model;
+            std::set<std::string> automata;
+        };
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        struct EdgeDestinationDd {
+            EdgeDestinationDd(storm::dd::Add<Type, ValueType> const& transitionsDd, std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}) : transitionsDd(transitionsDd), writtenGlobalVariables(writtenGlobalVariables) {
+                // Intentionally left empty.
+            }
+            
+            storm::dd::Add<Type, ValueType> transitionsDd;
+            std::set<storm::expressions::Variable> writtenGlobalVariables;
+        };
+        
+        // This structure represents an edge.
+        template<storm::dd::DdType Type, typename ValueType>
+        struct EdgeDd {
+            EdgeDd(storm::dd::Add<Type> const& guardDd = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitionsDd = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) {
+                // Intentionally left empty.
+            }
+            
+            EdgeDd(EdgeDd const& other) : globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes), writtenGlobalVariables(other.writtenGlobalVariables), guardDd(other.guardDd), transitionsDd(other.transitionsDd) {
+                // Intentionally left empty.
+            }
+            
+            EdgeDd& operator=(EdgeDd const& other) {
+                if (this != &other) {
+                    globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes;
+                    writtenGlobalVariables = other.writtenGlobalVariables;
+                    guardDd = other.guardDd;
+                    transitionsDd = other.transitionsDd;
+                }
+                return *this;
+            }
+            
+            std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
+            std::set<storm::expressions::Variable> writtenGlobalVariables;
+            storm::dd::Add<Type, ValueType> guardDd;
+            storm::dd::Add<Type, ValueType> transitionsDd;
+        };
+        
+        // This structure represents a subcomponent of a composition.
        template<storm::dd::DdType Type, typename ValueType>
        struct AutomatonDd {
-
+            AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
+                // Intentionally left empty.
+            }
+            
+            std::map<uint64_t, std::vector<EdgeDd<Type, ValueType>>> actionIndexToEdges;
+            storm::dd::Add<Type, ValueType> identity;
        };
        
        template <storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
-            auto system = this->model->getSystemComposition().accept(*this, boost::any());
+        EdgeDd<Type, ValueType> extendEdgeWithIdentity(EdgeDd<Type, ValueType> const& edge, storm::dd::Add<Type, ValueType> const& identity) {
+            EdgeDd<Type, ValueType> result(edge);
+            result.transitionsDd *= identity;
+            return result;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
-        boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) {
+        EdgeDd<Type, ValueType> composeEdgesInParallel(EdgeDd<Type, ValueType> const& edge1, EdgeDd<Type, ValueType> const& edge2) {
+            EdgeDd<Type, ValueType> result;
+            
+            // Compute the set of variables written multiple times by the composition.
+            std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
+            std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
            
+            std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
+            std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
+            
+            std::set<storm::expressions::Variable> variablesWrittenMultipleTimes;
+            std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin()));
+            
+            result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes);
+            
+            // Compute the set of variables written by the composition.
+            std::set<storm::expressions::Variable> variablesWritten;
+            std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin()));
+            
+            result.writtenGlobalVariables = variablesWritten;
+            
+            // Compose the guards.
+            result.guardDd = edge1.guardDd * edge2.guardDd;
+            
+            // Compose the transitions.
+            result.transitionsDd = edge1.transitionsDd * edge2.transitionsDd;
+            
+            return result;
        }
        
+        // A class that is responsible for performing the actual composition.
        template <storm::dd::DdType Type, typename ValueType>
-        boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::RenameComposition const& composition, boost::any const& data) {
+        class AutomatonComposer : public storm::jani::CompositionVisitor {
+        public:
+            AutomatonComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : model(model), variables(variables) {
+                // Intentionally left empty.
+            }
            
-        }
+            AutomatonDd<Type, ValueType> compose() {
+                return boost::any_cast<AutomatonDd<Type, ValueType>>(this->model.getSystemComposition().accept(*this, boost::none));
+            }
+            
+            boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
+                return buildAutomatonDd(composition.getAutomatonName());
+            }
+            
+            boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
+                AutomatonDd<Type, ValueType> subautomaton = boost::any_cast<AutomatonDd<Type, ValueType>>(composition.getSubcomposition().accept(*this, boost::none));
+                
+                // Build a mapping from indices to indices for the renaming.
+                std::map<uint64_t, uint64_t> renamingIndexToIndex;
+                for (auto const& entry : composition.getRenaming()) {
+                    if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) {
+                        // Distinguish the cases where we hide the action or properly rename it.
+                        if (entry.second) {
+                            renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get()));
+                        } else {
+                            renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex());
+                        }
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action.");
+                    }
+                }
+                
+                // Finally, apply the renaming.
+                AutomatonDd<Type, ValueType> result(subautomaton.identity);
+                for (auto const& actionEdges : subautomaton.actionIndexToEdges) {
+                    auto it = renamingIndexToIndex.find(actionEdges.first);
+                    if (it != renamingIndexToIndex.end()) {
+                        // If we are to rename the action, do so.
+                        result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end());
+                    } else {
+                        // Otherwise copy over the edges.
+                        result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end());
+                    }
+                }
+                return result;
+            }
+            
+            boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
+                AutomatonDd<Type, ValueType> leftSubautomaton = boost::any_cast<AutomatonDd<Type, ValueType>>(composition.getLeftSubcomposition().accept(*this, boost::none));
+                AutomatonDd<Type, ValueType> rightSubautomaton = boost::any_cast<AutomatonDd<Type, ValueType>>(composition.getRightSubcomposition().accept(*this, boost::none));
+                
+                // Build the set of synchronizing action indices.
+                std::set<uint64_t> synchronizingActionIndices;
+                for (auto const& entry : composition.getSynchronizationAlphabet()) {
+                    if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) {
+                        synchronizingActionIndices.insert(this->model.getActionIndex(entry));
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action.");
+                    }
+                }
+                
+                // Perform the composition.
+                
+                // First, consider all actions in the left subcomposition.
+                AutomatonDd<Type, ValueType> result(leftSubautomaton.identity * rightSubautomaton.identity);
+                for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) {
+                    // If we need to synchronize over this action, do so now.
+                    if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) {
+                        auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first);
+                        if (rightIt != rightSubautomaton.actionIndexToEdges.end()) {
+                            for (auto const& edge1 : actionEdges.second) {
+                                for (auto const& edge2 : rightIt->second) {
+                                    result.actionIndexToEdges[actionEdges.first].push_back(composeEdgesInParallel(edge1, edge2));
+                                }
+                            }
+                        }
+                    } else {
+                        // Extend all edges by the missing identity (unsynchronizing) and copy them over.
+                        for (auto const& edge : actionEdges.second) {
+                            result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity));
+                        }
+                    }
+                }
+                
+                // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because
+                // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none,
+                // such transitions can not be taken and we can drop them.
+                for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) {
+                    if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) {
+                        for (auto const& edge : actionEdges.second) {
+                            result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity));
+                        }
+                    }
+                }
+                
+                return result;
+            }
+            
+        private:
+            EdgeDestinationDd<Type, ValueType> buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add<Type, ValueType> const& guard) {
+                storm::dd::Add<Type, ValueType> transitionsDd = variables.manager->template getAddOne<ValueType>();
+                
+                STORM_LOG_TRACE("Translating edge destination.");
+                
+                // Iterate over all assignments (boolean and integer) and build the DD for it.
+                std::set<storm::expressions::Variable> assignedVariables;
+                for (auto const& assignment : destination.getAssignments()) {
+                    // Record the variable as being written.
+                    STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap.at(assignment.getExpressionVariable()).getName());
+                    assignedVariables.insert(assignment.getExpressionVariable());
+                    
+                    // Translate the written variable.
+                    auto const& primedMetaVariable = variables.variableToColumnMetaVariableMap.at(assignment.getExpressionVariable());
+                    storm::dd::Add<Type, ValueType> writtenVariable = variables.manager->template getIdentity<ValueType>(primedMetaVariable);
+                    
+                    // Translate the expression that is being assigned.
+                    storm::dd::Add<Type, ValueType> updateExpression = variables.rowExpressionAdapter->translateExpression(assignment.getExpressionVariable());
+                    
+                    // Combine the update expression with the guard.
+                    storm::dd::Add<Type, ValueType> result = updateExpression * guard;
+                    
+                    // Combine the variable and the assigned expression.
+                    result = result.equals(writtenVariable).template toAdd<ValueType>();
+                    result *= guard;
+                    
+                    // Restrict the transitions to the range of the written variable.
+                    result = result * variables.manager->getRange(primedMetaVariable).template toAdd<ValueType>();
+                    
+                    transitionsDd *= result;
+                }
+                
+                // Compute the set of assigned global variables.
+                std::set<storm::expressions::Variable> assignedGlobalVariables;
+                std::set_intersection(assignedVariables.begin(), assignedVariables.end(), variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin()));
+                
+                // All unassigned boolean variables need to keep their value.
+                for (storm::jani::BooleanVariable const& variable : automaton.getVariables().getBooleanVariables()) {
+                    if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) {
+                        STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName());
+                        transitionsDd *= variables.variableToIdentityMap.at(variable.getExpressionVariable());
+                    }
+                }
+                
+                // All unassigned integer variables need to keep their value.
+                for (storm::jani::BoundedIntegerVariable const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                    if (assignedVariables.find(variable.getExpressionVariable()) == assignedVariables.end()) {
+                        STORM_LOG_TRACE("Multiplying identity of variable " << variable.getName());
+                        transitionsDd *= variables.variableToIdentityMap.at(variable.getExpressionVariable());
+                    }
+                }
+                
+                return EdgeDestinationDd<Type, ValueType>(transitionsDd * variables.rowExpressionAdapter->translateExpression(destination.getProbability()), assignedGlobalVariables);
+            }
+            
+            /*!
+             * Builds the DD for the given edge.
+             */
+            EdgeDd<Type, ValueType> buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) {
+                STORM_LOG_TRACE("Translating guard " << edge.getGuard());
+                storm::dd::Add<Type, ValueType> guard = variables.rowExpressionAdapter->translateExpression(edge.getGuard()) * variables.automatonToRangeMap.at(automaton.getName());
+                STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
+                
+                if (!guard.isZero()) {
+                    // Create the DDs representing the individual updates.
+                    std::vector<EdgeDestinationDd<Type, ValueType>> destinationDds;
+                    for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) {
+                        destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard));
+                        
+                        STORM_LOG_WARN_COND(!destinationDds.back().transitionsDd.isZero(), "Destination does not have any effect.");
+                    }
+                    
+                    // Start by gathering all variables that were written in at least one update.
+                    std::set<storm::expressions::Variable> globalVariablesInSomeUpdate;
+                    
+                    // If the edge is not labeled with the silent action, we have to analyze which portion of the global
+                    // variables was written by any of the updates and make all update results equal w.r.t. this set. If
+                    // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
+                    if (edge.getActionId() != this->model.getSilentActionIndex()) {
+                        std::for_each(destinationDds.begin(), destinationDds.end(), [&globalVariablesInSomeUpdate] (EdgeDestinationDd<Type, ValueType> const& edgeDestinationDd) { globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end()); } );
+                    } else {
+                        globalVariablesInSomeUpdate = variables.allGlobalVariables;
+                    }
+                    
+                    // Then, multiply the missing identities.
+                    for (auto& destinationDd : destinationDds) {
+                        std::set<storm::expressions::Variable> missingIdentities;
+                        std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
+                        
+                        for (auto const& variable : missingIdentities) {
+                            STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD.");
+                            destinationDd.transitionsDd *= variables.variableToIdentityMap.at(variable);
+                        }
+                    }
+                    
+                    // Now combine the destination DDs to the edge DD.
+                    storm::dd::Add<Type, ValueType> transitionsDd = variables.manager->template getAddZero<ValueType>();
+                    for (auto const& destinationDd : destinationDds) {
+                        transitionsDd += destinationDd.transitionsDd;
+                    }
+                    
+                    return EdgeDd<Type, ValueType>(guard, guard * transitionsDd, globalVariablesInSomeUpdate);
+                } else {
+                    return EdgeDd<Type, ValueType>(variables.manager->template getAddZero<ValueType>(), variables.manager->template getAddZero<ValueType>());
+                }
+            }
+            
+            /*!
+             * Builds the DD for the automaton with the given name.
+             */
+            AutomatonDd<Type, ValueType> buildAutomatonDd(std::string const& automatonName) {
+                AutomatonDd<Type, ValueType> result(variables.automatonToIdentityMap.at(automatonName));
+                
+                storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
+                for (auto const& edge : automaton.getEdges()) {
+                    // Build the edge and add it if it adds transitions.
+                    EdgeDd<Type, ValueType> edgeDd = buildEdgeDd(automaton, edge);
+                    if (!edgeDd.guardDd.isZero()) {
+                        result.actionIndexToEdges[edge.getActionId()].push_back(edgeDd);
+                    }
+                }
+                
+                return result;
+            }
+            
+            // The model that is referred to by the composition.
+            storm::jani::Model const& model;
+            
+            // The variable to use when building an automaton.
+            CompositionVariables<Type, ValueType> const& variables;
+        };
        
        template <storm::dd::DdType Type, typename ValueType>
-        boost::any DdJaniModelBuilder<Type, ValueType>::visit(storm::jani::ParallelComposition const& composition, boost::any const& data) {
+        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::translate() {
+            CompositionVariableCreator<Type, ValueType> variableCreator(*this->model);
+            CompositionVariables<Type, ValueType> variables = variableCreator.create();
+            
+            AutomatonComposer<Type, ValueType> composer(*this->model, variables);
+            AutomatonDd<Type, ValueType> system = composer.compose();
            
+            // FIXME
+            return nullptr;
        }
-
        
        template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
        template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@ -19,7 +19,7 @@ namespace storm {
    namespace builder {
        
        template <storm::dd::DdType Type, typename ValueType = double>
-        class DdJaniModelBuilder : public storm::jani::CompositionVisitor {
+        class DdJaniModelBuilder {
        public:            
            struct Options {
                /*!
@ -108,11 +108,7 @@ namespace storm {
             * @return The translated model.
             */
            storm::jani::Model const& getTranslatedModel() const;
-            
-            virtual boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override;
-            virtual boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override;
-            virtual boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override;
-            
+                        
        private:
            /// The model to translate.
            boost::optional<storm::jani::Model> model;
--- a/src/storage/jani/Automaton.cpp
+++ b/src/storage/jani/Automaton.cpp
@ -8,133 +8,42 @@ namespace storm {
    namespace jani {
        
        namespace detail {
-            EdgeIterator::EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
+            Edges::Edges(iterator it, iterator ite) : it(it), ite(ite) {
                // Intentionally left empty.
            }
            
-            EdgeIterator& EdgeIterator::operator++() {
-                incrementIterator();
-                return *this;
+            Edges::iterator Edges::begin() const {
+                return it;
            }
            
-            EdgeIterator& EdgeIterator::operator++(int) {
-                incrementIterator();
-                return *this;
+            Edges::iterator Edges::end() const {
+                return ite;
            }
            
-            Edge& EdgeIterator::operator*() {
-                return *in_it;
+            bool Edges::empty() const {
+                return it == ite;
            }
            
-            bool EdgeIterator::operator==(EdgeIterator const& other) const {
-                return this->out_it == other.out_it && this->in_it == other.in_it;
-            }
-            
-            bool EdgeIterator::operator!=(EdgeIterator const& other) const {
-                return !(*this == other);
-            }
-            
-            void EdgeIterator::incrementIterator() {
-                ++in_it;
-                
-                // If the inner iterator has reached its end move it to the beginning of the next outer element.
-                if (in_it == out_it->end()) {
-                    ++out_it;
-                    while (out_it != out_ite && out_it->empty()) {
-                        ++out_it;
-                        in_it = out_it->end();
-                    }
-                    if (out_it != out_ite) {
-                        in_it = out_it->begin();
-                    }
-                }
-            }
-            
-            ConstEdgeIterator::ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it) : automaton(automaton), out_it(out_it), out_ite(out_ite), in_it(in_it) {
-                // Intentionally left empty.
-            }
-            
-            ConstEdgeIterator& ConstEdgeIterator::operator++() {
-                incrementIterator();
-                return *this;
-            }
-            
-            ConstEdgeIterator& ConstEdgeIterator::operator++(int) {
-                incrementIterator();
-                return *this;
-            }
-            
-            Edge const& ConstEdgeIterator::operator*() const {
-                return *in_it;
-            }
-            
-            bool ConstEdgeIterator::operator==(ConstEdgeIterator const& other) const {
-                return this->out_it == other.out_it && this->in_it == other.in_it;
-            }
-            
-            bool ConstEdgeIterator::operator!=(ConstEdgeIterator const& other) const {
-                return !(*this == other);
-            }
-            
-            void ConstEdgeIterator::incrementIterator() {
-                ++in_it;
-                
-                // If the inner iterator has reached its end move it to the beginning of the next outer element.
-                if (in_it == out_it->end()) {
-                    ++out_it;
-                    while (out_it != out_ite && out_it->empty()) {
-                        ++out_it;
-                        in_it = out_it->end();
-                    }
-                    if (out_it != out_ite) {
-                        in_it = out_it->begin();
-                    }
-                }
-            }
-            
-            Edges::Edges(Automaton& automaton) : automaton(automaton) {
+            ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) {
                // Intentionally left empty.
            }
            
-            EdgeIterator Edges::begin() {
-                auto outer = automaton.edges.begin();
-                while (outer != automaton.edges.end() && outer->empty()) {
-                    ++outer;
-                }
-                if (outer == automaton.edges.end()) {
-                    return end();
-                } else {
-                    return EdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
-                }
-            }
-            
-            EdgeIterator Edges::end() {
-                return EdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
-            }
-            
-            ConstEdges::ConstEdges(Automaton const& automaton) : automaton(automaton) {
-                // Intentionally left empty.
+            ConstEdges::const_iterator ConstEdges::begin() const {
+                return it;
            }
            
-            ConstEdgeIterator ConstEdges::begin() const {
-                auto outer = automaton.edges.begin();
-                while (outer != automaton.edges.end() && outer->empty()) {
-                    ++outer;
-                }
-                if (outer == automaton.edges.end()) {
-                    return end();
-                } else {
-                    return ConstEdgeIterator(automaton, outer, automaton.edges.end(), outer->begin());
-                }
+            ConstEdges::const_iterator ConstEdges::end() const {
+                return ite;
            }
-            
-            ConstEdgeIterator ConstEdges::end() const {
-                return ConstEdgeIterator(automaton, automaton.edges.end(), automaton.edges.end(), automaton.edges.back().end());
+
+            bool ConstEdges::empty() const {
+                return it == ite;
            }
        }
        
        Automaton::Automaton(std::string const& name) : name(name) {
-            // Intentionally left empty.
+            // Add a sentinel element to the mapping from locations to starting indices.
+            locationToStartingIndex.push_back(0);
        }
        
        std::string const& Automaton::getName() const {
@ -177,7 +86,7 @@ namespace storm {
            STORM_LOG_THROW(!this->hasLocation(location.getName()), storm::exceptions::WrongFormatException, "Cannot add location with name '" << location.getName() << "', because a location with this name already exists.");
            locationToIndex.emplace(location.getName(), locations.size());
            locations.push_back(location);
-            edges.push_back(EdgeSet());
+            locationToStartingIndex.push_back(edges.size());
            return locations.size() - 1;
        }

@ -204,31 +113,62 @@ namespace storm {
        uint64_t Automaton::getInitialLocationIndex() const {
            return initialLocationIndex;
        }
+
+        Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) {
+            auto it = locationToIndex.find(name);
+            STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve edges from unknown location '" << name << ".");
+            return getEdgesFromLocation(it->second);
+        }
+        
+        Automaton::Edges Automaton::getEdgesFromLocation(uint64_t index) {
+            auto it = edges.begin();
+            std::advance(it, locationToStartingIndex[index]);
+            auto ite = edges.begin();
+            std::advance(ite, locationToStartingIndex[index + 1]);
+            return Edges(it, ite);
+        }
        
-        EdgeSet const& Automaton::getEdgesFromLocation(std::string const& name) const {
+        Automaton::ConstEdges Automaton::getEdgesFromLocation(std::string const& name) const {
            auto it = locationToIndex.find(name);
            STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve edges from unknown location '" << name << ".");
            return getEdgesFromLocation(it->second);
        }
        
-        EdgeSet const& Automaton::getEdgesFromLocation(uint64_t index) const {
-            return edges[index];
+        Automaton::ConstEdges Automaton::getEdgesFromLocation(uint64_t index) const {
+            auto it = edges.begin();
+            std::advance(it, locationToStartingIndex[index]);
+            auto ite = edges.begin();
+            std::advance(ite, locationToStartingIndex[index + 1]);
+            return ConstEdges(it, ite);
        }
        
        void Automaton::addEdge(Edge const& edge) {
            STORM_LOG_THROW(edge.getSourceLocationId() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationId() << "'.");
-            edges[edge.getSourceLocationId()].addEdge(edge);
+            
+            // Find the right position for the edge and insert it properly.
+            auto posIt = edges.begin();
+            std::advance(posIt, locationToStartingIndex[edge.getSourceLocationId() + 1]);
+            edges.insert(posIt, edge);
+            
+            // Now update the starting indices of all subsequent locations.
+            for (uint64_t locationIndex = edge.getSourceLocationId() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
+                ++locationToStartingIndex[locationIndex];
+            }
        }
        
-        Automaton::Edges Automaton::getEdges() {
-            return Edges(*this);
+        std::vector<Edge>& Automaton::getEdges() {
+            return edges;
        }
        
-        Automaton::ConstEdges Automaton::getEdges() const {
-            return ConstEdges(*this);
+        std::vector<Edge> const& Automaton::getEdges() const {
+            return edges;
        }
        
        uint64_t Automaton::getNumberOfLocations() const {
+            return locations.size();
+        }
+        
+        uint64_t Automaton::getNumberOfEdges() const {
            return edges.size();
        }

--- a/src/storage/jani/Automaton.h
+++ b/src/storage/jani/Automaton.h
@ -5,7 +5,7 @@
 #include <unordered_map>

 #include "src/storage/jani/VariableSet.h"
-#include "src/storage/jani/EdgeSet.h"
+#include "src/storage/jani/Edge.h"
 #include "src/storage/jani/Location.h"

 namespace storm {
@ -14,108 +14,58 @@ namespace storm {
        class Automaton;
        
        namespace detail {
-            class EdgeIterator {
-            private:
-                typedef std::vector<EdgeSet>::iterator outer_iter;
-                typedef EdgeSet::iterator inner_iter;
-                
+            class Edges {
            public:
-                /*!
-                 * Creates an iterator over all edges.
-                 */
-                EdgeIterator(Automaton& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
-                
-                // Methods to advance the iterator.
-                EdgeIterator& operator++();
-                EdgeIterator& operator++(int);
-                
-                Edge& operator*();
-                
-                bool operator==(EdgeIterator const& other) const;
-                bool operator!=(EdgeIterator const& other) const;
-                
-            private:
-                // Moves the iterator to the next position.
-                void incrementIterator();
-                
-                // The underlying automaton.
-                Automaton& automaton;
+                typedef std::vector<Edge>::iterator iterator;
+                typedef std::vector<Edge>::const_iterator const_iterator;
                
-                // The current iterator positions.
-                outer_iter out_it;
-                outer_iter out_ite;
-                inner_iter in_it;
-            };
-            
-            class ConstEdgeIterator {
-            private:
-                typedef std::vector<EdgeSet>::const_iterator outer_iter;
-                typedef EdgeSet::const_iterator inner_iter;
+                Edges(iterator it, iterator ite);
                
-            public:
                /*!
-                 * Creates an iterator over all edges.
+                 * Retrieves an iterator to the edges.
                 */
-                ConstEdgeIterator(Automaton const& automaton, outer_iter out_it, outer_iter out_ite, inner_iter in_it);
-                
-                // Methods to advance the iterator.
-                ConstEdgeIterator& operator++();
-                ConstEdgeIterator& operator++(int);
-                
-                Edge const& operator*() const;
-                
-                bool operator==(ConstEdgeIterator const& other) const;
-                bool operator!=(ConstEdgeIterator const& other) const;
-                
-            private:
-                // Moves the iterator to the next position.
-                void incrementIterator();
-                
-                // The underlying automaton.
-                Automaton const& automaton;
-                
-                // The current iterator positions.
-                outer_iter out_it;
-                outer_iter out_ite;
-                inner_iter in_it;
-            };
-            
-            class Edges {
-            public:
-                Edges(Automaton& automaton);
+                iterator begin() const;
                
                /*!
-                 * Retrieves an iterator to all edges of the automaton.
+                 * Retrieves an end iterator to the edges.
                 */
-                EdgeIterator begin();
+                iterator end() const;
                
                /*!
-                 * Retrieves the end iterator to edges of the automaton.
+                 * Determines whether this set of edges is empty.
                 */
-                EdgeIterator end();
+                bool empty() const;
                
            private:
-                // The underlying automaton.
-                Automaton& automaton;
+                iterator it;
+                iterator ite;
            };
            
            class ConstEdges {
            public:
-                ConstEdges(Automaton const& automaton);
+                typedef std::vector<Edge>::iterator iterator;
+                typedef std::vector<Edge>::const_iterator const_iterator;
+                
+                ConstEdges(const_iterator it, const_iterator ite);
                
                /*!
-                 * Retrieves an iterator to all edges of the automaton.
+                 * Retrieves an iterator to the edges.
                 */
-                ConstEdgeIterator begin() const;
+                const_iterator begin() const;
                
                /*!
-                 * Retrieves the end iterator to edges of the automaton.
+                 * Retrieves an end iterator to the edges.
                 */
-                ConstEdgeIterator end() const;
+                const_iterator end() const;
+
+                /*!
+                 * Determines whether this set of edges is empty.
+                 */
+                bool empty() const;
                
            private:
-                // The underlying automaton.
-                Automaton const& automaton;
+                const_iterator it;
+                const_iterator ite;
            };
        }
        
@ -209,16 +159,26 @@ namespace storm {
             * Retrieves the index of the initial location.
             */
            uint64_t getInitialLocationIndex() const;
+
+            /*!
+             * Retrieves the edges of the location with the given name.
+             */
+            Edges getEdgesFromLocation(std::string const& name);
+            
+            /*!
+             * Retrieves the edges of the location with the given index.
+             */
+            Edges getEdgesFromLocation(uint64_t index);
            
            /*!
             * Retrieves the edges of the location with the given name.
             */
-            EdgeSet const& getEdgesFromLocation(std::string const& name) const;
+            ConstEdges getEdgesFromLocation(std::string const& name) const;

            /*!
             * Retrieves the edges of the location with the given index.
             */
-            EdgeSet const& getEdgesFromLocation(uint64_t index) const;
+            ConstEdges getEdgesFromLocation(uint64_t index) const;
            
            /*!
             * Adds an edge to the automaton.
@ -228,35 +188,44 @@ namespace storm {
            /*!
             * Retrieves the edges of the automaton.
             */
-            Edges getEdges();
+            std::vector<Edge>& getEdges();

            /*!
             * Retrieves the edges of the automaton.
             */
-            ConstEdges getEdges() const;
+            std::vector<Edge> const& getEdges() const;

            /*!
             * Retrieves the number of locations.
             */
            uint64_t getNumberOfLocations() const;
-            
+
+            /*!
+             * Retrieves the number of edges.
+             */
+            uint64_t getNumberOfEdges() const;
+
        private:
-            // The name of the automaton.
+            /// The name of the automaton.
            std::string name;

-            // The set of variables of this automaton.
+            /// The set of variables of this automaton.
            VariableSet variables;
            
-            // The locations of the automaton.
+            /// The locations of the automaton.
            std::vector<Location> locations;
            
-            // A mapping of location names to their indices.
+            /// A mapping of location names to their indices.
            std::unordered_map<std::string, uint64_t> locationToIndex;
            
-            // All edges of the automaton. The edges at index i are the edges of the location with index i.
-            std::vector<EdgeSet> edges;
+            /// All edges of the automaton
+            std::vector<Edge> edges;
+            
+            /// A mapping from location indices to the starting indices. If l is mapped to i, it means that the edges
+            /// leaving location l start at index i of the edges vector.
+            std::vector<uint64_t> locationToStartingIndex;

-            // The index of the initial location.
+            /// The index of the initial location.
            uint64_t initialLocationIndex;
        };
        
--- a/src/storage/jani/EdgeSet.cpp
+++ b/src/storage/jani/EdgeSet.cpp
@ -1,35 +0,0 @@
-#include "src/storage/jani/EdgeSet.h"
-
-namespace storm {
-    namespace jani {
-        
-        EdgeSet::EdgeSet(std::vector<Edge> const& edges) : edges(edges) {
-            // Intentionally left empty.
-        }
-        
-        EdgeSet::iterator EdgeSet::begin() {
-            return edges.begin();
-        }
-        
-        EdgeSet::iterator EdgeSet::end() {
-            return edges.end();
-        }
-        
-        EdgeSet::const_iterator EdgeSet::begin() const {
-            return edges.cbegin();
-        }
-        
-        EdgeSet::const_iterator EdgeSet::end() const {
-            return edges.cend();
-        }
-        
-        void EdgeSet::addEdge(Edge const& edge) {
-            edges.push_back(edge);
-        }
-        
-        bool EdgeSet::empty() const {
-            return edges.empty();
-        }
-        
-    }
-}
--- a/src/storage/jani/EdgeSet.h
+++ b/src/storage/jani/EdgeSet.h
@ -1,41 +0,0 @@
-#pragma once
-
-#include "src/storage/jani/Edge.h"
-
-namespace storm {
-    namespace jani {
-        
-        class EdgeSet {
-        public:
-            typedef std::vector<Edge> container_type;
-            typedef container_type::iterator iterator;
-            typedef container_type::const_iterator const_iterator;
-            
-            /*!
-             * Creates a new set of edges.
-             */
-            EdgeSet(std::vector<Edge> const& edges = std::vector<Edge>());
-
-            /*!
-             * Adds the edge to the edges.
-             */
-            void addEdge(Edge const& edge);
-            
-            /*!
-             * Retrieves whether the set of edges is empty.
-             */
-            bool empty() const;
-            
-            // Methods to get an iterator to the edges.
-            iterator begin();
-            iterator end();
-            const_iterator begin() const;
-            const_iterator end() const;
-            
-        private:
-            // The set of edges.
-            container_type edges;
-        };
-        
-    }
-}
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@ -65,6 +65,10 @@ namespace storm {
            return it->second;
        }
        
+        std::vector<Action> const& Model::getActions() const {
+            return actions;
+        }
+        
        uint64_t Model::addConstant(Constant const& constant) {
            auto it = constantToIndex.find(constant.getName());
            STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists.");
@ -147,6 +151,10 @@ namespace storm {
            return automata[it->second];
        }
        
+        std::size_t Model::getNumberOfAutomata() const {
+            return automata.size();
+        }
+        
        std::shared_ptr<Composition> Model::getStandardSystemComposition() const {
            std::set<std::string> fullSynchronizationAlphabet = getActionNames(false);
            
@ -249,6 +257,7 @@ namespace storm {
            
            // Substitute constants in all global variables.
            for (auto& variable : result.getGlobalVariables()) {
+                std::cout << "init: " << variable.getInitialValue() << std::endl;
                variable.setInitialValue(variable.getInitialValue().substitute(constantSubstitution));
            }
            for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@ -72,6 +72,11 @@ namespace storm {
             */
            Action const& getAction(uint64_t index) const;
            
+            /*!
+             * Retrieves the actions of the model.
+             */
+            std::vector<Action> const& getActions() const;
+            
            /*!
             * Adds the given constant to the model.
             */
@ -157,6 +162,11 @@ namespace storm {
             */
            Automaton const& getAutomaton(std::string const& name) const;

+            /*!
+             * Retrieves the number of automata in this model.
+             */
+            std::size_t getNumberOfAutomata() const;
+            
            /*!
             * Sets the system composition expression of the JANI model.
             */
--- a/src/storage/jani/RenameComposition.cpp
+++ b/src/storage/jani/RenameComposition.cpp
@ -20,6 +20,10 @@ namespace storm {
            return visitor.visit(*this, data);
        }
        
+        std::map<std::string, boost::optional<std::string>> const& RenameComposition::getRenaming() const {
+            return renaming;
+        }
+        
        void RenameComposition::write(std::ostream& stream) const {
            std::vector<std::string> renamingStrings;
            
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@ -9,190 +9,96 @@ namespace storm {
        
        namespace detail {
            
-            VariableSetIterator::VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
-                // Intentionally left empty.
-            }
-            
-            VariableSetIterator& VariableSetIterator::operator++() {
-                incrementIterator();
-                return *this;
-            }
-            
-            VariableSetIterator& VariableSetIterator::operator++(int) {
-                incrementIterator();
-                return *this;
-            }
-            
-            Variable& VariableSetIterator::operator*() {
-                if (it.which() == 0) {
-                    return *boost::get<bool_iter>(it);
-                } else if (it.which() == 1) {
-                    return *boost::get<bint_iter>(it);
-                } else {
-                    return *boost::get<int_iter>(it);
-                }
-            }
-            
-            bool VariableSetIterator::operator==(VariableSetIterator const& other) const {
-                return this->it == other.it;
+            template<typename VariableType>
+            VariableType& Dereferencer<VariableType>::operator()(std::shared_ptr<VariableType> const& d) {
+                return *d;
            }
            
-            bool VariableSetIterator::operator!=(VariableSetIterator const& other) const {
-                return this->it != other.it;
-            }
-            
-            void VariableSetIterator::incrementIterator() {
-                if (it.which() == 0) {
-                    bool_iter& tmp = boost::get<bool_iter>(it);
-                    if (tmp != variableSet.getBooleanVariables().end()) {
-                        ++tmp;
-                    } else {
-                        it = variableSet.getBoundedIntegerVariables().begin();
-                    }
-                } else if (it.which() == 1) {
-                    bint_iter& tmp = boost::get<bint_iter>(it);
-                    if (tmp != variableSet.getBoundedIntegerVariables().end()) {
-                        ++tmp;
-                    } else {
-                        it = variableSet.getUnboundedIntegerVariables().begin();
-                    }
-                } else {
-                    ++boost::get<int_iter>(it);
-                }
-            }
-            
-            ConstVariableSetIterator::ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator) : variableSet(variableSet), it(initialIterator) {
+            template<typename VariableType>
+            Variables<VariableType>::Variables(input_iterator it, input_iterator ite) : it(it), ite(ite) {
                // Intentionally left empty.
            }
-            
-            ConstVariableSetIterator& ConstVariableSetIterator::operator++() {
-                incrementIterator();
-                return *this;
-            }
-            
-            ConstVariableSetIterator& ConstVariableSetIterator::operator++(int) {
-                incrementIterator();
-                return *this;
-            }
-            
-            Variable const& ConstVariableSetIterator::operator*() {
-                if (it.which() == 0) {
-                    return *boost::get<bool_iter>(it);
-                } else if (it.which() == 1) {
-                    return *boost::get<bint_iter>(it);
-                } else {
-                    return *boost::get<int_iter>(it);
-                }
+                
+            template<typename VariableType>
+            typename Variables<VariableType>::iterator Variables<VariableType>::begin() {
+                return boost::make_transform_iterator(it, Dereferencer<VariableType>());
            }
            
-            bool ConstVariableSetIterator::operator==(ConstVariableSetIterator const& other) const {
-                return this->it == other.it;
+            template<typename VariableType>
+            typename Variables<VariableType>::iterator Variables<VariableType>::end() {
+                return boost::make_transform_iterator(ite, Dereferencer<VariableType>());
            }
-            
-            bool ConstVariableSetIterator::operator!=(ConstVariableSetIterator const& other) const {
-                return this->it != other.it;
-            }
-            
-            void ConstVariableSetIterator::incrementIterator() {
-                if (it.which() == 0) {
-                    bool_iter& tmp = boost::get<bool_iter>(it);
-                    if (tmp != variableSet.getBooleanVariables().end()) {
-                        ++tmp;
-                    } else {
-                        it = variableSet.getBoundedIntegerVariables().begin();
-                    }
-                } else if (it.which() == 1) {
-                    bint_iter& tmp = boost::get<bint_iter>(it);
-                    if (tmp != variableSet.getBoundedIntegerVariables().end()) {
-                        ++tmp;
-                    } else {
-                        it = variableSet.getUnboundedIntegerVariables().begin();
-                    }
-                } else {
-                    ++boost::get<int_iter>(it);
-                }
-            }
-            
-            IntegerVariables::IntegerVariables(VariableSet& variableSet) : variableSet(variableSet) {
-                // Intentionally left empty.
-            }
-            
-            VariableSetIterator IntegerVariables::begin() {
-                return VariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
-            }
-            
-            VariableSetIterator IntegerVariables::end() {
-                return VariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
-            }
-            
-            ConstIntegerVariables::ConstIntegerVariables(VariableSet const& variableSet) : variableSet(variableSet) {
+
+            template<typename VariableType>
+            ConstVariables<VariableType>::ConstVariables(const_input_iterator it, const_input_iterator ite) : it(it), ite(ite) {
                // Intentionally left empty.
            }
            
-            ConstVariableSetIterator ConstIntegerVariables::begin() const {
-                return ConstVariableSetIterator(variableSet, variableSet.getBoundedIntegerVariables().begin());
+            template<typename VariableType>
+            typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::begin() {
+                return boost::make_transform_iterator(it, Dereferencer<VariableType>());
            }
            
-            ConstVariableSetIterator ConstIntegerVariables::end() const {
-                return ConstVariableSetIterator(variableSet, variableSet.getUnboundedIntegerVariables().end());
+            template<typename VariableType>
+            typename ConstVariables<VariableType>::const_iterator ConstVariables<VariableType>::end() {
+                return boost::make_transform_iterator(ite, Dereferencer<VariableType>());
            }
+
        }
        
        VariableSet::VariableSet() {
            // Intentionally left empty.
        }
        
-        std::vector<BooleanVariable>& VariableSet::getBooleanVariables() {
-            return booleanVariables;
+        detail::Variables<BooleanVariable> VariableSet::getBooleanVariables() {
+            return detail::Variables<BooleanVariable>(booleanVariables.begin(), booleanVariables.end());
        }
        
-        std::vector<BooleanVariable> const& VariableSet::getBooleanVariables() const {
-            return booleanVariables;
-        }
-
-        std::vector<BoundedIntegerVariable>& VariableSet::getBoundedIntegerVariables() {
-            return boundedIntegerVariables;
+        detail::ConstVariables<BooleanVariable> VariableSet::getBooleanVariables() const {
+            return detail::ConstVariables<BooleanVariable>(booleanVariables.begin(), booleanVariables.end());
        }

-        std::vector<BoundedIntegerVariable> const& VariableSet::getBoundedIntegerVariables() const {
-            return boundedIntegerVariables;
+        detail::Variables<BoundedIntegerVariable> VariableSet::getBoundedIntegerVariables() {
+            return detail::Variables<BoundedIntegerVariable>(boundedIntegerVariables.begin(), boundedIntegerVariables.end());
        }

-        std::vector<UnboundedIntegerVariable>& VariableSet::getUnboundedIntegerVariables() {
-            return unboundedIntegerVariables;
+        detail::ConstVariables<BoundedIntegerVariable> VariableSet::getBoundedIntegerVariables() const {
+            return detail::ConstVariables<BoundedIntegerVariable>(boundedIntegerVariables.begin(), boundedIntegerVariables.end());
        }

-        std::vector<UnboundedIntegerVariable> const& VariableSet::getUnboundedIntegerVariables() const {
-            return unboundedIntegerVariables;
+        detail::Variables<UnboundedIntegerVariable> VariableSet::getUnboundedIntegerVariables() {
+            return detail::Variables<UnboundedIntegerVariable>(unboundedIntegerVariables.begin(), unboundedIntegerVariables.end());
        }

-        VariableSet::IntegerVariables VariableSet::getIntegerVariables() {
-            return IntegerVariables(*this);
+        detail::ConstVariables<UnboundedIntegerVariable> VariableSet::getUnboundedIntegerVariables() const {
+            return detail::ConstVariables<UnboundedIntegerVariable>(unboundedIntegerVariables.begin(), unboundedIntegerVariables.end());
        }

-        VariableSet::ConstIntegerVariables VariableSet::getIntegerVariables() const {
-            return ConstIntegerVariables(*this);
-        }
-        
        void VariableSet::addBooleanVariable(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.");
-            booleanVariables.push_back(variable);
+            std::shared_ptr<BooleanVariable> newVariable = std::make_shared<BooleanVariable>(variable);
+            variables.push_back(newVariable);
+            booleanVariables.push_back(newVariable);
            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
-            variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(0, booleanVariables.size() - 1));
+            variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
        }
        
        void VariableSet::addBoundedIntegerVariable(BoundedIntegerVariable 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.");
-            boundedIntegerVariables.push_back(variable);
+            std::shared_ptr<BoundedIntegerVariable> newVariable = std::make_shared<BoundedIntegerVariable>(variable);
+            variables.push_back(newVariable);
+            boundedIntegerVariables.push_back(newVariable);
            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
-            variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(1, boundedIntegerVariables.size() - 1));
+            variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
        }
        
        void VariableSet::addUnboundedIntegerVariable(UnboundedIntegerVariable 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.");
-            unboundedIntegerVariables.push_back(variable);
+            std::shared_ptr<UnboundedIntegerVariable> newVariable = std::make_shared<UnboundedIntegerVariable>(variable);
+            variables.push_back(newVariable);
+            unboundedIntegerVariables.push_back(newVariable);
            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
-            variableToVariable.emplace(variable.getExpressionVariable(), std::make_pair(2, boundedIntegerVariables.size() - 1));
+            variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
        }
        
        bool VariableSet::hasVariable(std::string const& name) const {
@ -206,36 +112,42 @@ namespace storm {
        }

        VariableSet::iterator VariableSet::begin() {
-            return iterator(*this, booleanVariables.begin());
+            return boost::make_transform_iterator(variables.begin(), detail::Dereferencer<Variable>());
        }

        VariableSet::const_iterator VariableSet::begin() const {
-            return const_iterator(*this, booleanVariables.begin());
+            return boost::make_transform_iterator(variables.begin(), detail::Dereferencer<Variable const>());
        }
        
        VariableSet::iterator VariableSet::end() {
-            return iterator(*this, unboundedIntegerVariables.end());
+            return boost::make_transform_iterator(variables.end(), detail::Dereferencer<Variable>());
        }

        VariableSet::const_iterator VariableSet::end() const {
-            return const_iterator(*this, unboundedIntegerVariables.end());
+            return boost::make_transform_iterator(variables.end(), detail::Dereferencer<Variable const>());
        }

        Variable const& VariableSet::getVariable(storm::expressions::Variable const& variable) const {
            auto it = variableToVariable.find(variable);
            STORM_LOG_THROW(it != variableToVariable.end(), storm::exceptions::InvalidArgumentException, "Unable to retrieve unknown variable '" << variable.getName() << "'.");
-            
-            if (it->second.first == 0) {
-                return booleanVariables[it->second.second];
-            } else if (it->second.first == 1) {
-                return boundedIntegerVariables[it->second.second];
-            } else {
-                return unboundedIntegerVariables[it->second.second];
-            }
+            return *it->second;
        }
        
        bool VariableSet::hasVariable(storm::expressions::Variable const& variable) const {
            return variableToVariable.find(variable) != variableToVariable.end();
        }
+        
+        bool VariableSet::containsBooleanVariable() const {
+            return !booleanVariables.empty();
+        }
+        
+        bool VariableSet::containsBoundedIntegerVariable() const {
+            return !boundedIntegerVariables.empty();
+        }
+        
+        bool VariableSet::containsUnboundedIntegerVariables() const {
+            return !unboundedIntegerVariables.empty();
+        }
+
    }
 }
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@ -3,7 +3,7 @@
 #include <vector>
 #include <set>

-#include <boost/variant.hpp>
+#include <boost/iterator/transform_iterator.hpp>

 #include "src/storage/jani/BooleanVariable.h"
 #include "src/storage/jani/UnboundedIntegerVariable.h"
@ -16,117 +16,55 @@ namespace storm {
        
        namespace detail {
            
-            class VariableSetIterator {
-            private:
-                typedef std::vector<BooleanVariable>::iterator bool_iter;
-                typedef std::vector<BoundedIntegerVariable>::iterator bint_iter;
-                typedef std::vector<UnboundedIntegerVariable>::iterator int_iter;
-                
+            template<typename VariableType>
+            class Dereferencer {
            public:
-                /*!
-                 * Creates an iterator over all variables.
-                 */
-                VariableSetIterator(VariableSet& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
-                
-                // Methods to advance the iterator.
-                VariableSetIterator& operator++();
-                VariableSetIterator& operator++(int);
-                
-                Variable& operator*();
-
-                bool operator==(VariableSetIterator const& other) const;
-                bool operator!=(VariableSetIterator const& other) const;
-                
-            private:
-                // Moves the iterator to the next position.
-                void incrementIterator();
-                
-                // The underlying variable set.
-                VariableSet& variableSet;
-
-                // The current iterator position.
-                boost::variant<bool_iter, bint_iter, int_iter> it;
+                VariableType& operator()(std::shared_ptr<VariableType> const& d);
            };
            
-            class ConstVariableSetIterator {
-            private:
-                typedef std::vector<BooleanVariable>::const_iterator bool_iter;
-                typedef std::vector<BoundedIntegerVariable>::const_iterator bint_iter;
-                typedef std::vector<UnboundedIntegerVariable>::const_iterator int_iter;
-                
+            template<typename VariableType>
+            class Variables {
            public:
-                /*!
-                 * Creates an iterator over all variables.
-                 */
-                ConstVariableSetIterator(VariableSet const& variableSet, boost::variant<bool_iter, bint_iter, int_iter> initialIterator);
-                
-                // Methods to advance the iterator.
-                ConstVariableSetIterator& operator++();
-                ConstVariableSetIterator& operator++(int);
-                
-                Variable const& operator*();
-                
-                bool operator==(ConstVariableSetIterator const& other) const;
-                bool operator!=(ConstVariableSetIterator const& other) const;
-                
-            private:
-                // Moves the iterator to the next position.
-                void incrementIterator();
-                
-                // The underlying variable set.
-                VariableSet const& variableSet;
+                typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
+                typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
+                typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
+                typedef boost::transform_iterator<Dereferencer<VariableType const>, const_input_iterator> const_iterator;
                
-                // The current iterator position.
-                boost::variant<bool_iter, bint_iter, int_iter> it;
-            };
-            
-            class IntegerVariables {
-            public:
-                IntegerVariables(VariableSet& variableSet);
+                Variables(input_iterator it, input_iterator ite);
                
-                /*!
-                 * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
-                 */
-                VariableSetIterator begin();
-
-                /*!
-                 * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
-                 */
-                VariableSetIterator end();
+                iterator begin();
+                iterator end();
                
            private:
-                // The underlying variable set.
-                VariableSet& variableSet;
+                input_iterator it;
+                input_iterator ite;
            };
-            
-            class ConstIntegerVariables {
+
+            template<typename VariableType>
+            class ConstVariables {
            public:
-                ConstIntegerVariables(VariableSet const& variableSet);
+                typedef typename std::vector<std::shared_ptr<VariableType>>::iterator input_iterator;
+                typedef typename std::vector<std::shared_ptr<VariableType>>::const_iterator const_input_iterator;
+                typedef boost::transform_iterator<Dereferencer<VariableType>, input_iterator> iterator;
+                typedef boost::transform_iterator<Dereferencer<VariableType const>, const_input_iterator> const_iterator;
                
-                /*!
-                 * Retrieves an iterator to all integer variables (bounded and unbounded) in the variable set.
-                 */
-                ConstVariableSetIterator begin() const;
+                ConstVariables(const_input_iterator it, const_input_iterator ite);
                
-                /*!
-                 * Retrieves the end iterator to all integer variables (bounded and unbounded) in the variable set.
-                 */
-                ConstVariableSetIterator end() const;
+                const_iterator begin();
+                const_iterator end();
                
            private:
-                // The underlying variable set.
-                VariableSet const& variableSet;
+                input_iterator it;
+                input_iterator ite;
            };
        }
        
        class VariableSet {
        public:
-            friend class detail::VariableSetIterator;
-            
-            typedef detail::VariableSetIterator iterator;
-            typedef detail::ConstVariableSetIterator const_iterator;
-            typedef detail::IntegerVariables IntegerVariables;
-            typedef detail::ConstIntegerVariables ConstIntegerVariables;
+            typedef typename std::vector<std::shared_ptr<Variable>>::iterator input_iterator;
+            typedef typename std::vector<std::shared_ptr<Variable>>::const_iterator const_input_iterator;
+            typedef boost::transform_iterator<detail::Dereferencer<Variable>, input_iterator> iterator;
+            typedef boost::transform_iterator<detail::Dereferencer<Variable>, const_input_iterator> const_iterator;
            
            /*!
             * Creates an empty variable set.
@ -136,42 +74,32 @@ namespace storm {
            /*!
             * Retrieves the boolean variables in this set.
             */
-            std::vector<BooleanVariable>& getBooleanVariables();
+            detail::Variables<BooleanVariable> getBooleanVariables();

            /*!
             * Retrieves the boolean variables in this set.
             */
-            std::vector<BooleanVariable> const& getBooleanVariables() const;
+            detail::ConstVariables<BooleanVariable> getBooleanVariables() const;

            /*!
             * Retrieves the bounded integer variables in this set.
             */
-            std::vector<BoundedIntegerVariable>& getBoundedIntegerVariables();
+            detail::Variables<BoundedIntegerVariable> getBoundedIntegerVariables();

            /*!
             * Retrieves the bounded integer variables in this set.
             */
-            std::vector<BoundedIntegerVariable> const& getBoundedIntegerVariables() const;
+            detail::ConstVariables<BoundedIntegerVariable> getBoundedIntegerVariables() const;

            /*!
             * Retrieves the unbounded integer variables in this set.
             */
-            std::vector<UnboundedIntegerVariable>& getUnboundedIntegerVariables();
+            detail::Variables<UnboundedIntegerVariable> getUnboundedIntegerVariables();

            /*!
             * Retrieves the unbounded integer variables in this set.
             */
-            std::vector<UnboundedIntegerVariable> const& getUnboundedIntegerVariables() const;
-
-            /*!
-             * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
-             */
-            IntegerVariables getIntegerVariables();
-            
-            /*!
-             * Retrieves an iterable object to all integer (bounded and unbounded) variables in the variable set.
-             */
-            ConstIntegerVariables getIntegerVariables() const;
+            detail::ConstVariables<UnboundedIntegerVariable> getUnboundedIntegerVariables() const;
            
            /*!
             * Adds the given boolean variable to this set.
@ -228,21 +156,39 @@ namespace storm {
             */
            const_iterator end() const;

+            /*!
+             * Retrieves whether the set of variables contains a boolean variable.
+             */
+            bool containsBooleanVariable() const;
+
+            /*!
+             * Retrieves whether the set of variables contains a bounded integer variable.
+             */
+            bool containsBoundedIntegerVariable() const;
+
+            /*!
+             * Retrieves whether the set of variables contains an unbounded integer variable.
+             */
+            bool containsUnboundedIntegerVariables() const;
+
        private:
+            /// The vector of all variables.
+            std::vector<std::shared_ptr<Variable>> variables;
+            
            /// The boolean variables in this set.
-            std::vector<BooleanVariable> booleanVariables;
+            std::vector<std::shared_ptr<BooleanVariable>> booleanVariables;

            /// The bounded integer variables in this set.
-            std::vector<BoundedIntegerVariable> boundedIntegerVariables;
+            std::vector<std::shared_ptr<BoundedIntegerVariable>> boundedIntegerVariables;

            /// The unbounded integer variables in this set.
-            std::vector<UnboundedIntegerVariable> unboundedIntegerVariables;
+            std::vector<std::shared_ptr<UnboundedIntegerVariable>> unboundedIntegerVariables;
            
            /// A set of all variable names currently in use.
            std::map<std::string, storm::expressions::Variable> nameToVariable;
            
            /// A mapping from expression variables to their variable objects.
-            std::map<storm::expressions::Variable, std::pair<uint8_t, uint64_t>> variableToVariable;
+            std::map<storm::expressions::Variable, std::shared_ptr<Variable>> variableToVariable;
        };
        
    }
--- a/test/functional/.DS_Store
+++ b/test/functional/.DS_Store
--- a/test/functional/builder/DdJaniModelBuilderTest.cpp
+++ b/test/functional/builder/DdJaniModelBuilderTest.cpp
@ -0,0 +1,75 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
+#include "src/models/symbolic/Mdp.h"
+
+#include "src/storage/dd/Add.h"
+#include "src/storage/dd/Bdd.h"
+
+#include "src/models/symbolic/StandardRewardModel.h"
+#include "src/parser/PrismParser.h"
+#include "src/builder/DdJaniModelBuilder.h"
+
+TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::jani::Model janiModel = program.toJani();
+    
+    storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.translate();
+    EXPECT_EQ(13ul, model->getNumberOfStates());
+    EXPECT_EQ(20ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+    janiModel = program.toJani();
+    builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
+    model = builder.translate();
+    EXPECT_EQ(677ul, model->getNumberOfStates());
+    EXPECT_EQ(867ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    janiModel = program.toJani();
+    model = builder.translate();
+    EXPECT_EQ(8607ul, model->getNumberOfStates());
+    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    janiModel = program.toJani();
+    model = builder.translate();
+    EXPECT_EQ(273ul, model->getNumberOfStates());
+    EXPECT_EQ(397ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+    janiModel = program.toJani();
+    model = builder.translate();
+    EXPECT_EQ(1728ul, model->getNumberOfStates());
+    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+}
+
+//TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
+//    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+//    
+//    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//    EXPECT_EQ(13ul, model->getNumberOfStates());
+//    EXPECT_EQ(20ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//    EXPECT_EQ(677ul, model->getNumberOfStates());
+//    EXPECT_EQ(867ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//    EXPECT_EQ(8607ul, model->getNumberOfStates());
+//    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//    EXPECT_EQ(273ul, model->getNumberOfStates());
+//    EXPECT_EQ(397ul, model->getNumberOfTransitions());
+//    
+//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>().translateProgram(program);
+//    EXPECT_EQ(1728ul, model->getNumberOfStates());
+//    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+//}