added dd-based partial quotient extraction for DTMCs

src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -87,7 +87,7 @@ namespace storm {
                 this->values = newMap;
             }
         }
-        
+
         template<typename ValueType>
         ValueType ExplicitQuantitativeCheckResult<ValueType>::getMin() const {
             STORM_LOG_THROW(!values.empty(), storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined.");
@@ -123,7 +123,7 @@ namespace storm {
         
         template<typename ValueType>
         ValueType ExplicitQuantitativeCheckResult<ValueType>::sum() const {
-            STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined");
+            STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Sum of empty set is not defined");
             
             ValueType sum = storm::utility::zero<ValueType>();
             if (this->isResultForAllStates()) {
@@ -142,7 +142,7 @@ namespace storm {
         
         template<typename ValueType>
         ValueType ExplicitQuantitativeCheckResult<ValueType>::average() const {
-            STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined");
+            STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Average of empty set is not defined");
             
             ValueType sum = storm::utility::zero<ValueType>();
             if (this->isResultForAllStates()) {

src/storm/modelchecker/results/QuantitativeCheckResult.h

@@ -15,7 +15,6 @@ namespace storm {
             
             
             virtual ValueType getMin() const = 0;
-            
             virtual ValueType getMax() const = 0;
             
             virtual ValueType average() const = 0;

src/storm/storage/dd/BisimulationDecomposition.h

@@ -52,7 +52,7 @@ namespace storm {
              *
              * @return True iff the computation arrived at a fixpoint.
              */
-            bool compute(uint64_t steps, bisimulation::SignatureMode const& mode);
+            bool compute(uint64_t steps, bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager);
             
             /*!
              * Retrieves the quotient model after the bisimulation decomposition was computed.

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

@@ -2,6 +2,9 @@
 
 #include "storm/storage/dd/DdManager.h"
 
+#include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
 #include "storm/settings/SettingsManager.h"
 
 #include "storm/utility/macros.h"
@@ -17,17 +20,6 @@ namespace storm {
                 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>
@@ -47,7 +39,103 @@ namespace storm {
             
             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;
+                
+                auto modelType = model.getType();
+                if (modelType == storm::models::ModelType::Dtmc) {
+                    // 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());
+                    storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(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()));
+                    }
+                    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()));
+                        }
+                    }
+                    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());
+                    
+//                    // Pick a representative from each block.
+//                    auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
+//                    partitionAsBdd &= representatives;
+//                    partitionAsAdd *= partitionAsBdd.template toAdd<ValueType>();
+                    
+//                    quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables());
+                    quotientTransitionMatrix = quotientTransitionMatrix * partitionAsAdd;
+                    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.");
+                    }
+                    
+                    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(blockPrimeVariableSet) && 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() * partitionAsAdd;
+                        }
+                        
+                        boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateActionRewards;
+                        if (rewardModel.hasStateActionRewards()) {
+                            quotientStateActionRewards = rewardModel.getStateActionRewardVector() * partitionAsAdd;
+                        }
+                        
+                        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.");
+                    
+                    std::set<storm::expressions::Variable> newNondeterminismVariables = model.getNondeterminismVariables();
+                    newNondeterminismVariables.insert(model.getRowVariables().begin(), model.getRowVariables().end());
+                    
+                    if (modelType == storm::models::ModelType::Dtmc) {
+                        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, newNondeterminismVariables, preservedLabelBdds, quotientRewardModels));
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type.");
+                    }
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract partial quotient for this model type.");
+                }
             }
             
             template class PartialQuotientExtractor<storm::dd::DdType::CUDD, double>;

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

@@ -28,9 +28,7 @@ namespace storm {
                 
                 // 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/storm/storage/dd/bisimulation/PartitionRefiner.cpp

@@ -123,6 +123,11 @@ namespace storm {
                 return statePartition;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            Signature<DdType, ValueType> PartitionRefiner<DdType, ValueType>::getFullSignature() const {
+                return signatureComputer.getFullSignature(statePartition);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             Status PartitionRefiner<DdType, ValueType>::getStatus() const {
                 return status;

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

@@ -43,6 +43,11 @@ namespace storm {
                  */
                 Partition<DdType, ValueType> const& getStatePartition() const;
                 
+                /*!
+                 * Retrieves the full signature of all states wrt. the current state partition.
+                 */
+                Signature<DdType, ValueType> getFullSignature() const;
+                
                 /*!
                  * Retrieves the status of the refinement process.
                  */

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

@@ -50,12 +50,12 @@ namespace storm {
                 void setSignatureMode(SignatureMode const& newMode);
 
                 SignatureIterator<DdType, ValueType> compute(Partition<DdType, ValueType> const& partition);
-                
-            private:
+
                 /// Methods to compute the signatures.
                 Signature<DdType, ValueType> getFullSignature(Partition<DdType, ValueType> const& partition) const;
                 Signature<DdType, ValueType> getQualitativeSignature(Partition<DdType, ValueType> const& partition) const;
-                
+
+            private:
                 bool qualitativeTransitionMatrixIsBdd() const;
                 storm::dd::Bdd<DdType> const& getQualitativeTransitionMatrixAsBdd() const;
                 storm::dd::Add<DdType, ValueType> const& getQualitativeTransitionMatrixAsAdd() const;

src/test/storm/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp

@@ -2,12 +2,13 @@
 #include "storm-config.h"
 
 #include "storm/logic/Formulas.h"
+#include "storm/parser/FormulaParser.h"
+
 #include "storm/utility/solver.h"
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
-#include "storm/parser/FormulaParser.h"
 #include "storm/parser/PrismParser.h"
 #include "storm/builder/DdPrismModelBuilder.h"
 #include "storm/models/symbolic/Dtmc.h"

src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp

@@ -9,9 +9,22 @@
 #include "storm/storage/dd/BisimulationDecomposition.h"
 #include "storm/storage/SymbolicModelDescription.h"
 
+#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "storm/modelchecker/results/QuantitativeCheckResult.h"
+
+#include "storm/solver/SymbolicLinearEquationSolver.h"
+#include "storm/solver/SymbolicMinMaxLinearEquationSolver.h"
+
+#include "storm/logic/Formulas.h"
+#include "storm/parser/FormulaParser.h"
+
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 
+#include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
@@ -51,7 +64,88 @@ TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_Cudd) {
     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();
+    ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+
+    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>();
+    
+    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker(*quotientMdp, std::make_unique<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>());
+    
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]");
+    std::shared_ptr<storm::logic::Formula const> maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]");
+
+    std::pair<double, double> resultBounds;
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
+    result = checker.check(*maxFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+
+    EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
+    EXPECT_EQ(resultBounds.second, storm::utility::one<double>());
+
+    // Perform only one step.
+    decomposition.compute(1);
+    
+    quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>();
+    
+    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker2(*quotientMdp, std::make_unique<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>());
+
+    result = checker2.check(*minFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
+    result = checker2.check(*maxFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+
+    EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
+    EXPECT_NEAR(resultBounds.second, static_cast<double>(1)/3, 1e-6);
+
+    // Perform only one step.
+    decomposition.compute(1);
+    
+    quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>();
+
+    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>> checker3(*quotientMdp, std::make_unique<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>());
+
+    result = checker3.check(*minFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
+    result = checker3.check(*maxFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+
+    EXPECT_NEAR(resultBounds.first, static_cast<double>(1)/6, 1e-6);
+    EXPECT_NEAR(resultBounds.second, static_cast<double>(1)/6, 1e-6);
+    EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6);
+    
+    decomposition.compute(1);
+
+    quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>> checker4(*quotientDtmc);
+
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+
+    result = checker4.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates()));
+    resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+
+    EXPECT_NEAR(resultBounds.first, static_cast<double>(1)/6, 1e-6);
 }
 
 TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) {
@@ -84,6 +178,96 @@ TEST(SymbolicModelBisimulationDecomposition, Die_Sylvan) {
     EXPECT_TRUE(quotient->isSymbolicModel());
 }
 
+TEST(SymbolicModelBisimulationDecomposition, DiePartialQuotient_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);
+    
+    std::shared_ptr<storm::models::Model<double>> quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    
+    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>();
+    
+    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker(*quotientMdp, std::make_unique<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>());
+    
+    storm::parser::FormulaParser formulaParser;
+    std::shared_ptr<storm::logic::Formula const> minFormula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"one\"]");
+    std::shared_ptr<storm::logic::Formula const> maxFormula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"one\"]");
+    
+    std::pair<double, double> resultBounds;
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
+    result = checker.check(*maxFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+    
+    EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
+    EXPECT_EQ(resultBounds.second, storm::utility::one<double>());
+    
+    // Perform only one step.
+    decomposition.compute(1);
+    
+    quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>();
+    
+    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker2(*quotientMdp, std::make_unique<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>());
+    
+    result = checker2.check(*minFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
+    result = checker2.check(*maxFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+    
+    EXPECT_EQ(resultBounds.first, storm::utility::zero<double>());
+    EXPECT_NEAR(resultBounds.second, static_cast<double>(1)/3, 1e-6);
+    
+    // Perform only one step.
+    decomposition.compute(1);
+    
+    quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Mdp, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    quotientMdp = quotient->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>();
+    
+    storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>> checker3(*quotientMdp, std::make_unique<storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>());
+    
+    result = checker3.check(*minFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.first = result->asQuantitativeCheckResult<double>().sum();
+    result = checker3.check(*maxFormula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientMdp->getReachableStates(), quotientMdp->getInitialStates()));
+    resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+    
+    EXPECT_NEAR(resultBounds.first, static_cast<double>(1)/6, 1e-6);
+    EXPECT_NEAR(resultBounds.second, static_cast<double>(1)/6, 1e-6);
+    EXPECT_NEAR(resultBounds.first, resultBounds.second, 1e-6);
+    
+    decomposition.compute(1);
+    
+    quotient = decomposition.getQuotient();
+    ASSERT_EQ(storm::models::ModelType::Dtmc, quotient->getType());
+    ASSERT_TRUE(quotient->isSymbolicModel());
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> quotientDtmc = quotient->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>> checker4(*quotientDtmc);
+    
+    std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    
+    result = checker4.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(quotientDtmc->getReachableStates(), quotientDtmc->getInitialStates()));
+    resultBounds.first = resultBounds.second = result->asQuantitativeCheckResult<double>().sum();
+    
+    EXPECT_NEAR(resultBounds.first, static_cast<double>(1)/6, 1e-6);
+}
+
 TEST(SymbolicModelBisimulationDecomposition, Crowds_Cudd) {
     storm::storage::SymbolicModelDescription smd = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds5_5.pm");