started on quotient extraction using the original variables, debugging CUDD...

src/storm/settings/modules/BisimulationSettings.cpp

@@ -15,6 +15,7 @@ namespace storm {
             const std::string BisimulationSettings::moduleName = "bisimulation";
             const std::string BisimulationSettings::typeOptionName = "type";
             const std::string BisimulationSettings::representativeOptionName = "repr";
+            const std::string BisimulationSettings::originalVariablesOptionName = "origvar";
             const std::string BisimulationSettings::quotientFormatOptionName = "quot";
             const std::string BisimulationSettings::signatureModeOptionName = "sigmode";
             const std::string BisimulationSettings::reuseOptionName = "reuse";
@@ -29,6 +30,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").build());
 
                 std::vector<std::string> signatureModes = { "eager", "lazy" };
                 this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
@@ -78,6 +80,10 @@ namespace storm {
                 return this->getOption(representativeOptionName).getHasOptionBeenSet();
             }
             
+            bool BisimulationSettings::isUseOriginalVariablesSet() const {
+                return this->getOption(originalVariablesOptionName).getHasOptionBeenSet();
+            }
+            
             storm::dd::bisimulation::SignatureMode BisimulationSettings::getSignatureMode() const {
                 std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString();
                 if (modeAsString == "eager") {

src/storm/settings/modules/BisimulationSettings.h

@@ -56,6 +56,13 @@ namespace storm {
                  */
                 bool isUseRepresentativesSet() const;
                 
+                /*!
+                 * Retrieves whether the extracted quotient model is supposed to use the same variables as the original
+                 * model.
+                 * NOTE: only applies to DD-based bisimulation.
+                 */
+                bool isUseOriginalVariablesSet() const;
+                
                 /*!
                  * Retrieves the mode to compute signatures.
                  */
@@ -85,6 +92,7 @@ namespace storm {
                 // Define the string names of the options as constants.
                 static const std::string typeOptionName;
                 static const std::string representativeOptionName;
+                static const std::string originalVariablesOptionName;
                 static const std::string quotientFormatOptionName;
                 static const std::string signatureModeOptionName;
                 static const std::string reuseOptionName;

src/storm/storage/dd/Add.cpp

@@ -231,6 +231,46 @@ namespace storm {
             return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
         }
         
+        template<DdType LibraryType, typename ValueType>
+        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const {
+            std::vector<InternalBdd<LibraryType>> fromBdds;
+            std::vector<InternalBdd<LibraryType>> toBdds;
+            
+            for (auto const& metaVariable : from) {
+                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present.");
+                DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
+                for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
+                    fromBdds.push_back(ddVariable.getInternalBdd());
+                    std::cout << "from - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl;
+                }
+            }
+//            std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
+            for (auto const& metaVariable : to) {
+                STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present.");
+                DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
+                for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
+                    toBdds.push_back(ddVariable.getInternalBdd());
+                    std::cout << "to - idx " << ddVariable.getInternalBdd().getIndex() << ", lvl " << ddVariable.getInternalBdd().getLevel() << std::endl;
+                }
+            }
+//            std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
+
+            std::set<storm::expressions::Variable> newContainedMetaVariables = to;
+            std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin()));
+            
+            if (fromBdds.size() == toBdds.size()) {
+                return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables);
+            } else {
+                InternalBdd<LibraryType> cube = this->getDdManager().getBddOne().getInternalBdd();
+                for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) {
+                    cube &= fromBdds[index];
+                }
+                fromBdds.resize(toBdds.size());
+                
+                return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.sumAbstract(cube).permuteVariables(fromBdds, toBdds), newContainedMetaVariables);
+            }
+        }
+        
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
             std::set<storm::expressions::Variable> newContainedMetaVariables;

src/storm/storage/dd/Add.h

