tempest/src/storm/builder/DdJaniModelBuilder.cpp

#include "storm/builder/DdJaniModelBuilder.h"

#include <sstream>

#include <boost/algorithm/string/join.hpp>

#include "storm/logic/Formulas.h"

#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/AutomatonComposition.h"
#include "storm/storage/jani/ParallelComposition.h"
#include "storm/storage/jani/CompositionInformationVisitor.h"

#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/adapters/AddExpressionAdapter.h"

#include "storm/storage/expressions/ExpressionManager.h"

#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/symbolic/Ctmc.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"

#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"

#include "storm/utility/macros.h"
#include "storm/utility/jani.h"
#include "storm/utility/dd.h"
#include "storm/utility/math.h"
#include "storm/exceptions/WrongFormatException.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/NotSupportedException.h"

namespace storm {
    namespace builder {
        
        template <storm::dd::DdType Type, typename ValueType>
        DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
            // Intentionally left empty.
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        DdJaniModelBuilder<Type, ValueType>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
            this->preserveFormula(formula);
            this->setTerminalStatesFromFormula(formula);
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
            if (formulas.empty()) {
                this->buildAllRewardModels = true;
            } else {
                for (auto const& formula : formulas) {
                    this->preserveFormula(*formula);
                }
                if (formulas.size() == 1) {
                    this->setTerminalStatesFromFormula(*formulas.front());
                }
            }
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        void DdJaniModelBuilder<Type, ValueType>::Options::preserveFormula(storm::logic::Formula const& formula) {
            // If we already had terminal states, we need to erase them.
            if (terminalStates) {
                terminalStates.reset();
            }
            if (negatedTerminalStates) {
                negatedTerminalStates.reset();
            }
            
            // If we are not required to build all reward models, we determine the reward models we need to build.
            if (!buildAllRewardModels) {
                std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
                rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
            }
            
            // Extract all the labels used in the formula.
            std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
            for (auto const& formula : atomicLabelFormulas) {
                addLabel(formula->getLabel());
            }
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        void DdJaniModelBuilder<Type, ValueType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
            if (formula.isAtomicExpressionFormula()) {
                terminalStates = formula.asAtomicExpressionFormula().getExpression();
            } else if (formula.isEventuallyFormula()) {
                storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula();
                if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) {
                    this->setTerminalStatesFromFormula(sub);
                }
            } else if (formula.isUntilFormula()) {
                storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
                if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
                    this->setTerminalStatesFromFormula(right);
                }
                storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
                if (left.isAtomicExpressionFormula()) {
                    negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
                }
            } else if (formula.isProbabilityOperatorFormula()) {
                storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
                if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
                    this->setTerminalStatesFromFormula(sub);
                }
            }
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        std::set<std::string> const& DdJaniModelBuilder<Type, ValueType>::Options::getRewardModelNames() const {
            return rewardModelsToBuild;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllRewardModelsSet() const {
            return buildAllRewardModels;
        }

        template <storm::dd::DdType Type, typename ValueType>
        bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllLabelsSet() const {
            return buildAllLabels;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        void DdJaniModelBuilder<Type, ValueType>::Options::addLabel(std::string const& labelName) {
            STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
            labelNames.insert(labelName);
        }

        template <storm::dd::DdType Type, typename ValueType>
        struct CompositionVariables {
            CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
            variableToRowMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()),
            rowExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToRowMetaVariableMap)),
            variableToColumnMetaVariableMap(std::make_shared<std::map<storm::expressions::Variable, storm::expressions::Variable>>()),
            columnExpressionAdapter(std::make_shared<storm::adapters::AddExpressionAdapter<Type>>(manager, variableToColumnMetaVariableMap)) {
                // 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::shared_ptr<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::shared_ptr<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 variables encoding their location.
            std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
            std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationDdVariableMap;
            
            // A mapping from action indices to the meta variables used to encode these actions.
            std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
            
            // The meta variables used to encode the remaining nondeterminism.
            std::vector<storm::expressions::Variable> localNondeterminismVariables;
            
            // The meta variable used to distinguish Markovian from probabilistic choices in Markov automata.
            storm::expressions::Variable markovNondeterminismVariable;
            storm::dd::Bdd<Type> markovMarker;
            
            // The meta variables used to encode the actions and nondeterminism.
            std::set<storm::expressions::Variable> allNondeterminismVariables;
            
            // DDs representing the identity for each variable.
            std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap;
            
            // DDs representing the ranges of each variable.
            std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> variableToRangeMap;
            
            // 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 DD representing the valid ranges of the global variables.
            storm::dd::Add<Type, ValueType> globalVariableRanges;
        };
        
        // 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, storm::jani::CompositionInformation const& actionInformation) : model(model), automata(), actionInformation(actionInformation) {
                // Intentionally left empty.
            }
            
            CompositionVariables<Type, ValueType> create() {
                // First, check whether every automaton appears exactly once in the system composition. Simultaneously,
                // we determine the set of non-silent actions used by the 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.");
                
                STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidArgumentException, "The symbolic JANI model builder currently does not support transient edge destination assignments.");
                
                // Then, check that the model does not contain non-transient unbounded integer or non-transient real variables.
                STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient global unbounded integer variables.");
                STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables.");
                for (auto const& automaton : this->model.getAutomata()) {
                    STORM_LOG_THROW(!automaton.getVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient unbounded integer variables in automaton '" << automaton.getName() << "'.");
                    STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient real 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 automaton '" << composition.getAutomatonName() << "' multiple times.");
                automata.insert(it, composition.getAutomatonName());
                return boost::none;
            }

            boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
                for (auto const& subcomposition : composition.getSubcompositions()) {
                    subcomposition->accept(*this, boost::none);
                }
                return boost::none;
            }
            
        private:
            CompositionVariables<Type, ValueType> createVariables() {
                CompositionVariables<Type, ValueType> result;
                
                for (auto const& nonSilentActionIndex : actionInformation.getNonSilentActionIndices()) {
                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(actionInformation.getActionName(nonSilentActionIndex));
                    result.actionVariablesMap[nonSilentActionIndex] = variablePair.first;
                    result.allNondeterminismVariables.insert(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.localNondeterminismVariables.push_back(variablePair.first);
                    result.allNondeterminismVariables.insert(variablePair.first);
                }
                
                if (this->model.getModelType() == storm::jani::ModelType::MA) {
                    result.markovNondeterminismVariable = result.manager->addMetaVariable("markov").first;
                    result.markovMarker = result.manager->getEncoding(result.markovNondeterminismVariable, 1);
                    result.allNondeterminismVariables.insert(result.markovNondeterminismVariable);
                }
                
                for (auto const& automaton : this->model.getAutomata()) {
                    // Start by creating a meta variable for the location of the automaton.
                    storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc");
                    result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable;
                    std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
                    result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair;
                    result.rowColumnMetaVariablePairs.push_back(variablePair);

                    result.variableToRowMetaVariableMap->emplace(locationExpressionVariable, variablePair.first);
                    result.variableToColumnMetaVariableMap->emplace(locationExpressionVariable, variablePair.second);
                    
                    // Add the location variable to the row/column variables.
                    result.rowMetaVariables.insert(variablePair.first);
                    result.columnMetaVariables.insert(variablePair.second);
                    
                    // Add the legal range for the location variables.
                    result.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
                    result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));
                }
                
                // Create global variables.
                storm::dd::Bdd<Type> globalVariableRanges = result.manager->getBddOne();
                for (auto const& variable : this->model.getGlobalVariables()) {
                    // Only create the variable if it's non-transient.
                    if (variable.isTransient()) {
                        continue;
                    }
                    
                    createVariable(variable, result);
                    globalVariableRanges &= result.manager->getRange(result.variableToRowMetaVariableMap->at(variable.getExpressionVariable()));
                }
                result.globalVariableRanges = globalVariableRanges.template toAdd<ValueType>();
                
                // 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();
                    
                    // Add the identity and ranges of the location variables to the ones of the automaton.
                    std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()];
                    storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
                    identity &= variableIdentity.toBdd();
                    range &= result.manager->getRange(locationVariables.first);
                    
                    // Then create variables for the variables of the automaton.
                    for (auto const& variable : automaton.getVariables()) {
                        // Only create the variable if it's non-transient.
                        if (variable.isTransient()) {
                            continue;
                        }
                        
                        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 && globalVariableRanges).template toAdd<ValueType>();
                }
                
                return result;
            }
            
            void createVariable(storm::jani::Variable const& variable, CompositionVariables<Type, ValueType>& result) {
                if (variable.isBooleanVariable()) {
                    createVariable(variable.asBooleanVariable(), result);
                } else if (variable.isBoundedIntegerVariable()) {
                    createVariable(variable.asBoundedIntegerVariable(), result);
                } else {
                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid type of variable in JANI model.");
                }
            }
            
            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.getExpressionVariable().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.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
                result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));
                
                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.getExpressionVariable().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.variableToRangeMap.emplace(variablePair.first, result.manager->getRange(variablePair.first));
                result.variableToRangeMap.emplace(variablePair.second, result.manager->getRange(variablePair.second));
                
                result.rowColumnMetaVariablePairs.push_back(variablePair);
                result.allGlobalVariables.insert(variable.getExpressionVariable());
            }
            
            storm::jani::Model const& model;
            std::set<std::string> automata;
            storm::jani::CompositionInformation actionInformation;
        };
        
        template <storm::dd::DdType Type, typename ValueType>
        struct ComposerResult {
            ComposerResult(storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientLocationAssignments, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, storm::dd::Bdd<Type> const& illegalFragment, uint64_t numberOfNondeterminismVariables = 0) : transitions(transitions), transientLocationAssignments(transientLocationAssignments), transientEdgeAssignments(transientEdgeAssignments), illegalFragment(illegalFragment), numberOfNondeterminismVariables(numberOfNondeterminismVariables) {
                // Intentionally left empty.
            }
            
            storm::dd::Add<Type, ValueType> transitions;
            std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientLocationAssignments;
            std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
            storm::dd::Bdd<Type> illegalFragment;
            uint64_t numberOfNondeterminismVariables;
        };
        
        // A class that is responsible for performing the actual composition. This
        template <storm::dd::DdType Type, typename ValueType>
        class SystemComposer : public storm::jani::CompositionVisitor {
        public:
            SystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : model(model), variables(variables), transientVariables(transientVariables) {
                // Intentionally left empty.
            }
            
            virtual ComposerResult<Type, ValueType> compose() = 0;

        protected:
            // 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;
            
            // The transient variables to consider during system composition.
            std::vector<storm::expressions::Variable> transientVariables;
        };

        // This structure represents an edge destination.
        template <storm::dd::DdType Type, typename ValueType>
        struct EdgeDestinationDd {
            EdgeDestinationDd(storm::dd::Add<Type, ValueType> const& transitions, std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}) : transitions(transitions), writtenGlobalVariables(writtenGlobalVariables) {
                // Intentionally left empty.
            }
            
            storm::dd::Add<Type, ValueType> transitions;
            std::set<storm::expressions::Variable> writtenGlobalVariables;
        };
        
        template <storm::dd::DdType Type, typename ValueType>
        EdgeDestinationDd<Type, ValueType> buildEdgeDestinationDd(storm::jani::Automaton const& automaton, storm::jani::EdgeDestination const& destination, storm::dd::Add<Type, ValueType> const& guard, CompositionVariables<Type, ValueType> const& variables) {
            storm::dd::Add<Type, ValueType> transitions = variables.rowExpressionAdapter->translateExpression(destination.getProbability());
            
            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.getOrderedAssignments().getNonTransientAssignments()) {
                // 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> assignedExpression = variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
                
                // Combine the assigned expression with the guard.
                storm::dd::Add<Type, ValueType> result = assignedExpression * 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.variableToRangeMap.at(primedMetaVariable).template toAdd<ValueType>();
                
                // Combine the assignment DDs.
                transitions *= 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());
                    transitions *= 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());
                    transitions *= variables.variableToIdentityMap.at(variable.getExpressionVariable());
                }
            }
            
            transitions *= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
            
            return EdgeDestinationDd<Type, ValueType>(transitions, assignedGlobalVariables);
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        storm::dd::Add<Type, ValueType> encodeAction(boost::optional<uint64_t> const& actionIndex, CompositionVariables<Type, ValueType> const& variables) {
            storm::dd::Add<Type, ValueType> encoding = variables.manager->template getAddOne<ValueType>();
            
            for (auto it = variables.actionVariablesMap.rbegin(), ite = variables.actionVariablesMap.rend(); it != ite; ++it) {
                if (actionIndex && it->first == actionIndex.get()) {
                    encoding *= variables.manager->getEncoding(it->second, 1).template toAdd<ValueType>();
                } else {
                    encoding *= variables.manager->getEncoding(it->second, 0).template toAdd<ValueType>();
                }
            }
            
            return encoding;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        storm::dd::Add<Type, ValueType> encodeIndex(uint64_t index, uint64_t localNondeterminismVariableOffset, uint64_t numberOfLocalNondeterminismVariables, CompositionVariables<Type, ValueType> const& variables) {
            storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
            
            std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap;
            for (uint_fast64_t i = 0; i < numberOfLocalNondeterminismVariables; ++i) {
                if (index & (1ull << (numberOfLocalNondeterminismVariables - i - 1))) {
                    metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 1);
                } else {
                    metaVariableNameToValueMap.emplace(variables.localNondeterminismVariables[localNondeterminismVariableOffset + i], 0);
                }
            }
            
            result.setValue(metaVariableNameToValueMap, 1);
            return result;
        }
                
        template <storm::dd::DdType Type, typename ValueType>
        class CombinedEdgesSystemComposer : public SystemComposer<Type, ValueType> {
        public:
            // This structure represents an edge.
            struct EdgeDd {
                EdgeDd(bool isMarkovian, storm::dd::Add<Type> const& guard, storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, std::set<storm::expressions::Variable> const& writtenGlobalVariables) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment() {
                    
                    // Convert the set of written variables to a mapping from variable to the writing fragments.
                    for (auto const& variable : writtenGlobalVariables) {
                        variableToWritingFragment[variable] = guard.toBdd();
                    }
                }

                EdgeDd(bool isMarkovian, storm::dd::Add<Type> const& guard, storm::dd::Add<Type, ValueType> const& transitions, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment) : isMarkovian(isMarkovian), guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), variableToWritingFragment(variableToWritingFragment) {
                    // Intentionally left empty.
                }

                // A flag storing whether this edge is a Markovian one (i.e. one with a rate).
                bool isMarkovian;
                
                // A DD that represents all states that have this edge enabled.
                storm::dd::Add<Type, ValueType> guard;
                
                // A DD that represents the transitions of this edge.
                storm::dd::Add<Type, ValueType> transitions;
                
                // A mapping from transient variables to the DDs representing their value assignments.
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                
                // A mapping of variables to the variables to the fragment of transitions that is writing the corresponding variable.
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> variableToWritingFragment;
            };
            
            // This structure represents an edge.
            struct ActionDd {
                ActionDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientEdgeAssignments = {}, std::pair<uint64_t, uint64_t> localNondeterminismVariables = std::pair<uint64_t, uint64_t>(0, 0), std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& variableToWritingFragment = {}, storm::dd::Bdd<Type> const& illegalFragment = storm::dd::Bdd<Type>()) : guard(guard), transitions(transitions), transientEdgeAssignments(transientEdgeAssignments), localNondeterminismVariables(localNondeterminismVariables), variableToWritingFragment(variableToWritingFragment), illegalFragment(illegalFragment), inputEnabled(false) {
                    // Intentionally left empty.
                }
                
                uint64_t getLowestLocalNondeterminismVariable() const {
                    return localNondeterminismVariables.first;
                }

                uint64_t getHighestLocalNondeterminismVariable() const {
                    return localNondeterminismVariables.second;
                }
                
                std::pair<uint64_t, uint64_t> const& getLocalNondeterminismVariables() const {
                    return localNondeterminismVariables;
                }
                
                ActionDd multiplyTransitions(storm::dd::Add<Type, ValueType> const& factor) const {
                    return ActionDd(guard, transitions * factor, transientEdgeAssignments, localNondeterminismVariables, variableToWritingFragment, illegalFragment);
                }

                bool isInputEnabled() const {
                    return inputEnabled;
                }
                
                void setIsInputEnabled() {
                    inputEnabled = true;
                }
                
                // A DD that represents all states that have this edge enabled.
                storm::dd::Add<Type, ValueType> guard;
                
                // A DD that represents the transitions of this edge.
                storm::dd::Add<Type, ValueType> transitions;
                
                // A mapping from transient variables to their assignments.
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                
                // The local nondeterminism variables used by this action DD, given as the lowest
                std::pair<uint64_t, uint64_t> localNondeterminismVariables;
                
                // A mapping from global variables to a DD that characterizes choices (nondeterminism variables) in
                // states that write to this global variable.
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> variableToWritingFragment;
                
                // A DD characterizing the fragment of the states satisfying the guard that are illegal because
                // there are synchronizing edges enabled that write to the same global variable.
                storm::dd::Bdd<Type> illegalFragment;
                
                // A flag storing whether this action is input-enabled.
                bool inputEnabled;
            };
            
            // This structure represents a subcomponent of a composition.
            struct AutomatonDd {
                AutomatonDd(storm::dd::Add<Type, ValueType> const& identity, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientLocationAssignments = {}) : actionIndexToAction(), transientLocationAssignments(transientLocationAssignments), identity(identity), localNondeterminismVariables(std::make_pair<uint64_t, uint64_t>(0, 0)) {
                    // Intentionally left empty.
                }
                
                uint64_t getLowestLocalNondeterminismVariable() const {
                    return localNondeterminismVariables.first;
                }

                void setLowestLocalNondeterminismVariable(uint64_t newValue) {
                    localNondeterminismVariables.first = newValue;
                }
                
                uint64_t getHighestLocalNondeterminismVariable() const {
                    return localNondeterminismVariables.second;
                }

                void setHighestLocalNondeterminismVariable(uint64_t newValue) {
                    localNondeterminismVariables.second = newValue;
                }
                
                void extendLocalNondeterminismVariables(std::pair<uint64_t, uint64_t> const& localNondeterminismVariables) {
                    setLowestLocalNondeterminismVariable(std::min(localNondeterminismVariables.first, getLowestLocalNondeterminismVariable()));
                    setHighestLocalNondeterminismVariable(std::max(localNondeterminismVariables.second, getHighestLocalNondeterminismVariable()));
                }
                
                // A mapping from action indices to the action DDs.
                std::map<uint64_t, ActionDd> actionIndexToAction;
                
                // A mapping from transient variables to their location-based transient assignment values.
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientLocationAssignments;
                
                // The identity of the automaton's variables.
                storm::dd::Add<Type, ValueType> identity;
                
                // The local nondeterminism variables used by this action DD, given as the lowest and highest variable index.
                std::pair<uint64_t, uint64_t> localNondeterminismVariables;

            };
            
            CombinedEdgesSystemComposer(storm::jani::Model const& model, storm::jani::CompositionInformation const& actionInformation, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionInformation(actionInformation) {
                // Intentionally left empty.
            }
        
            storm::jani::CompositionInformation const& actionInformation;

            ComposerResult<Type, ValueType> compose() override {
                std::map<uint64_t, uint64_t> actionIndexToLocalNondeterminismVariableOffset;
                for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
                    actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
                }
                actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::SILENT_ACTION_INDEX] = 0;

                AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
                return buildSystemFromAutomaton(globalAutomaton);
            }
            
            boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
                std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint_fast64_t, uint_fast64_t> const&>(data);
                
                std::set<uint64_t> inputEnabledActionIndices;
                for (auto const& actionName : composition.getInputEnabledActions()) {
                    inputEnabledActionIndices.insert(actionInformation.getActionIndex(actionName));
                }
                
                return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset, inputEnabledActionIndices);
            }
            
            boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
                std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint64_t, uint64_t> const&>(data);
                
                std::vector<AutomatonDd> subautomata;
                for (uint64_t subcompositionIndex = 0; subcompositionIndex < composition.getNumberOfSubcompositions(); ++subcompositionIndex) {
                    // Prepare the new offset mapping.
                    std::map<uint64_t, uint64_t> newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset;
                    
                    if (subcompositionIndex == 0) {
                        for (auto const& synchVector : composition.getSynchronizationVectors()) {
                            auto it = actionIndexToLocalNondeterminismVariableOffset.find(actionInformation.getActionIndex(synchVector.getOutput()));
                            STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action " << synchVector.getOutput() << ".");
                            if (synchVector.getInput(0) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) {
                                newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(0))] = it->second;
                            }
                        }
                    } else {
                        // Based on the previous results, we need to update the offsets.
                        for (auto const& synchVector : composition.getSynchronizationVectors()) {
                            if (synchVector.getInput(subcompositionIndex) != storm::jani::SynchronizationVector::NO_ACTION_INPUT) {
                                boost::optional<uint64_t> previousActionPosition = synchVector.getPositionOfPrecedingParticipatingAction(subcompositionIndex);
                                if (previousActionPosition) {
                                    AutomatonDd const& previousAutomatonDd = subautomata[previousActionPosition.get()];

                                    std::string const& previousAction = synchVector.getInput(previousActionPosition.get());
                                    auto it = previousAutomatonDd.actionIndexToAction.find(actionInformation.getActionIndex(previousAction));
                                    if (it != previousAutomatonDd.actionIndexToAction.end()) {
                                        newSynchronizingActionToOffsetMap[actionInformation.getActionIndex(synchVector.getInput(subcompositionIndex))] = it->second.getHighestLocalNondeterminismVariable();
                                    } else {
                                        STORM_LOG_ASSERT(false, "Subcomposition does not have action that is mentioned in parallel composition.");
                                    }
                                }
                            }
                        }
                    }
                    
                    // Build the DD for the next element of the composition wrt. to the current offset mapping.
                    subautomata.push_back(boost::any_cast<AutomatonDd>(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap)));
                }
                
                return composeInParallel(subautomata, composition.getSynchronizationVectors());
            }
            
        private:
            AutomatonDd composeInParallel(std::vector<AutomatonDd> const& subautomata, std::vector<storm::jani::SynchronizationVector> const& synchronizationVectors) {
                typedef storm::dd::Add<Type, ValueType> IdentityAdd;
                typedef std::pair<ActionDd, IdentityAdd> ActionAndAutomatonIdentity;
                typedef std::vector<ActionAndAutomatonIdentity> ActionAndAutomatonIdentities;
                typedef std::vector<boost::optional<std::pair<ActionAndAutomatonIdentities, IdentityAdd>>> SynchronizationVectorActionsAndIdentities;
                
                AutomatonDd result(this->variables.manager->template getAddOne<ValueType>());
                
                std::map<uint64_t, std::vector<ActionDd>> nonSynchronizingActions;
                SynchronizationVectorActionsAndIdentities synchronizationVectorActions(synchronizationVectors.size(), boost::none);
                for (uint64_t automatonIndex = 0; automatonIndex < subautomata.size(); ++automatonIndex) {
                    AutomatonDd const& subautomaton = subautomata[automatonIndex];
                    
                    // Add the transient assignments from the new subautomaton.
                    addToTransientAssignmentMap(result.transientLocationAssignments, subautomaton.transientLocationAssignments);
                    
                    // Initilize the used local nondeterminism variables appropriately.
                    if (automatonIndex == 0) {
                        result.setLowestLocalNondeterminismVariable(subautomaton.getLowestLocalNondeterminismVariable());
                        result.setHighestLocalNondeterminismVariable(subautomaton.getHighestLocalNondeterminismVariable());
                    }

                    // Compose the actions according to the synchronization vectors.
                    std::set<uint64_t> actionsInSynch;
                    for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) {
                        auto const& synchVector = synchronizationVectors[synchVectorIndex];
                        
                        if (synchVector.isNoActionInput(synchVector.getInput(automatonIndex))) {
                            if (automatonIndex == 0) {
                                // Create a new action that is the identity over the first automaton.
                                synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(ActionDd(this->variables.manager->template getAddOne<ValueType>(), subautomaton.identity, {}, subautomaton.localNondeterminismVariables, {}, this->variables.manager->getBddZero()), subautomaton.identity)}, this->variables.manager->template getAddOne<ValueType>());
                            } else {
                                // If there is no action in the output spot, this means that some other subcomposition did
                                // not provide the action necessary for the synchronization vector to resolve.
                                if (synchronizationVectorActions[synchVectorIndex]) {
                                    synchronizationVectorActions[synchVectorIndex].get().second *= subautomaton.identity;
                                }
                            }
                        } else {
                            // Determine the indices of input (at the current automaton position) and the output.
                            uint64_t inputActionIndex = actionInformation.getActionIndex(synchVector.getInput(automatonIndex));
                            actionsInSynch.insert(inputActionIndex);
                            
                            // Either set the action (if it's the first of the ones to compose) or compose the actions directly.
                            if (automatonIndex == 0) {
                                // If the action cannot be found, the particular spot in the output will be left empty.
                                auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
                                if (inputActionIt != subautomaton.actionIndexToAction.end()) {
                                    synchronizationVectorActions[synchVectorIndex] = std::make_pair(ActionAndAutomatonIdentities{std::make_pair(inputActionIt->second, subautomaton.identity)}, this->variables.manager->template getAddOne<ValueType>());
                                }
                            } else {
                                // If there is no action in the output spot, this means that some other subcomposition did
                                // not provide the action necessary for the synchronization vector to resolve.
                                if (synchronizationVectorActions[synchVectorIndex]) {
                                    auto inputActionIt = subautomaton.actionIndexToAction.find(inputActionIndex);
                                    if (inputActionIt != subautomaton.actionIndexToAction.end()) {
                                        synchronizationVectorActions[synchVectorIndex].get().first.push_back(std::make_pair(inputActionIt->second, subautomaton.identity));
                                    } else {
                                        // If the current subcomposition does not provide the required action for the synchronization
                                        // vector, we clear the action.
                                        synchronizationVectorActions[synchVectorIndex] = boost::none;
                                    }
                                }
                            }
                        }
                    }

                    // Now treat all unsynchronizing actions.
                    if (automatonIndex == 0) {
                        // Since it's the first automaton, there is nothing to combine.
                        for (auto const& action : subautomaton.actionIndexToAction) {
                            if (actionsInSynch.find(action.first) == actionsInSynch.end()) {
                                nonSynchronizingActions[action.first].push_back(action.second);
                            }
                        }
                    } else {
                        // Extend all other non-synchronizing actions with the identity of the current subautomaton.
                        for (auto& actions : nonSynchronizingActions) {
                            for (auto& action : actions.second) {
                                STORM_LOG_TRACE("Extending action '" << actionInformation.getActionName(actions.first) << "' with identity of next composition.");
                                action.transitions *= subautomaton.identity;
                            }
                        }
                        
                        // Extend the actions of the current subautomaton with the identity of the previous system and
                        // add it to the overall non-synchronizing action result.
                        for (auto const& action : subautomaton.actionIndexToAction) {
                            if (actionsInSynch.find(action.first) == actionsInSynch.end()) {
                                STORM_LOG_TRACE("Adding action " << actionInformation.getActionName(action.first) << " to non-synchronizing actions and multiply it with system identity.");
                                nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity));
                            }
                        }
                    }
                    
                    // Finally, construct combined identity.
                    result.identity *= subautomaton.identity;
                }
                
                // Add the results of the synchronization vectors to that of the non-synchronizing actions.
                for (uint64_t synchVectorIndex = 0; synchVectorIndex < synchronizationVectors.size(); ++synchVectorIndex) {
                    auto const& synchVector = synchronizationVectors[synchVectorIndex];
                    
                    // If there is an action resulting from this combination of actions, add it to the output action.
                    if (synchronizationVectorActions[synchVectorIndex]) {
                        uint64_t outputActionIndex = actionInformation.getActionIndex(synchVector.getOutput());
                        nonSynchronizingActions[outputActionIndex].push_back(combineSynchronizingActions(synchronizationVectorActions[synchVectorIndex].get().first, synchronizationVectorActions[synchVectorIndex].get().second));
                    }
                }
                
                // Now that we have built the individual action DDs for all resulting actions, we need to combine them
                // in an unsynchronizing way.
                for (auto const& nonSynchronizingActionDds : nonSynchronizingActions) {
                    std::vector<ActionDd> const& actionDds = nonSynchronizingActionDds.second;
                    if (actionDds.size() > 1) {
                        ActionDd combinedAction = combineUnsynchronizedActions(actionDds);
                        result.actionIndexToAction[nonSynchronizingActionDds.first] = combinedAction;
                        result.extendLocalNondeterminismVariables(combinedAction.getLocalNondeterminismVariables());
                    } else {
                        result.actionIndexToAction[nonSynchronizingActionDds.first] = actionDds.front();
                        result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables());
                    }
                }
                
                return result;
            }
            
            ActionDd combineSynchronizingActions(std::vector<std::pair<ActionDd, storm::dd::Add<Type, ValueType>>> const& actionsAndIdentities, storm::dd::Add<Type, ValueType> const& nonSynchronizingAutomataIdentities) {
                // If there is just one action, no need to combine anything.
                if (actionsAndIdentities.size() == 1) {
                    return actionsAndIdentities.front().first;
                }
                
                // If there are only input-enabled actions, we also need to build the disjunction of the guards.
                bool allActionsInputEnabled = true;
                for (auto const& actionIdentityPair : actionsAndIdentities) {
                    auto const& action = actionIdentityPair.first;
                    if (!action.isInputEnabled()) {
                        allActionsInputEnabled = false;
                    }
                }
                
                boost::optional<storm::dd::Bdd<Type>> guardDisjunction;
                if (allActionsInputEnabled) {
                    guardDisjunction = this->variables.manager->getBddZero();
                }
                
                // Otherwise, construct the synchronization.
                storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
                
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragment;
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragmentWithoutNondeterminism;
                
                storm::dd::Bdd<Type> inputEnabledGuard = this->variables.manager->getBddOne();
                storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddOne<ValueType>();
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                
                uint64_t lowestNondeterminismVariable = actionsAndIdentities.front().first.getLowestLocalNondeterminismVariable();
                uint64_t highestNondeterminismVariable = actionsAndIdentities.front().first.getHighestLocalNondeterminismVariable();
                
                storm::dd::Bdd<Type> newIllegalFragment = this->variables.manager->getBddZero();
                for (auto const& actionIdentityPair : actionsAndIdentities) {
                    auto const& action = actionIdentityPair.first;
                    storm::dd::Bdd<Type> actionGuard = action.guard.toBdd();
                    if (guardDisjunction) {
                        guardDisjunction.get() |= actionGuard;
                    }
                    
                    lowestNondeterminismVariable = std::min(lowestNondeterminismVariable, action.getLowestLocalNondeterminismVariable());
                    highestNondeterminismVariable = std::max(highestNondeterminismVariable, action.getHighestLocalNondeterminismVariable());
                    transientEdgeAssignments = joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments);
                    
                    if (action.isInputEnabled()) {
                        // If the action is input-enabled, we add self-loops to all states.
                        transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second);
                    } else {
                        transitions *= action.transitions;
                    }
                    
                    // Create a set of variables that is used as nondeterminism variables in this action.
                    auto nondetVariables = std::set<storm::expressions::Variable>(this->variables.localNondeterminismVariables.begin() + action.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action.getHighestLocalNondeterminismVariable());
                    
                    for (auto const& entry : action.variableToWritingFragment) {
                        storm::dd::Bdd<Type> guardedWritingFragment = inputEnabledGuard && entry.second;
                        
                        // Check whether there already is an entry for this variable in the mapping of global variables
                        // to their writing fragments.
                        auto globalFragmentIt = globalVariableToWritingFragment.find(entry.first);
                        if (globalFragmentIt != globalVariableToWritingFragment.end()) {
                            // If there is, take the conjunction of the entries and also of their versions without nondeterminism
                            // variables.
                            globalFragmentIt->second &= guardedWritingFragment;
                            illegalFragment |= globalVariableToWritingFragmentWithoutNondeterminism[entry.first] && guardedWritingFragment.existsAbstract(nondetVariables);
                            globalVariableToWritingFragmentWithoutNondeterminism[entry.first] |= guardedWritingFragment.existsAbstract(nondetVariables);
                        } else {
                            // If not, create the entry and also create a version of the entry that abstracts from the
                            // used nondeterminism variables.
                            globalVariableToWritingFragment[entry.first] = guardedWritingFragment;
                            globalVariableToWritingFragmentWithoutNondeterminism[entry.first] = guardedWritingFragment.existsAbstract(nondetVariables);
                        }
                        
                        // Join all individual illegal fragments so we can see whether any of these elements lie in the
                        // conjunction of all guards.
                        illegalFragment |= action.illegalFragment;
                    }
                    
                    // Now go through all fragments that are not written by the current action and join them with the
                    // guard of the current action if the current action is not input enabled.
                    for (auto& entry : globalVariableToWritingFragment) {
                        if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end() && !action.isInputEnabled()) {
                            entry.second &= actionGuard;
                        }
                    }
                    
                    if (!action.isInputEnabled()) {
                        inputEnabledGuard &= actionGuard;
                    }
                }
                
                // If all actions were input-enabled, we need to constrain the transitions with the disjunction of all
                // guards to make sure there are not transitions resulting from input enabledness alone.
                if (allActionsInputEnabled) {
                    inputEnabledGuard &= guardDisjunction.get();
                    transitions *= guardDisjunction.get().template toAdd<ValueType>();
                }
                
                // Cut the union of the illegal fragments to the conjunction of the guards since only these states have
                // such a combined transition.
                illegalFragment &= inputEnabledGuard;
                
                return ActionDd(inputEnabledGuard.template toAdd<ValueType>(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
            }
            
            ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add<Type, ValueType> const& identity1, storm::dd::Add<Type, ValueType> const& identity2) {
                // First extend the action DDs by the other identities.
                STORM_LOG_TRACE("Multiplying identities to combine unsynchronized actions.");
                action1.transitions = action1.transitions * identity2;
                action2.transitions = action2.transitions * identity1;
                
                // Then combine the extended action DDs.
                return combineUnsynchronizedActions(action1, action2);
            }
            
            ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2) {
                return combineUnsynchronizedActions({action1, action2});
            }

            ActionDd combineUnsynchronizedActions(std::vector<ActionDd> actions) {
                STORM_LOG_TRACE("Combining unsynchronized actions.");
                
                if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
                    auto actionIt = actions.begin();
                    ActionDd result(*actionIt);
                    
                    for (++actionIt; actionIt != actions.end(); ++actionIt) {
                        result = ActionDd(result.guard + actionIt->guard, result.transitions + actionIt->transitions, joinTransientAssignmentMaps(result.transientEdgeAssignments, actionIt->transientEdgeAssignments), std::make_pair<uint64_t, uint64_t>(0, 0), joinVariableWritingFragmentMaps(result.variableToWritingFragment, actionIt->variableToWritingFragment), result.illegalFragment || actionIt->illegalFragment);
                    }
                    return result;
                } else if (this->model.getModelType() == storm::jani::ModelType::MDP) {
                    // Ensure that all actions start at the same local nondeterminism variable.
                    uint_fast64_t lowestLocalNondeterminismVariable = actions.front().getLowestLocalNondeterminismVariable();
                    uint_fast64_t highestLocalNondeterminismVariable = actions.front().getHighestLocalNondeterminismVariable();
                    for (auto const& action : actions) {
                        STORM_LOG_ASSERT(action.getLowestLocalNondeterminismVariable() == lowestLocalNondeterminismVariable, "Mismatching lowest nondeterminism variable indices.");
                        highestLocalNondeterminismVariable = std::max(highestLocalNondeterminismVariable, action.getHighestLocalNondeterminismVariable());
                    }
                    
                    // Bring all actions to the same number of variables that encode the nondeterminism.
                    for (auto& action : actions) {
                        storm::dd::Bdd<Type> nondeterminismEncodingBdd = this->variables.manager->getBddOne();
                        for (uint_fast64_t i = action.getHighestLocalNondeterminismVariable(); i < highestLocalNondeterminismVariable; ++i) {
                            nondeterminismEncodingBdd &= this->variables.manager->getEncoding(this->variables.localNondeterminismVariables[i], 0);
                        }
                        storm::dd::Add<Type, ValueType> nondeterminismEncoding = nondeterminismEncodingBdd.template toAdd<ValueType>();

                        action.transitions *= nondeterminismEncoding;
                        
                        for (auto& variableFragment : action.variableToWritingFragment) {
                            variableFragment.second &= nondeterminismEncodingBdd;
                        }
                        for (auto& transientAssignment : action.transientEdgeAssignments) {
                            transientAssignment.second *= nondeterminismEncoding;
                        }
                    }
                    
                    uint64_t numberOfLocalNondeterminismVariables = static_cast<uint64_t>(std::ceil(std::log2(actions.size())));
                    storm::dd::Bdd<Type> guard = this->variables.manager->getBddZero();
                    storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
                    std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                    std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> variableToWritingFragment;
                    storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();

                    for (uint64_t actionIndex = 0; actionIndex < actions.size(); ++actionIndex) {
                        ActionDd& action = actions[actionIndex];

                        guard |= action.guard.toBdd();

                        storm::dd::Add<Type, ValueType> nondeterminismEncoding = encodeIndex(actionIndex, highestLocalNondeterminismVariable, numberOfLocalNondeterminismVariables, this->variables);
                        transitions += nondeterminismEncoding * action.transitions;
                        
                        joinTransientAssignmentMaps(transientEdgeAssignments, action.transientEdgeAssignments);
                        
                        storm::dd::Bdd<Type> nondeterminismEncodingBdd = nondeterminismEncoding.toBdd();
                        for (auto& entry : action.variableToWritingFragment) {
                            entry.second &= nondeterminismEncodingBdd;
                        }
                        addToVariableWritingFragmentMap(variableToWritingFragment, action.variableToWritingFragment);
                        illegalFragment |= action.illegalFragment;
                    }
                    
                    return ActionDd(guard.template toAdd<ValueType>(), transitions, transientEdgeAssignments, std::make_pair(lowestLocalNondeterminismVariable, highestLocalNondeterminismVariable + numberOfLocalNondeterminismVariables), variableToWritingFragment, illegalFragment);
                } else {
                    STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type.");
                }
            }
            
            void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function<void (storm::jani::Assignment const&)> const& callback) {
                auto transientVariableIt = this->transientVariables.begin();
                auto transientVariableIte = this->transientVariables.end();
                for (auto const& assignment : transientAssignments) {
                    while (transientVariableIt != transientVariableIte && *transientVariableIt < assignment.getExpressionVariable()) {
                        ++transientVariableIt;
                    }
                    if (transientVariableIt == transientVariableIte) {
                        break;
                    }
                    if (*transientVariableIt == assignment.getExpressionVariable()) {
                        callback(assignment);
                        ++transientVariableIt;
                    }
                }
            }
            
            EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) {
                STORM_LOG_TRACE("Translating guard " << edge.getGuard());
                
                // We keep the guard and a "ranged" version seperate, because building the destinations tends to be
                // slower when the full range is applied.
                storm::dd::Add<Type, ValueType> guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());
                storm::dd::Add<Type, ValueType> rangedGuard = guard * this->variables.automatonToRangeMap.at(automaton.getName());
                STORM_LOG_WARN_COND(!rangedGuard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
                
                if (!rangedGuard.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, this->variables));
                        
                        STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect.");
                    }
                    
                    // Now that we have built the destinations, we always take the full guard.
                    guard = rangedGuard;
                    
                    // Start by gathering all variables that were written in at least one destination.
                    std::set<storm::expressions::Variable> globalVariablesInSomeDestination;
                    
                    // 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.getActionIndex() != storm::jani::Model::SILENT_ACTION_INDEX) {
                        for (auto const& edgeDestinationDd : destinationDds) {
                            globalVariablesInSomeDestination.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
                        }
                    } else {
                        globalVariablesInSomeDestination = this->variables.allGlobalVariables;
                    }
                    
                    // Then, multiply the missing identities.
                    for (auto& destinationDd : destinationDds) {
                        std::set<storm::expressions::Variable> missingIdentities;
                        std::set_difference(globalVariablesInSomeDestination.begin(), globalVariablesInSomeDestination.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.transitions *= this->variables.variableToIdentityMap.at(variable);
                        }
                    }
                    
                    // Now combine the destination DDs to the edge DD.
                    storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
                    for (auto const& destinationDd : destinationDds) {
                        transitions += destinationDd.transitions;
                    }
                    
                    // Add the source location and the guard.
                    storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
                    transitions *= sourceLocationAndGuard;
                    
                    // If we multiply the ranges of global variables, make sure everything stays within its bounds.
                    if (!globalVariablesInSomeDestination.empty()) {
                        transitions *= this->variables.globalVariableRanges;
                    }
                    
                    // If the edge has a rate, we multiply it to the DD.
                    bool isMarkovian = false;
                    if (edge.hasRate()) {
                        transitions *=  this->variables.rowExpressionAdapter->translateExpression(edge.getRate());
                        isMarkovian = true;
                    }
                    
                    // Finally treat the transient assignments.
                    std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                    if (!this->transientVariables.empty()) {
                        performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) {
                            transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
                        } );
                    }
                    
                    return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
                } else {
                    return EdgeDd(false, rangedGuard, rangedGuard, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>(), std::set<storm::expressions::Variable>());
                }
            }
            
            EdgeDd combineMarkovianEdgesToSingleEdge(std::vector<EdgeDd> const& edgeDds) {
                storm::dd::Bdd<Type> guard = this->variables.manager->getBddZero();
                storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> variableToWritingFragment;

                bool overlappingGuards = false;
                for (auto const& edge : edgeDds) {
                    STORM_LOG_THROW(edge.isMarkovian, storm::exceptions::InvalidArgumentException, "Can only combine Markovian edges.");
                    
                    if (!overlappingGuards) {
                        overlappingGuards |= !(guard && edge.guard.toBdd()).isZero();
                    }
                    
                    guard |= edge.guard.toBdd();
                    transitions += edge.transitions;
                    variableToWritingFragment = joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment);
                    joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments);
                }

                // Currently, we can only combine the transient edge assignments if there is no overlap of the guards of the edges.
                STORM_LOG_THROW(!overlappingGuards || transientEdgeAssignments.empty(), storm::exceptions::NotSupportedException, "Cannot have transient edge assignments when combining Markovian edges with overlapping guards.");
                
                return EdgeDd(true, guard.template toAdd<ValueType>(), transitions, transientEdgeAssignments, variableToWritingFragment);
            }
            
            ActionDd buildActionDdForActionIndex(storm::jani::Automaton const& automaton, uint64_t actionIndex, uint64_t localNondeterminismVariableOffset) {
                // Translate the individual edges.
                std::vector<EdgeDd> markovianEdges;
                std::vector<EdgeDd> nonMarkovianEdges;
                uint64_t numberOfEdges = 0;
                for (auto const& edge : automaton.getEdges()) {
                    ++numberOfEdges;
                    if (edge.getActionIndex() == actionIndex) {
                        EdgeDd result = buildEdgeDd(automaton, edge);
                        if (result.isMarkovian) {
                            markovianEdges.push_back(result);
                        } else {
                            nonMarkovianEdges.push_back(result);
                        }
                    }
                }
                
                // Now combine the edges to a single action.
                if (numberOfEdges > 0) {
                    storm::jani::ModelType modelType = this->model.getModelType();
                    if (modelType == storm::jani::ModelType::DTMC) {
                        STORM_LOG_THROW(markovianEdges.empty(), storm::exceptions::WrongFormatException, "Illegal Markovian edges in DTMC.");
                        return combineEdgesToActionDeterministic(nonMarkovianEdges);
                    } else if (modelType == storm::jani::ModelType::CTMC) {
                        STORM_LOG_THROW(nonMarkovianEdges.empty(), storm::exceptions::WrongFormatException, "Illegal non-Markovian edges in CTMC.");
                        return combineEdgesToActionDeterministic(markovianEdges);
                    } else if (modelType == storm::jani::ModelType::MDP) {
                        STORM_LOG_THROW(markovianEdges.empty(), storm::exceptions::WrongFormatException, "Illegal Markovian edges in MDP.");
                        return combineEdgesToActionNondeterministic(nonMarkovianEdges, boost::none, localNondeterminismVariableOffset);
                    } else if (modelType == storm::jani::ModelType::MA) {
                        boost::optional<EdgeDd> markovianEdge = boost::none;
                        if (markovianEdges.size() > 1) {
                            markovianEdge = combineMarkovianEdgesToSingleEdge(markovianEdges);
                        } else if (markovianEdges.size() == 1) {
                            markovianEdge = markovianEdges.front();
                        }
                        return combineEdgesToActionNondeterministic(nonMarkovianEdges, markovianEdge, localNondeterminismVariableOffset);
                    } else {
                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type.");
                    }
                } else {
                    return ActionDd(this->variables.manager->template getAddZero<ValueType>(), this->variables.manager->template getAddZero<ValueType>(), {}, std::make_pair<uint64_t, uint64_t>(0, 0), {}, this->variables.manager->getBddZero());
                }
            }
            
            void addToTransientAssignmentMap(std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>& transientAssignments, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& assignmentsToAdd) {
                for (auto const& entry : assignmentsToAdd) {
                    auto it = transientAssignments.find(entry.first);
                    if (it != transientAssignments.end()) {
                        it->second += entry.second;
                    } else {
                        transientAssignments[entry.first] = entry.second;
                    }
                }
            }

            void addToTransientAssignmentMap(std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>& transientAssignments, storm::expressions::Variable const& variable, storm::dd::Add<Type, ValueType> const& assignmentToAdd) {
                auto it = transientAssignments.find(variable);
                if (it != transientAssignments.end()) {
                    it->second += assignmentToAdd;
                } else {
                    transientAssignments[variable] = assignmentToAdd;
                }
            }

            std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> joinTransientAssignmentMaps(std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientAssignments1, std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> const& transientAssignments2) {
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> result = transientAssignments1;
                
                for (auto const& entry : transientAssignments2) {
                    auto resultIt = result.find(entry.first);
                    if (resultIt != result.end()) {
                        resultIt->second += entry.second;
                    } else {
                        result[entry.first] = entry.second;
                    }
                }
                
                return result;
            }

            ActionDd combineEdgesToActionDeterministic(std::vector<EdgeDd> const& edgeDds) {
                storm::dd::Bdd<Type> allGuards = this->variables.manager->getBddZero();
                storm::dd::Add<Type, ValueType> allTransitions = this->variables.manager->template getAddZero<ValueType>();
                storm::dd::Bdd<Type> temporary;
                
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragment;
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                bool overlappingGuards = false;
                for (auto const& edgeDd : edgeDds) {
                    STORM_LOG_THROW((this->model.getModelType() == storm::jani::ModelType::CTMC) == edgeDd.isMarkovian, storm::exceptions::WrongFormatException, "Unexpected non-Markovian edge in CTMC.");
                    
                    // Check for overlapping guards.
                    storm::dd::Bdd<Type> guardBdd = edgeDd.guard.toBdd();
                    overlappingGuards = !(guardBdd && allGuards).isZero();
                    
                    // Issue a warning if there are overlapping guards in a DTMC.
                    STORM_LOG_WARN_COND(!overlappingGuards || this->model.getModelType() == storm::jani::ModelType::CTMC, "Guard of an edge in a DTMC overlaps with previous guards.");
                    
                    // Add the elements of the current edge to the global ones.
                    allGuards |= guardBdd;
                    allTransitions += edgeDd.transitions;
                    
                    // Add the transient variable assignments to the resulting one. This transformation is illegal for
                    // CTMCs for which there is some overlap in edges that have some transient assignment (this needs to
                    // be checked later).
                    addToTransientAssignmentMap(transientEdgeAssignments, edgeDd.transientEdgeAssignments);
                    
                    // Keep track of the fragment that is writing global variables.
                    globalVariableToWritingFragment = joinVariableWritingFragmentMaps(globalVariableToWritingFragment, edgeDd.variableToWritingFragment);
                }

                STORM_LOG_THROW(this->model.getModelType() == storm::jani::ModelType::DTMC || !overlappingGuards || transientEdgeAssignments.empty(), storm::exceptions::NotSupportedException, "Cannot have transient edge assignments when combining Markovian edges with overlapping guards.");
                
                return ActionDd(allGuards.template toAdd<ValueType>(), allTransitions, transientEdgeAssignments, std::make_pair<uint64_t, uint64_t>(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero());
            }
            
            void addToVariableWritingFragmentMap(std::map<storm::expressions::Variable, storm::dd::Bdd<Type>>& globalVariableToWritingFragment, storm::expressions::Variable const& variable, storm::dd::Bdd<Type> const& partToAdd) const {
                auto it = globalVariableToWritingFragment.find(variable);
                if (it != globalVariableToWritingFragment.end()) {
                    it->second |= partToAdd;
                } else {
                    globalVariableToWritingFragment.emplace(variable, partToAdd);
                }
            }

            void addToVariableWritingFragmentMap(std::map<storm::expressions::Variable, storm::dd::Bdd<Type>>& globalVariableToWritingFragment, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& partToAdd) const {
                for (auto const& entry : partToAdd) {
                    addToVariableWritingFragmentMap(globalVariableToWritingFragment, entry.first, entry.second);
                }
            }

            std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> joinVariableWritingFragmentMaps(std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& globalVariableToWritingFragment1, std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> const& globalVariableToWritingFragment2) {
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> result = globalVariableToWritingFragment1;
                
                for (auto const& entry : globalVariableToWritingFragment2) {
                    auto resultIt = result.find(entry.first);
                    if (resultIt != result.end()) {
                        resultIt->second |= entry.second;
                    } else {
                        result[entry.first] = entry.second;
                    }
                }
                
                return result;
            }
            
            ActionDd combineEdgesBySummation(storm::dd::Add<Type, ValueType> const& guard, std::vector<EdgeDd> const& edges, boost::optional<EdgeDd> const& markovianEdge) {
                bool addMarkovianFlag = this->model.getModelType() == storm::jani::ModelType::MA;
                STORM_LOG_ASSERT(addMarkovianFlag || !markovianEdge, "Illegally adding Markovian edge without marker.");
                
                storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
                std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragment;
                std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                
                storm::dd::Bdd<Type> flagBdd = addMarkovianFlag ? !this->variables.markovMarker : this->variables.manager->getBddOne();
                storm::dd::Add<Type, ValueType> flag = flagBdd.template toAdd<ValueType>();
                for (auto const& edge : edges) {
                    transitions += addMarkovianFlag ? flag * edge.transitions : edge.transitions;
                    for (auto const& assignment : edge.transientEdgeAssignments) {
                        addToTransientAssignmentMap(transientEdgeAssignments, assignment.first, addMarkovianFlag ? flag * assignment.second : assignment.second);
                    }
                    for (auto const& variableFragment : edge.variableToWritingFragment) {
                        addToVariableWritingFragmentMap(globalVariableToWritingFragment, variableFragment.first, addMarkovianFlag ? flagBdd && variableFragment.second : variableFragment.second);
                    }
                }
                
                // Add the Markovian edge (if any).
                if (markovianEdge) {
                    flagBdd = addMarkovianFlag ? !this->variables.markovMarker : this->variables.manager->getBddOne();
                    flag = flagBdd.template toAdd<ValueType>();
                    EdgeDd const& edge = markovianEdge.get();
                    
                    transitions += flag * edge.transitions;
                    for (auto const& assignment : edge.transientEdgeAssignments) {
                        addToTransientAssignmentMap(transientEdgeAssignments, assignment.first, addMarkovianFlag ? flag * assignment.second : assignment.second);
                    }
                    for (auto const& variableFragment : edge.variableToWritingFragment) {
                        addToVariableWritingFragmentMap(globalVariableToWritingFragment, variableFragment.first, addMarkovianFlag ? flagBdd && variableFragment.second : variableFragment.second);
                    }
                }
                
                return ActionDd(guard, transitions, transientEdgeAssignments, std::make_pair<uint64_t, uint64_t>(0, 0), globalVariableToWritingFragment, this->variables.manager->getBddZero());
            }
            
            ActionDd combineEdgesToActionNondeterministic(std::vector<EdgeDd> const& nonMarkovianEdges, boost::optional<EdgeDd> const& markovianEdge, uint64_t localNondeterminismVariableOffset) {
                // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
                storm::dd::Bdd<Type> allGuards = this->variables.manager->getBddZero();
                storm::dd::Add<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
                for (auto const& edge : nonMarkovianEdges) {
                    STORM_LOG_ASSERT(!edge.isMarkovian, "Unexpected Markovian edge.");
                    sumOfGuards += edge.guard;
                    allGuards |= edge.guard.toBdd();
                }
                uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
                STORM_LOG_TRACE("Found " << maxChoices << " non-Markovian local choices.");
                
                // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism.
                if (maxChoices <= 1) {
                    return combineEdgesBySummation(allGuards.template toAdd<ValueType>(), nonMarkovianEdges, markovianEdge);
                } else {
                    // Calculate number of required variables to encode the nondeterminism.
                    uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
                    
                    storm::dd::Add<Type, ValueType> allEdges = this->variables.manager->template getAddZero<ValueType>();
                    std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragment;
                    std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientAssignments;
                    
                    storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
                    std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, this->variables.manager->template getAddZero<ValueType>());
                    std::vector<storm::dd::Bdd<Type>> remainingDds(maxChoices, this->variables.manager->getBddZero());
                    std::vector<std::pair<storm::dd::Bdd<Type>, storm::dd::Add<Type, ValueType>>> indicesEncodedWithLocalNondeterminismVariables;
                    for (uint64_t j = 0; j < maxChoices; ++j) {
                        storm::dd::Add<Type, ValueType> indexEncoding = encodeIndex(j, localNondeterminismVariableOffset, numberOfBinaryVariables, this->variables);
                        indicesEncodedWithLocalNondeterminismVariables.push_back(std::make_pair(indexEncoding.toBdd(), indexEncoding));
                    }
                    
                    for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
                        // Determine the set of states with exactly currentChoices choices.
                        equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast<double>(currentChoices)));
                        
                        // If there is no such state, continue with the next possible number of choices.
                        if (equalsNumberOfChoicesDd.isZero()) {
                            continue;
                        }
                        
                        // Reset the previously used intermediate storage.
                        for (uint_fast64_t j = 0; j < currentChoices; ++j) {
                            choiceDds[j] = this->variables.manager->template getAddZero<ValueType>();
                            remainingDds[j] = equalsNumberOfChoicesDd;
                        }
                        
                        for (std::size_t j = 0; j < nonMarkovianEdges.size(); ++j) {
                            EdgeDd const& currentEdge = nonMarkovianEdges[j];
                            
                            // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices
                            // choices such that one outgoing choice is given by the j-th edge.
                            storm::dd::Bdd<Type> guardChoicesIntersection = currentEdge.guard.toBdd() && equalsNumberOfChoicesDd;
                            
                            // If there is no such state, continue with the next command.
                            if (guardChoicesIntersection.isZero()) {
                                continue;
                            }
                            
                            // Split the currentChoices nondeterministic choices.
                            for (uint_fast64_t k = 0; k < currentChoices; ++k) {
                                // Calculate the overlapping part of command guard and the remaining DD.
                                storm::dd::Bdd<Type> remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k];
                                
                                // Check if we can add some overlapping parts to the current index.
                                if (!remainingGuardChoicesIntersection.isZero()) {
                                    // Remove overlapping parts from the remaining DD.
                                    remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection;
                                    
                                    // Combine the overlapping part of the guard with command updates and add it to the resulting DD.
                                    choiceDds[k] += remainingGuardChoicesIntersection.template toAdd<ValueType>() * currentEdge.transitions;
                                    
                                    // Keep track of the fragment of transient assignments.
                                    for (auto const& transientAssignment : currentEdge.transientEdgeAssignments) {
                                        addToTransientAssignmentMap(transientAssignments, transientAssignment.first, remainingGuardChoicesIntersection.template toAdd<ValueType>() * transientAssignment.second * indicesEncodedWithLocalNondeterminismVariables[k].first.template toAdd<ValueType>());
                                    }
                                    
                                    // Keep track of the written global variables of the fragment.
                                    for (auto const& variableFragment : currentEdge.variableToWritingFragment) {
                                        addToVariableWritingFragmentMap(globalVariableToWritingFragment, variableFragment.first, remainingGuardChoicesIntersection && variableFragment.second && indicesEncodedWithLocalNondeterminismVariables[k].first);
                                    }
                                }
                                
                                // Remove overlapping parts from the command guard DD
                                guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection;
                                
                                // If the guard DD has become equivalent to false, we can stop here.
                                if (guardChoicesIntersection.isZero()) {
                                    break;
                                }
                            }
                        }
                        
                        // Add the meta variables that encode the nondeterminisim to the different choices.
                        for (uint_fast64_t j = 0; j < currentChoices; ++j) {
                            allEdges += indicesEncodedWithLocalNondeterminismVariables[j].second * choiceDds[j];
                        }
                        
                        // Delete currentChoices out of overlapping DD
                        sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
                    }
                    
                    // Extend the transitions with the appropriate flag if needed.
                    bool addMarkovianFlag = this->model.getModelType() == storm::jani::ModelType::MA;
                    STORM_LOG_ASSERT(addMarkovianFlag || !markovianEdge, "Illegally adding Markovian edge without marker.");
                    if (addMarkovianFlag) {
                        storm::dd::Bdd<Type> flagBdd = !this->variables.markovMarker;
                        storm::dd::Add<Type, ValueType> flag = flagBdd.template toAdd<ValueType>();
                        allEdges *= flag;
                        for (auto& assignment : transientAssignments) {
                            assignment.second *= flag;
                        }
                        for (auto& writingFragment : globalVariableToWritingFragment) {
                            writingFragment.second &= flagBdd;
                        }
                    }
                    
                    // Add Markovian edge (if there is any).
                    if (markovianEdge) {
                        storm::dd::Bdd<Type> flagBdd = this->variables.markovMarker;
                        storm::dd::Add<Type, ValueType> flag = flagBdd.template toAdd<ValueType>();
                        EdgeDd const& edge = markovianEdge.get();

                        allEdges += flag * edge.transitions;
                        for (auto const& assignment : edge.transientEdgeAssignments) {
                            addToTransientAssignmentMap(transientAssignments, assignment.first, flag * assignment.second);
                        }
                        for (auto const& variableFragment : edge.variableToWritingFragment) {
                            addToVariableWritingFragmentMap(globalVariableToWritingFragment, variableFragment.first, flagBdd && variableFragment.second);
                        }
                    }
                    
                    return ActionDd(allGuards.template toAdd<ValueType>(), allEdges, transientAssignments, std::make_pair(localNondeterminismVariableOffset, localNondeterminismVariableOffset + numberOfBinaryVariables), globalVariableToWritingFragment, this->variables.manager->getBddZero());
                }
            }
            
            AutomatonDd buildAutomatonDd(std::string const& automatonName, std::map<uint_fast64_t, uint_fast64_t> const& actionIndexToLocalNondeterminismVariableOffset, std::set<uint64_t> const& inputEnabledActionIndices) {
                AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName));
                
                storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
                for (auto const& action : this->model.getActions()) {
                    uint64_t actionIndex = this->model.getActionIndex(action.getName());
                    if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) {
                        continue;
                    }
                    ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex));
                    if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) {
                        actionDd.setIsInputEnabled();
                    }
                    
                    result.actionIndexToAction[actionIndex] = actionDd;
                    result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable()));
                    result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable()));
                }
                
                for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) {
                    auto const& location = automaton.getLocation(locationIndex);
                    performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) {
                        storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
                        auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable());
                        if (it != result.transientLocationAssignments.end()) {
                            it->second += assignedValues;
                        } else {
                            result.transientLocationAssignments[assignment.getExpressionVariable()] = assignedValues;
                        }
                    });
                }
                
                return result;
            }

            void addMissingGlobalVariableIdentities(ActionDd& action) {
                // Build a DD that we can multiply to the transitions and adds all missing global variable identities that way.
                storm::dd::Add<Type, ValueType> missingIdentities = this->variables.manager->template getAddOne<ValueType>();
                
                for (auto const& variable : this->variables.allGlobalVariables) {
                    auto it = action.variableToWritingFragment.find(variable);
                    if (it != action.variableToWritingFragment.end()) {
                        missingIdentities *= (it->second).ite(this->variables.manager->template getAddOne<ValueType>(), this->variables.variableToIdentityMap.at(variable));
                    } else {
                        missingIdentities *= this->variables.variableToIdentityMap.at(variable);
                    }
                }
                
                action.transitions *= missingIdentities;
            }
            
            ComposerResult<Type, ValueType> buildSystemFromAutomaton(AutomatonDd& automaton) {
                // If the model is an MDP, we need to encode the nondeterminism using additional variables.
                if (this->model.getModelType() == storm::jani::ModelType::MDP) {
                    storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
                    storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
                    
                    // First, determine the highest number of nondeterminism variables that is used in any action and make
                    // all actions use the same amout of nondeterminism variables.
                    uint64_t numberOfUsedNondeterminismVariables = automaton.getHighestLocalNondeterminismVariable();
                    
                    // Add missing global variable identities, action and nondeterminism encodings.
                    std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                    for (auto& action : automaton.actionIndexToAction) {
                        illegalFragment |= action.second.illegalFragment;
                        addMissingGlobalVariableIdentities(action.second);
                        storm::dd::Add<Type, ValueType> actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional<uint64_t>(action.first) : boost::none, this->variables);
                        storm::dd::Add<Type, ValueType> missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables);
                        storm::dd::Add<Type, ValueType> extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions;
                        for (auto const& transientAssignment : action.second.transientEdgeAssignments) {
                            addToTransientAssignmentMap(transientEdgeAssignments, transientAssignment.first, actionEncoding * missingNondeterminismEncoding * transientAssignment.second);
                        }
                        
                        result += extendedTransitions;
                    }
                    
                    return ComposerResult<Type, ValueType>(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, numberOfUsedNondeterminismVariables);
                } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
                    // Simply add all actions, but make sure to include the missing global variable identities.

                    storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
                    storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
                    std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                    for (auto& action : automaton.actionIndexToAction) {
                        illegalFragment |= action.second.illegalFragment;
                        addMissingGlobalVariableIdentities(action.second);
                        addToTransientAssignmentMap(transientEdgeAssignments, action.second.transientEdgeAssignments);
                        result += action.second.transitions;
                    }

                    return ComposerResult<Type, ValueType>(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, 0);
                } else {
                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
                }
            }
        };
        
        template <storm::dd::DdType Type, typename ValueType>
        struct ModelComponents {
            storm::dd::Bdd<Type> reachableStates;
            storm::dd::Bdd<Type> initialStates;
            storm::dd::Bdd<Type> deadlockStates;
            storm::dd::Add<Type, ValueType> transitionMatrix;
            std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
            std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
        };
        
        template <storm::dd::DdType Type, typename ValueType>
        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
            
            if (modelType == storm::jani::ModelType::DTMC) {
                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
            } else if (modelType == storm::jani::ModelType::CTMC) {
                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
            } else if (modelType == storm::jani::ModelType::MDP) {
                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
            } else {
                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
            }
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        void postprocessVariables(storm::jani::ModelType const& modelType, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType>& variables) {
            // Add all action/row/column variables to the DD. If we omitted multiplying edges in the construction, this will
            // introduce the variables so they can later be abstracted without raising an error.
            system.transitions.addMetaVariables(variables.rowMetaVariables);
            system.transitions.addMetaVariables(variables.columnMetaVariables);
            
            // If the model is an MDP, we also add all action variables.
            if (modelType == storm::jani::ModelType::MDP) {
                for (auto const& actionVariablePair : variables.actionVariablesMap) {
                    system.transitions.addMetaVariable(actionVariablePair.second);
                }
            }
            
            // Get rid of the local nondeterminism variables that were not used.
            for (uint64_t index = system.numberOfNondeterminismVariables; index < variables.localNondeterminismVariables.size(); ++index) {
                variables.allNondeterminismVariables.erase(variables.localNondeterminismVariables[index]);
            }
            variables.localNondeterminismVariables.resize(system.numberOfNondeterminismVariables);
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        storm::dd::Bdd<Type> postprocessSystem(storm::jani::Model const& model, ComposerResult<Type, ValueType>& system, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
            // For DTMCs, we normalize each row to 1 (to account for non-determinism).
            if (model.getModelType() == storm::jani::ModelType::DTMC) {
                storm::dd::Add<Type, ValueType> stateToNumberOfChoices = system.transitions.sumAbstract(variables.columnMetaVariables);
                system.transitions = system.transitions / stateToNumberOfChoices;
                
                // Scale all state-action rewards.
                for (auto& entry : system.transientEdgeAssignments) {
                    entry.second = entry.second / stateToNumberOfChoices;
                }
            }
            
            // If we were asked to treat some states as terminal states, we cut away their transitions now.
            if (options.terminalStates || options.negatedTerminalStates) {
                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = model.getConstantsSubstitution();
                
                storm::dd::Bdd<Type> terminalStatesBdd = variables.manager->getBddZero();
                if (options.terminalStates) {
                    storm::expressions::Expression terminalExpression = options.terminalStates.get().substitute(constantsSubstitution);
                    STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
                    terminalStatesBdd = variables.rowExpressionAdapter->translateExpression(terminalExpression).toBdd();
                }
                if (options.negatedTerminalStates) {
                    storm::expressions::Expression negatedTerminalExpression = options.negatedTerminalStates.get().substitute(constantsSubstitution);
                    STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal.");
                    terminalStatesBdd |= !variables.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd();
                }
                
                system.transitions *= (!terminalStatesBdd).template toAdd<ValueType>();
                return terminalStatesBdd;
            }
            return variables.manager->getBddZero();
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        storm::dd::Bdd<Type> computeInitialStates(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) {
            std::vector<std::reference_wrapper<storm::jani::Automaton const>> allAutomata;
            for (auto const& automaton : model.getAutomata()) {
                allAutomata.push_back(automaton);
            }
            storm::dd::Bdd<Type> initialStates = variables.rowExpressionAdapter->translateExpression(model.getInitialStatesExpression(allAutomata)).toBdd();
            for (auto const& automaton : model.getAutomata()) {
                storm::dd::Bdd<Type> initialLocationIndices = variables.manager->getBddZero();
                for (auto const& locationIndex : automaton.getInitialLocationIndices()) {
                    initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, locationIndex);
                }
                initialStates &= initialLocationIndices;
            }
            for (auto const& metaVariable : variables.rowMetaVariables) {
                initialStates &= variables.variableToRangeMap.at(metaVariable);
            }
            return initialStates;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        storm::dd::Bdd<Type> fixDeadlocks(storm::jani::ModelType const& modelType, storm::dd::Add<Type, ValueType>& transitionMatrix, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& reachableStates, CompositionVariables<Type, ValueType> const& variables) {
            // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
            storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(variables.columnMetaVariables);
            storm::dd::Bdd<Type> deadlockStates = reachableStates && !statesWithTransition;
            
            if (!deadlockStates.isZero()) {
                // If we need to fix deadlocks, we do so now.
                if (!storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet()) {
                    STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: ");
                    
                    storm::dd::Add<Type, ValueType> deadlockStatesAdd = deadlockStates.template toAdd<ValueType>();
                    uint_fast64_t count = 0;
                    for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.end(); it != ite && count < 3; ++it, ++count) {
                        STORM_LOG_INFO((*it).first.toPrettyString(variables.rowMetaVariables) << std::endl);
                    }
                    
                    // Create a global identity DD.
                    storm::dd::Add<Type, ValueType> globalIdentity = variables.manager->template getAddOne<ValueType>();
                    for (auto const& identity : variables.automatonToIdentityMap) {
                        globalIdentity *= identity.second;
                    }
                    for (auto const& variable : variables.allGlobalVariables) {
                        globalIdentity *= variables.variableToIdentityMap.at(variable);
                    }
                    
                    if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) {
                        // For DTMCs, we can simply add the identity of the global module for all deadlock states.
                        transitionMatrix += deadlockStatesAdd * globalIdentity;
                    } else if (modelType == storm::jani::ModelType::MDP) {
                        // For MDPs, however, we need to select an action associated with the self-loop, if we do not
                        // want to attach a lot of self-loops to the deadlock states.
                        storm::dd::Add<Type, ValueType> action = variables.manager->template getAddOne<ValueType>();
                        for (auto const& variable : variables.actionVariablesMap) {
                            action *= variables.manager->template getIdentity<ValueType>(variable.second);
                        }
                        for (auto const& variable : variables.localNondeterminismVariables) {
                            action *= variables.manager->template getIdentity<ValueType>(variable);
                        }
                        transitionMatrix += deadlockStatesAdd * globalIdentity * action;
                    }
                } else {
                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
                }
            }
            return deadlockStates;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        std::vector<storm::expressions::Variable> selectRewardVariables(storm::jani::Model const& model, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
            std::vector<storm::expressions::Variable> result;
            if (options.isBuildAllRewardModelsSet()) {
                for (auto const& variable : model.getGlobalVariables()) {
                    if (variable.isTransient() && (variable.isRealVariable() || variable.isUnboundedIntegerVariable())) {
                        result.push_back(variable.getExpressionVariable());
                    }
                }
            } else {
                auto const& globalVariables = model.getGlobalVariables();
                for (auto const& rewardModelName : options.getRewardModelNames()) {
                    if (globalVariables.hasVariable(rewardModelName)) {
                        result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
                    } else {
                        STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
                        STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
                    }
                }
                
                // If no reward model was yet added, but there was one that was given in the options, we try to build the
                // standard reward model.
                if (result.empty() && !options.getRewardModelNames().empty()) {
                    result.push_back(globalVariables.getTransientVariables().front().getExpressionVariable());
                }
            }
            
            return result;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> buildRewardModels(ComposerResult<Type, ValueType> const& system, std::vector<storm::expressions::Variable> const& rewardVariables) {
            std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> result;
            
            for (auto const& variable : rewardVariables) {
                boost::optional<storm::dd::Add<Type, ValueType>> stateRewards = boost::none;
                boost::optional<storm::dd::Add<Type, ValueType>> stateActionRewards = boost::none;
                boost::optional<storm::dd::Add<Type, ValueType>> transitionRewards = boost::none;
                
                auto it = system.transientLocationAssignments.find(variable);
                if (it != system.transientLocationAssignments.end()) {
                    stateRewards = it->second;
                }
                
                it = system.transientEdgeAssignments.find(variable);
                if (it != system.transientEdgeAssignments.end()) {
                    stateActionRewards = it->second;
                }
                
                result.emplace(variable.getName(), storm::models::symbolic::StandardRewardModel<Type, ValueType>(stateRewards, stateActionRewards, transitionRewards));
            }
            
            return result;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        std::map<std::string, storm::expressions::Expression> buildLabelExpressions(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
            std::map<std::string, storm::expressions::Expression> result;
            
            for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
                if (variable.isBooleanVariable()) {
                    if (options.buildAllLabels || options.labelNames.find(variable.getName()) != options.labelNames.end()) {
                        result[variable.getName()] = model.getLabelExpression(variable.asBooleanVariable(), variables.automatonToLocationVariableMap);
                    }
                }
            }
            
            return result;
        }
        
        template <storm::dd::DdType Type, typename ValueType>
        std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
            if (model.hasUndefinedConstants()) {
                std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
                std::vector<std::string> strings;
                for (auto const& constant : undefinedConstants) {
                    std::stringstream stream;
                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
                    strings.push_back(stream.str());
                }
                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << ".");
            }
            
            STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels.");
            
            storm::jani::Model preparedModel = model;
            
            // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
            if (preparedModel.hasTransientEdgeDestinationAssignments()) {
                preparedModel.liftTransientEdgeDestinationAssignments();
            }
            
            STORM_LOG_THROW(!preparedModel.hasTransientEdgeDestinationAssignments(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support transient edge destination assignments.");
            
            // Determine the actions that will appear in the parallel composition.
            storm::jani::CompositionInformationVisitor visitor(preparedModel, preparedModel.getSystemComposition());
            storm::jani::CompositionInformation actionInformation = visitor.getInformation();
            
            // Create all necessary variables.
            CompositionVariableCreator<Type, ValueType> variableCreator(preparedModel, actionInformation);
            CompositionVariables<Type, ValueType> variables = variableCreator.create();
            
            // Determine which transient assignments need to be considered in the building process.
            std::vector<storm::expressions::Variable> rewardVariables = selectRewardVariables<Type, ValueType>(preparedModel, options);
            
            // Create a builder to compose and build the model.
            CombinedEdgesSystemComposer<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables);
            ComposerResult<Type, ValueType> system = composer.compose();
            
            // Postprocess the variables in place.
            postprocessVariables(preparedModel.getModelType(), system, variables);
            
            // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off).
            storm::dd::Bdd<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options);
            
            // Start creating the model components.
            ModelComponents<Type, ValueType> modelComponents;
            
            // Build initial states.
            modelComponents.initialStates = computeInitialStates(preparedModel, variables);
            
            // Perform reachability analysis to obtain reachable states.
            storm::dd::Bdd<Type> transitionMatrixBdd = system.transitions.notZero();
            if (preparedModel.getModelType() == storm::jani::ModelType::MDP) {
                transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables);
            }
            modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables);
            
            // Check that the reachable fragment does not overlap with the illegal fragment.
            storm::dd::Bdd<Type> reachableIllegalFragment = modelComponents.reachableStates && system.illegalFragment;
            STORM_LOG_THROW(reachableIllegalFragment.isZero(), storm::exceptions::WrongFormatException, "There are reachable states in the model that have synchronizing edges enabled that write the same global variable.");
            
            // Cut transitions to reachable states.
            storm::dd::Add<Type, ValueType> reachableStatesAdd = modelComponents.reachableStates.template toAdd<ValueType>();
            modelComponents.transitionMatrix = system.transitions * reachableStatesAdd;
            
            // Fix deadlocks if existing.
            modelComponents.deadlockStates = fixDeadlocks(preparedModel.getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables);
            
            // Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal.
            modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates;
            
            // Build the reward models.
            modelComponents.rewardModels = buildRewardModels(system, rewardVariables);
            
            // Build the label to expressions mapping.
            modelComponents.labelToExpressionMap = buildLabelExpressions(preparedModel, variables, options);
            
            // Finally, create the model.
            return createModel(preparedModel.getModelType(), variables, modelComponents);
        }
        
        template class DdJaniModelBuilder<storm::dd::DdType::CUDD, double>;
        template class DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>;
    }
}