started on partial quotient extraction in symbolic bisimulation

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -4,6 +4,7 @@
 #include "storm/storage/dd/bisimulation/PartitionRefiner.h"
 #include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h"
 #include "storm/storage/dd/bisimulation/QuotientExtractor.h"
+#include "storm/storage/dd/bisimulation/PartialQuotientExtractor.h"
 
 #include "storm/models/symbolic/Model.h"
 #include "storm/models/symbolic/Mdp.h"
@@ -36,6 +37,11 @@ namespace storm {
             showProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
             this->refineWrtRewardModels();
+            
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+#ifndef NDEBUG
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
+#endif
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -44,6 +50,11 @@ namespace storm {
             showProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
             this->refineWrtRewardModels();
+            
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+#ifndef NDEBUG
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
+#endif
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -52,6 +63,11 @@ namespace storm {
             showProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
             this->refineWrtRewardModels();
+            
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+#ifndef NDEBUG
+            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
+#endif
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -60,11 +76,7 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         void BisimulationDecomposition<DdType, ValueType>::compute(bisimulation::SignatureMode const& mode) {
             STORM_LOG_ASSERT(refiner, "No suitable refiner.");
-            
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
-#ifndef NDEBUG
-            STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
-#endif
+            STORM_LOG_ASSERT(this->refiner->getStatus() != Status::FixedPoint, "Can only proceed if no fixpoint has been reached yet.");
 
             auto start = std::chrono::high_resolution_clock::now();
             auto timeOfLastMessage = start;
@@ -90,16 +102,54 @@ namespace storm {
             
             STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "s (" << iterations << " iterations).");
         }
+
+        template <storm::dd::DdType DdType, typename ValueType>
+        bool BisimulationDecomposition<DdType, ValueType>::compute(uint64_t steps, bisimulation::SignatureMode const& mode) {
+            STORM_LOG_ASSERT(refiner, "No suitable refiner.");
+            STORM_LOG_ASSERT(this->refiner->getStatus() != Status::FixedPoint, "Can only proceed if no fixpoint has been reached yet.");
+            STORM_LOG_ASSERT(steps > 0, "Can only perform positive number of steps.");
+
+            auto start = std::chrono::high_resolution_clock::now();
+            auto timeOfLastMessage = start;
+            uint64_t iterations = 0;
+            bool refined = true;
+            while (refined && iterations < steps) {
+                refined = refiner->refine(mode);
+                
+                ++iterations;
+                
+                if (showProgress) {
+                    auto now = std::chrono::high_resolution_clock::now();
+                    auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
+                    if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
+                        auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
+                        STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "s) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
+                        timeOfLastMessage = std::chrono::high_resolution_clock::now();
+                    }
+                }
+            }
+            
+            return !refined;
+        }
         
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
-            STORM_LOG_THROW(this->refiner->getStatus() == Status::FixedPoint, storm::exceptions::InvalidOperationException, "Cannot extract quotient, because bisimulation decomposition was not completed.");
-            
-            STORM_LOG_TRACE("Starting quotient extraction.");
-            QuotientExtractor<DdType, ValueType> extractor;
-            std::shared_ptr<storm::models::Model<ValueType>> quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
+            std::shared_ptr<storm::models::Model<ValueType>> quotient;
+            if (this->refiner->getStatus() == Status::FixedPoint) {
+                STORM_LOG_TRACE("Starting full quotient extraction.");
+                QuotientExtractor<DdType, ValueType> extractor;
+                quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
+            } else {
+                STORM_LOG_TRACE("Starting partial quotient extraction.");
+                if (!partialQuotientExtractor) {
+                    partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType>>(model);
+                }
+
+                quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
+                STORM_LOG_TRACE("Quotient extraction done.");
+            }
+
             STORM_LOG_TRACE("Quotient extraction done.");
-            
             return quotient;
         }
         

src/storm/storage/dd/BisimulationDecomposition.h

@@ -28,6 +28,9 @@ namespace storm {
 
             template <storm::dd::DdType DdType, typename ValueType>
             class PartitionRefiner;
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            class PartialQuotientExtractor;
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -40,10 +43,17 @@ namespace storm {
             ~BisimulationDecomposition();
             
             /*!
-             * Computes the decomposition.
+             * Performs partition refinement until a fixpoint has been reached.
              */
             void compute(bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager);
             
+            /*!
+             * Performs the given number of refinement steps.
+             *
+             * @return True iff the computation arrived at a fixpoint.
+             */
+            bool compute(uint64_t steps, bisimulation::SignatureMode const& mode);
+            
             /*!
              * Retrieves the quotient model after the bisimulation decomposition was computed.
              */
@@ -61,6 +71,9 @@ namespace storm {
             // The refiner to use.
             std::unique_ptr<bisimulation::PartitionRefiner<DdType, ValueType>> refiner;
             
+            // A quotient extractor that is used when the fixpoint has not been reached yet.
+            mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType>> partialQuotientExtractor;
+            
             // A flag indicating whether progress is reported.
             bool showProgress;
             

src/storm/storage/dd/DdManager.h

@@ -168,8 +168,8 @@ namespace storm {
              * Clones the given meta variable and optionally changes the number of layers of the variable.
              *
              * @param variable The variable to clone.
-             * @param newVariableName The name of the variable to crate.
-             * @param numberOfLayers The number of layers of the variable to crate
+             * @param newVariableName The name of the variable to create.
+             * @param numberOfLayers The number of layers of the variable to create.
              */
             std::vector<storm::expressions::Variable> cloneVariable(storm::expressions::Variable const& variable, std::string const& newVariableName, boost::optional<uint64_t> const& numberOfLayers = boost::none);
             

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

@@ -0,0 +1,63 @@
+#include "storm/storage/dd/bisimulation/PartialQuotientExtractor.h"
+
+#include "storm/storage/dd/DdManager.h"
+
+#include "storm/settings/SettingsManager.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+
+            template<storm::dd::DdType DdType, typename ValueType>
+            PartialQuotientExtractor<DdType, ValueType>::PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model) : model(model) {
+                auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
+                this->quotientFormat = settings.getQuotientFormat();
+                
+                STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
+                
+                // We need to create auxiliary variables that encode the nondeterminism arising from partion quotient extraction.
+                auto& manager = model.getManager();
+                uint64_t numberOfDdVariables = 0;
+                for (auto const& metaVariable : model.getRowVariables()) {
+                    auto const& ddMetaVariable = manager.getMetaVariable(metaVariable);
+                    numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables();
+                }
+                std::vector<storm::expressions::Variable> auxVariables = manager.addBitVectorMetaVariable("quot", numberOfDdVariables, 1);
+                STORM_LOG_ASSERT(auxVariables.size() == 1, "Expected exactly one meta variable.");
+                nondeterminismVariable = auxVariables.front();
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            std::shared_ptr<storm::models::Model<ValueType>> PartialQuotientExtractor<DdType, ValueType>::extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+                auto start = std::chrono::high_resolution_clock::now();
+                std::shared_ptr<storm::models::Model<ValueType>> result;
+
+                STORM_LOG_THROW(this->quotientFormat == storm::settings::modules::BisimulationSettings::QuotientFormat::Dd, storm::exceptions::NotSupportedException, "Only DD-based partial quotient extraction is currently supported.");
+                result = extractDdQuotient(partition, preservationInformation);
+                auto end = std::chrono::high_resolution_clock::now();
+                STORM_LOG_TRACE("Quotient extraction completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                
+                STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "Quotient could not be extracted.");
+                
+                return result;
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> PartialQuotientExtractor<DdType, ValueType>::extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
+                return nullptr;
+            }
+            
+            template class PartialQuotientExtractor<storm::dd::DdType::CUDD, double>;
+            template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, double>;
+
+#ifdef STORM_HAVE_CARL
+            template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalNumber>;
+            template class PartialQuotientExtractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#endif
+            
+        }
+    }
+}

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

@@ -0,0 +1,39 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/models/symbolic/Model.h"
+#include "storm/models/sparse/Model.h"
+
+#include "storm/storage/dd/bisimulation/Partition.h"
+#include "storm/storage/dd/bisimulation/PreservationInformation.h"
+
+#include "storm/settings/modules/BisimulationSettings.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+
+            template<storm::dd::DdType DdType, typename ValueType>
+            class PartialQuotientExtractor {
+                public:
+                PartialQuotientExtractor(storm::models::symbolic::Model<DdType, ValueType> const& model);
+                
+                std::shared_ptr<storm::models::Model<ValueType>> extract(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                
+                private:
+                std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
+                
+                // The model for which to compute the partial quotient.
+                storm::models::symbolic::Model<DdType, ValueType> const& model;
+                
+                storm::expressions::Variable nondeterminismVariable;
+                
+                storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat;
+            };
+            
+        }
+    }
+}