@@ -331,6 +331,20 @@ namespace storm {
              */
             Add<LibraryType, ValueType> renameVariables(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
             
+            /*!
+             * Renames the given meta variables in the ADD. The number of the underlying DD variables of the from meta
+             * variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide,
+             * this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables
+             * and then performs the renaming.
+             *
+             * @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables.
+             * @param to The meta variables that are the target of the renaming process. The current ADD must not contain
+             * any of these meta variables.
+             * @return The resulting ADD.
+             */
+            Add<LibraryType, ValueType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
+
+            
             /*!
              * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have
              * the same number of underlying ADD variables.

src/storm/storage/dd/Bdd.cpp

@@ -319,6 +319,44 @@ namespace storm {
             return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> Bdd<LibraryType>::renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const {
+            std::vector<InternalBdd<LibraryType>> fromBdds;
+            std::vector<InternalBdd<LibraryType>> toBdds;
+            
+            for (auto const& metaVariable : from) {
+                STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present.");
+                DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
+                for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
+                    fromBdds.push_back(ddVariable.getInternalBdd());
+                }
+            }
+            std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
+            for (auto const& metaVariable : to) {
+                STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present.");
+                DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
+                for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
+                    toBdds.push_back(ddVariable.getInternalBdd());
+                }
+            }
+            std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
+            
+            std::set<storm::expressions::Variable> newContainedMetaVariables = to;
+            std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin()));
+            
+            if (fromBdds.size() == toBdds.size()) {
+                return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
+            } else {
+                InternalBdd<LibraryType> cube = this->getDdManager().getBddOne().getInternalBdd();
+                for (uint64_t index = fromBdds.size(); index < fromBdds.size(); ++index) {
+                    cube &= fromBdds[index];
+                }
+                fromBdds.resize(toBdds.size());
+                
+                return Bdd<LibraryType>(this->getDdManager(), internalBdd.existsAbstract(cube).swapVariables(fromBdds, toBdds), newContainedMetaVariables);
+            }
+        }
+        
         template<DdType LibraryType>
         template<typename ValueType>
         Add<LibraryType, ValueType> Bdd<LibraryType>::toAdd() const {

src/storm/storage/dd/Bdd.h

@@ -285,6 +285,19 @@ namespace storm {
              */
             Bdd<LibraryType> renameVariables(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
             
+            /*!
+             * Renames the given meta variables in the BDD. The number of the underlying DD variables of the from meta
+             * variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide,
+             * this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables
+             * and then performs the renaming.
+             *
+             * @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables.
+             * @param to The meta variables that are the target of the renaming process. The current ADD must not contain
+             * any of these meta variables.
+             * @return The resulting ADD.
+             */
+            Bdd<LibraryType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
+            
             /*!
              * Retrieves whether this DD represents the constant one function.
              *

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -821,6 +821,7 @@ namespace storm {
             QuotientExtractor<DdType, ValueType>::QuotientExtractor() : useRepresentatives(false) {
                 auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
                 this->useRepresentatives = settings.isUseRepresentativesSet();
+                this->useOriginalVariables = settings.isUseOriginalVariablesSet();
                 this->quotientFormat = settings.getQuotientFormat();
             }
             
@@ -921,7 +922,12 @@ namespace storm {
 
             template<storm::dd::DdType DdType, typename ValueType>
             std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
-                return extractQuotientUsingBlockVariables(model, partition, preservationInformation);
+                
+                if (this->useOriginalVariables) {
+                    return extractQuotientUsingOriginalVariables(model, partition, preservationInformation);
+                } else {
+                    return extractQuotientUsingBlockVariables(model, partition, preservationInformation);
+                }
             }
 
             template<storm::dd::DdType DdType, typename ValueType>
@@ -1036,6 +1042,134 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
                 }
             }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+                auto modelType = model.getType();
+                
+                if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) {
+                    STORM_LOG_WARN_COND(!this->useRepresentatives, "Using representatives is unsupported for this extraction, falling back to regular extraction.");
+                    
+                    // Sanity checks.
+                    STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size.");
+                    STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition.");
+                    
+                    std::set<storm::expressions::Variable> blockVariableSet = {partition.getBlockVariable()};
+                    std::set<storm::expressions::Variable> blockPrimeVariableSet = {partition.getPrimedBlockVariable()};
+                    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())};
+                    
+                    storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero();
+                    
+                    auto start = std::chrono::high_resolution_clock::now();
+                    partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
+                    storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
+                    storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
+                    
+                    std::map<std::string, storm::dd::Bdd<DdType>> preservedLabelBdds;
+                    for (auto const& label : preservationInformation.getLabels()) {
+                        preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()));
+                    }
+                    for (auto const& expression : preservationInformation.getExpressions()) {
+                        std::stringstream stream;
+                        stream << expression;
+                        std::string expressionAsString = stream.str();
+                        
+                        auto it = preservedLabelBdds.find(expressionAsString);
+                        if (it != preservedLabelBdds.end()) {
+                            STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition.");
+                        } else {
+                            preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()));
+                        }
+                    }
+                    auto end = std::chrono::high_resolution_clock::now();
+                    STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    
+                    start = std::chrono::high_resolution_clock::now();
+                    std::set<storm::expressions::Variable> blockAndRowVariables;
+                    std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end()));
+                    std::set<storm::expressions::Variable> blockPrimeAndColumnVariables;
+                    std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end()));
+                    storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
+                    storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables());
+                    (model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()).renameVariablesAbstract(blockPrimeVariableSet, model.getColumnVariables())).exportToDot("tmp0.dot");
+                    quotientTransitionMatrix.exportToDot("tmp1.dot");
+                    std::cout << "q1 size: " << quotientTransitionMatrix.getNodeCount() << ", " << quotientTransitionMatrix.getNonZeroCount() << std::endl;
+                    quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("tmp1_1.dot");
+//                    quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("tmp1_1.dot");
+
+                    // Pick a representative from each block.
+                    auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
+                    partitionAsBdd &= representatives;
+                    partitionAsAdd *= partitionAsBdd.template toAdd<ValueType>();
+                    partitionAsAdd.exportToDot("partrepr.dot");
+                    partitionAsAdd.sumAbstract(model.getRowVariables()).exportToDot("part2.dot");
+                    std::cout << "part size " << partitionAsAdd.getNodeCount() << ", " << partitionAsAdd.getNonZeroCount() << std::endl;
+                    
+                    auto tmp1 = partitionAsAdd.multiplyMatrix(quotientTransitionMatri, model.getRowVariables());
+                    auto tmp2 = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables());
+                    std::cout << "size1: " << tmp1.getNodeCount() << ", " << tmp1.getNonZeroCount() << std::endl;
+                    std::cout << "size2: " << tmp2.getNodeCount() << ", " << tmp2.getNonZeroCount() << std::endl;
+                    if (tmp1 != tmp2) {
+                        tmp1.exportToDot("tmp1__.dot");
+                        tmp2.exportToDot("tmp2__.dot");
+                        (tmp2-tmp1).exportToDot("diff.dot");
+                        STORM_LOG_ASSERT(false, "error");
+                    }
+                    quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).exportToDot("tmp2.dot");
+                    quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(model.getColumnVariables()).exportToDot("tmp2_2.dot");
+//                    quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).sumAbstract(blockPrimeVariableSet).exportToDot("tmp2_2.dot");
+                    quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
+                    end = std::chrono::high_resolution_clock::now();
+                    
+                    // Check quotient matrix for sanity.
+                    if (std::is_same<ValueType, storm::RationalNumber>::value) {
+                        STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
+                    } else {
+                        STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(1e-6)).isZero(), "Illegal entries in quotient matrix.");
+                    }
+                    quotientTransitionMatrix.exportToDot("trans.dot");
+                    quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).exportToDot("trans1.dot");
+                    quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd<ValueType>().exportToDot("trans2.dot");
+                    STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal probabilistic matrix.");
+                    
+                    STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    
+                    storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
+                    storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates;
+                    
+                    start = std::chrono::high_resolution_clock::now();
+                    std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<DdType, ValueType>> quotientRewardModels;
+                    for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) {
+                        auto const& rewardModel = model.getRewardModel(rewardModelName);
+                        
+                        boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateRewards;
+                        if (rewardModel.hasStateRewards()) {
+                            quotientStateRewards = rewardModel.getStateRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
+                        }
+                        
+                        boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateActionRewards;
+                        if (rewardModel.hasStateActionRewards()) {
+                            quotientStateActionRewards = rewardModel.getStateActionRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
+                        }
+                        
+                        quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel<DdType, ValueType>(quotientStateRewards, quotientStateActionRewards, boost::none));
+                    }
+                    end = std::chrono::high_resolution_clock::now();
+                    STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                    
+                    if (modelType == storm::models::ModelType::Dtmc) {
+                        return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
+                    } else if (modelType == storm::models::ModelType::Ctmc) {
+                        return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
+                    } else if (modelType == storm::models::ModelType::Mdp) {
+                        return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
+                    } else {
+                        return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
+                    }
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
+                }
+            }
                         
             template class QuotientExtractor<storm::dd::DdType::CUDD, double>;
             

src/storm/storage/dd/bisimulation/QuotientExtractor.h

@@ -28,8 +28,10 @@ namespace storm {
                 
                 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
                 std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
-                
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+
                 bool useRepresentatives;
+                bool useOriginalVariables;
                 storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat;
             };
             

src/storm/storage/dd/cudd/InternalCuddAdd.cpp

@@ -202,6 +202,7 @@ namespace storm {
             for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
                 fromAdd.push_back(it1->getCuddBdd().Add());
                 toAdd.push_back(it2->getCuddBdd().Add());
+                std::cout << fromAdd.back().NodeReadIndex() << " <-> " << toAdd.back().NodeReadIndex() << std::endl;
             }
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd));
         }

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -319,7 +319,7 @@ namespace storm {
              * @return The resulting ADD.
              */
             InternalAdd<DdType::Sylvan, ValueType> swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const;
-
+            
             /*!
              * Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by
              * ADDs must have equal length.