src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp

@@ -45,6 +45,45 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Cudd) {
     EXPECT_TRUE(quotient->isSymbolicModel());
 }
 
+TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD, double>().build(program);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::CUDD, double> decomposition(*model, storm::storage::BisimulationType::Strong);
+    std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+}
+
+TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, double>().build(program);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
+    decomposition.compute();
+    std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+    
+    EXPECT_EQ(11ul, quotient->getNumberOfStates());
+    EXPECT_EQ(17ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+    
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+    
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+    formulas.push_back(formula);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
+    decomposition2.compute();
+    quotient = decomposition2.getQuotient();
+    
+    EXPECT_EQ(5ul, quotient->getNumberOfStates());
+    EXPECT_EQ(8ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+}
+
 TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) {
     storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");
     
@@ -78,6 +117,39 @@ TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) {
     EXPECT_TRUE(quotient->isSymbolicModel());
 }
 
+TEST(SymbolicModelBisimulationDecomposition, Crowds_Sylvan) {
+    storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");
+    
+    // Preprocess model to substitute all constants.
+    smd = smd.preprocess();
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, double>().build(smd.asPrismProgram());
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
+    decomposition.compute();
+    std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+    
+    EXPECT_EQ(2007ul, quotient->getNumberOfStates());
+    EXPECT_EQ(3738ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+    
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+    formulas.push_back(formula);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
+    decomposition2.compute();
+    quotient = decomposition2.getQuotient();
+    
+    EXPECT_EQ(65ul, quotient->getNumberOfStates());
+    EXPECT_EQ(105ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+}
+
 TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
 
@@ -110,6 +182,38 @@ TEST(SymbolicModelBisimulationDecomposition, TwoDice_Cudd) {
     EXPECT_EQ(19ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
 }
 
+TEST(SymbolicModelBisimulationDecomposition, TwoDice_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, double>().build(program);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
+    decomposition.compute();
+    std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+    
+    EXPECT_EQ(77ul, quotient->getNumberOfStates());
+    EXPECT_EQ(210ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+    EXPECT_EQ(116ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>()->getNumberOfChoices()));
+    
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+    formulas.push_back(formula);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
+    decomposition2.compute();
+    quotient = decomposition2.getQuotient();
+    
+    EXPECT_EQ(11ul, quotient->getNumberOfStates());
+    EXPECT_EQ(34ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+    EXPECT_EQ(19ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>()->getNumberOfChoices()));
+}
+
 TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
     storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
     
@@ -144,3 +248,38 @@ TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Cudd) {
     EXPECT_TRUE(quotient->isSymbolicModel());
     EXPECT_EQ(2152ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>()->getNumberOfChoices()));
 }
+
+TEST(SymbolicModelBisimulationDecomposition, AsynchronousLeader_Sylvan) {
+    storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
+    
+    // Preprocess model to substitute all constants.
+    smd = smd.preprocess();
+    
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, double>().build(smd.asPrismProgram(), *formula);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition(*model, storm::storage::BisimulationType::Strong);
+    decomposition.compute();
+    std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+    
+    EXPECT_EQ(252ul, quotient->getNumberOfStates());
+    EXPECT_EQ(624ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+    EXPECT_EQ(500ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>()->getNumberOfChoices()));
+    
+    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+    formulas.push_back(formula);
+    
+    storm::dd::BisimulationDecomposition<storm::dd::DdType::Sylvan, double> decomposition2(*model, formulas, storm::storage::BisimulationType::Strong);
+    decomposition2.compute();
+    quotient = decomposition2.getQuotient();
+    
+    EXPECT_EQ(1107ul, quotient->getNumberOfStates());
+    EXPECT_EQ(2684ul, quotient->getNumberOfTransitions());
+    EXPECT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    EXPECT_TRUE(quotient->isSymbolicModel());
+    EXPECT_EQ(2152ul, (quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>()->getNumberOfChoices()));
+}