Started making hybrid (dd/sparse) model checking work.

Former-commit-id: 23fac3a672

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -0,0 +1,110 @@
+#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
+
+#include "src/storage/dd/CuddOdd.h"
+
+#include "src/utility/macros.h"
+#include "src/utility/graph.h"
+
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+
+#include "src/exceptions/InvalidStateException.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType DdType, typename ValueType>
+        HybridDtmcPrctlModelChecker<DdType, ValueType>::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker<DdType>(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        HybridDtmcPrctlModelChecker<DdType, ValueType>::HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType> const& model) : SymbolicPropositionalModelChecker<DdType>(model), linearEquationSolverFactory(new storm::utility::solver::LinearEquationSolverFactory<ValueType>()) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool HybridDtmcPrctlModelChecker<DdType, ValueType>::canHandle(storm::logic::Formula const& formula) const {
+            return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::dd::Add<DdType> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+            // We need to identify the states which have to be taken out of the matrix, i.e. all states that have
+            // probability 0 and 1 of satisfying the until-formula.
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
+            storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates();
+            
+            // Create the ODD for the translation between symbolic and explicit storage.
+            storm::dd::Odd<DdType> odd(maybeStates);
+            
+            // Perform some logging.
+            STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states.");
+            STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states.");
+            STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
+            
+            // Check whether we need to compute exact probabilities for some states.
+            if (qualitative) {
+                // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
+                return statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5);
+            } else {
+                // If there are maybe states, we need to solve an equation system.
+                if (!maybeStates.isZero()) {
+                    // Create the matrix and the vector for the equation system.
+                    storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd();
+                    
+                    // Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
+                    // non-maybe states in the matrix.
+                    storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd;
+                    
+                    // Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
+                    // maybe states.
+                    storm::dd::Add<DdType> prob1StatesAsColumn = statesWithProbability01.second.toAdd();
+                    prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs());
+                    storm::dd::Add<DdType> subvector = submatrix * prob1StatesAsColumn;
+                    subvector = subvector.sumAbstract(model.getColumnVariables());
+                    
+                    // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed
+                    // for solving the equation system (i.e. compute (I-A)).
+                    submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
+                    submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix;
+                    
+                    // Create the solution vector.
+                    std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
+                    
+                    // Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
+                    storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
+                    std::vector<ValueType> b = subvector.template toVector<ValueType>(odd);
+                    
+                    std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix);
+                    solver->solveEquationSystem(x, b);
+                    
+                    // Now that we have the explicit solution of the system, we need to transform it to a symbolic representation.
+                    storm::dd::Add<DdType> numericResult; // = storm::dd::Add<DdType>(x, odd);
+                    return statesWithProbability01.second.toAdd() + numericResult;
+                } else {
+                    return statesWithProbability01.second.toAdd();
+                }
+            }
+            
+            exit(-1);
+            return storm::dd::Add<DdType>();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+            SymbolicQualitativeCheckResult<DdType> const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+            SymbolicQualitativeCheckResult<DdType> const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+            return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->computeUntilProbabilitiesHelper(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory)));
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::models::symbolic::Dtmc<DdType> const& HybridDtmcPrctlModelChecker<DdType, ValueType>::getModel() const {
+            return this->template getModelAs<storm::models::symbolic::Dtmc<DdType>>();
+        }
+        
+        template class HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double>;
+    }
+}

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h

@@ -0,0 +1,34 @@
+#ifndef STORM_MODELCHECKER_HYBRIDDTMCPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_HYBRIDDTMCPRCTLMODELCHECKER_H_
+
+#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
+#include "src/models/symbolic/Dtmc.h"
+#include "src/utility/solver.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType DdType, typename ValueType>
+        class HybridDtmcPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType> {
+        public:
+            explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType> const& model);
+            explicit HybridDtmcPrctlModelChecker(storm::models::symbolic::Dtmc<DdType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
+            
+            // The implemented methods of the AbstractModelChecker interface.
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
+            virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            
+        protected:
+            storm::models::symbolic::Dtmc<DdType> const& getModel() const override;
+            
+        private:
+            // The methods that perform the actual checking.
+            static storm::dd::Add<DdType> computeUntilProbabilitiesHelper(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
+            
+            // An object that is used for retrieving linear equation solvers.
+            std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
+        };
+        
+    } // namespace modelchecker
+} // namespace storm
+
+#endif /* STORM_MODELCHECKER_HYBRIDDTMCPRCTLMODELCHECKER_H_ */

src/modelchecker/propositional/SymbolicPropositionalModelChecker.h

@@ -2,7 +2,6 @@
 #define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
 
 #include "src/modelchecker/AbstractModelChecker.h"
-
 #include "src/models/symbolic/Model.h"
 
 namespace storm {

src/modelchecker/results/SymbolicQualitativeCheckResult.cpp

@@ -6,7 +6,7 @@
 namespace storm {
     namespace modelchecker {
         template <storm::dd::DdType Type>
-        SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& allStates, storm::dd::Bdd<Type> const& truthValues) : allStates(allStates), truthValues(truthValues) {
+        SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues) : reachableStates(reachableStates), truthValues(truthValues) {
             // Intentionally left empty.
         }
         
@@ -29,21 +29,23 @@ namespace storm {
         QualitativeCheckResult& SymbolicQualitativeCheckResult<Type>::operator&=(QualitativeCheckResult const& other) {
             STORM_LOG_THROW(other.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
             this->truthValues &= other.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
+            return *this;
         }
 
         template <storm::dd::DdType Type>
         QualitativeCheckResult& SymbolicQualitativeCheckResult<Type>::operator|=(QualitativeCheckResult const& other) {
             STORM_LOG_THROW(other.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
             this->truthValues |= other.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
+            return *this;
         }
 
         template <storm::dd::DdType Type>
         void SymbolicQualitativeCheckResult<Type>::complement() {
-            this->truthValues = !this->truthValues && allStates;
+            this->truthValues = !this->truthValues && reachableStates;
         }
         
         template <storm::dd::DdType Type>
-        storm::dd::Dd<Type> const& SymbolicQualitativeCheckResult<Type>::getTruthValuesVector() const {
+        storm::dd::Bdd<Type> const& SymbolicQualitativeCheckResult<Type>::getTruthValuesVector() const {
             return truthValues;
         }
         
@@ -62,5 +64,7 @@ namespace storm {
             STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter.");
             this->truthValues &= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
         }
+        
+        template class SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>;
     }
 }

src/modelchecker/results/SymbolicQualitativeCheckResult.h

@@ -12,7 +12,7 @@ namespace storm {
         class SymbolicQualitativeCheckResult : public QualitativeCheckResult {
         public:
             SymbolicQualitativeCheckResult() = default;
-            SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& allStates, storm::dd::Bdd<Type> const& truthValues);
+            SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues);
             
             SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default;
             SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default;
@@ -30,15 +30,15 @@ namespace storm {
             virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override;
             virtual void complement() override;
             
-            storm::dd::Dd<Type> const& getTruthValuesVector() const;
+            storm::dd::Bdd<Type> const& getTruthValuesVector() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual void filter(QualitativeCheckResult const& filter) override;
             
         private:
-            // The set of all states.
-            storm::dd::Bdd<Type> allStates;
+            // The set of all reachable states.
+            storm::dd::Bdd<Type> reachableStates;
             
             // The values of the qualitative check result.
             storm::dd::Bdd<Type> truthValues;

src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -7,22 +7,23 @@
 namespace storm {
     namespace modelchecker {
         template<storm::dd::DdType Type>
-        SymbolicQuantitativeCheckResult<Type>::SymbolicQuantitativeCheckResult(storm::dd::Add<Type> const& allStates, storm::dd::Add<Type> const& values) : allStates(allStates), values(values) {
+        SymbolicQuantitativeCheckResult<Type>::SymbolicQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Add<Type> const& values) : reachableStates(reachableStates), values(values) {
             // Intentionally left empty.
         }
         
         template<storm::dd::DdType Type>
         std::unique_ptr<CheckResult> SymbolicQuantitativeCheckResult<Type>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
-            std::unique_ptr<SymbolicQualitativeCheckResult<Type>> result;
-            if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::GreaterEqual) {
-                result = std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(allStates, values.greaterOrEqual(bound)));
-            } else {
-                result = std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(allStates, values.greater(bound)));
+            storm::dd::Bdd<Type> states;
+            if (comparisonType == storm::logic::ComparisonType::Less) {
+                states = values.less(bound);
+            } else if (comparisonType == storm::logic::ComparisonType::LessEqual) {
+                states = values.lessOrEqual(bound);
+            } else if (comparisonType == storm::logic::ComparisonType::Greater) {
+                states = values.greater(bound);
+            } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) {
+                states = values.greaterOrEqual(bound);
             }
-            if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
-                result->complement();
-            }
-            return result;
+            return std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, values.greaterOrEqual(bound)));;
         }
         
         template<storm::dd::DdType Type>
@@ -64,7 +65,10 @@ namespace storm {
         template<storm::dd::DdType Type>
         void SymbolicQuantitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) {
             STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter.");
-            this->truthValues *= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector().toMtbdd();
+            this->values *= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector().toAdd();
         }
+        
+        // Explicitly instantiate the class.
+        template class SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>;
     }
 }

src/modelchecker/results/SymbolicQuantitativeCheckResult.h

@@ -12,7 +12,7 @@ namespace storm {
         class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult {
         public:
             SymbolicQuantitativeCheckResult() = default;
-            SymbolicQuantitativeCheckResult(storm::dd::Add<Type> const& allStates, storm::dd::Add<Type> const& values);
+            SymbolicQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Add<Type> const& values);
             
             SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default;
             SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default;
@@ -35,8 +35,8 @@ namespace storm {
             virtual void filter(QualitativeCheckResult const& filter) override;
             
         private:
-            // The set of all states.
-            storm::dd::Add<Type> allStates;
+            // The set of all reachable states.
+            storm::dd::Bdd<Type> reachableStates;
             
             // The values of the quantitative check result.
             storm::dd::Add<Type> values;

src/models/symbolic/Model.cpp

@@ -132,6 +132,16 @@ namespace storm {
                 return labelToExpressionMap;
             }
             
+            template<storm::dd::DdType Type>
+            storm::dd::Add<Type> Model<Type>::getRowColumnIdentity() const {
+                storm::dd::Add<Type> result = this->getManager().getAddOne();
+                for (auto const& pair : this->getRowColumnMetaVariablePairs()) {
+                    result *= this->getManager().getIdentity(pair.first).equals(this->getManager().getIdentity(pair.second));
+                    result *= this->getManager().getRange(pair.first).toAdd() * this->getManager().getRange(pair.second).toAdd();
+                }
+                return result;
+            }
+            
             template<storm::dd::DdType Type>
             void Model<Type>::printModelInformationToStream(std::ostream& out) const {
                 out << "-------------------------------------------------------------- " << std::endl;

src/models/symbolic/Model.h

@@ -193,6 +193,13 @@ namespace storm {
                  */
                 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& getRowColumnMetaVariablePairs() const;
                 
+                /*!
+                 * Retrieves an ADD that represents the diagonal of the transition matrix.
+                 *
+                 * @return An ADD that represents the diagonal of the transition matrix.
+                 */
+                storm::dd::Add<Type> getRowColumnIdentity() const;
+                
                 virtual std::size_t getSizeInBytes() const override;
                 
                 virtual void printModelInformationToStream(std::ostream& out) const override;

src/settings/modules/GeneralSettings.cpp

@@ -82,9 +82,9 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
                 
-                std::vector<std::string> engines = {"sparse", "dd"};
+                std::vector<std::string> engines = {"sparse", "hybrid", "dd"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
@@ -274,6 +274,8 @@ namespace storm {
                 std::string engine = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString();
                 if (engine == "sparse") {
                     return GeneralSettings::Engine::Sparse;
+                } else if (engine == "hybrid") {
+                    return GeneralSettings::Engine::Hybrid;
                 } else if (engine == "dd") {
                     return GeneralSettings::Engine::Dd;
                 }
@@ -298,7 +300,7 @@ namespace storm {
                 uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0);
                 STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both.");
                 
-                STORM_LOG_THROW(this->getEngine() != Engine::Dd || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Decision-diagram engine can only be used with symbolic input models.");
+                STORM_LOG_THROW(this->getEngine() == Engine::Sparse || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine.");
                 
                 return true;
             }

src/settings/modules/GeneralSettings.h

@@ -14,7 +14,7 @@ namespace storm {
             class GeneralSettings : public ModuleSettings {
             public:                
                 // An enumeration of all engines.
-                enum class Engine { Sparse, Dd };
+                enum class Engine { Sparse, Hybrid, Dd };
                 
                 // An enumeration of all available LP solvers.
                 enum class LpSolver { Gurobi, glpk };

src/storage/dd/CuddAdd.cpp

@@ -300,6 +300,14 @@ namespace storm {
             return Bdd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables());
         }
         
+        Bdd<DdType::CUDD> Add<DdType::CUDD>::less(double value) const {
+            return Bdd<DdType::CUDD>(this->getDdManager(), ~this->getCuddAdd().BddThreshold(value), this->getContainedMetaVariables());
+        }
+        
+        Bdd<DdType::CUDD> Add<DdType::CUDD>::lessOrEqual(double value) const {
+            return Bdd<DdType::CUDD>(this->getDdManager(), ~this->getCuddAdd().BddStrictThreshold(value), this->getContainedMetaVariables());
+        }
+        
         Bdd<DdType::CUDD> Add<DdType::CUDD>::notZero() const {
             return this->toBdd();
         }

src/storage/dd/CuddAdd.h

@@ -337,6 +337,24 @@ namespace storm {
              */
             Bdd<DdType::CUDD> greaterOrEqual(double value) const;
             
+            /*!
+             * Computes a BDD that represents the function in which all assignments with a function value strictly
+             * lower than the given value are mapped to one and all others to zero.
+             *
+             * @param value The value used for the comparison.
+             * @return The resulting BDD.
+             */
+            Bdd<DdType::CUDD> less(double value) const;
+            
+            /*!
+             * Computes a BDD that represents the function in which all assignments with a function value less or equal
+             * to the given value are mapped to one and all others to zero.
+             *
+             * @param value The value used for the comparison.
+             * @return The resulting BDD.
+             */
+            Bdd<DdType::CUDD> lessOrEqual(double value) const;
+            
             /*!
              * Computes a BDD that represents the function in which all assignments with a function value unequal to
              * zero are mapped to one and all others to zero.

src/utility/cli.h

@@ -67,6 +67,9 @@ log4cplus::Logger printer;
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
+#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
 // Headers for counterexample generation.
 #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
@@ -77,6 +80,7 @@ log4cplus::Logger printer;
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidSettingsException.h"
 #include "src/exceptions/InvalidTypeException.h"
+#include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace utility {
@@ -331,7 +335,7 @@ namespace storm {
                     }
                     
                     result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
-                } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd) {
+                } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
                     typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
                     if (formula) {
                         options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
@@ -409,26 +413,24 @@ namespace storm {
                 
                 // If we were requested to generate a counterexample, we now do so.
                 if (settings.isCounterexampleSet()) {
-                    STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Counterexample generation is only available for sparse models.");
                     STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
                     generateCounterexample<ValueType>(program.get(), model, formula);
                 } else {
-                    std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
                     std::cout << std::endl << "Model checking property: " << *formula << " ...";
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
                     if (model->getType() == storm::models::ModelType::Dtmc) {
-                        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>();
-                        storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
+                        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
+                        storm::modelchecker::SparseDtmcPrctlModelChecker<ValueType> modelchecker(*dtmc);
                         if (modelchecker.canHandle(*formula.get())) {
                             result = modelchecker.check(*formula.get());
                         } else {
-                            storm::modelchecker::SparseDtmcPrctlModelChecker<ValueType> modelchecker2(*dtmc);
+                            storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker2(*dtmc);
                             if (modelchecker2.canHandle(*formula.get())) {
                                 modelchecker2.check(*formula.get());
                             }
                         }
                     } else if (model->getType() == storm::models::ModelType::Mdp) {
-                        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = sparseModel->template as<storm::models::sparse::Mdp<ValueType>>();
+                        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
 #ifdef STORM_HAVE_CUDA
                         if (settings.isCudaSet()) {
                             storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
@@ -442,7 +444,7 @@ namespace storm {
                         result = modelchecker.check(*formula.get());
 #endif
                     } else if (model->getType() == storm::models::ModelType::Ctmc) {
-                        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = sparseModel->template as<storm::models::sparse::Ctmc<ValueType>>();
+                        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
 
                         storm::modelchecker::SparseCtmcCslModelChecker<ValueType> modelchecker(*ctmc);
                         result = modelchecker.check(*formula.get());
@@ -451,7 +453,7 @@ namespace storm {
                     if (result) {
                         std::cout << " done." << std::endl;
                         std::cout << "Result (initial states): ";
-                        result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+                        result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
                         std::cout << *result << std::endl;
                     } else {
                         std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
@@ -489,6 +491,32 @@ namespace storm {
             }
 #endif
             
+            template<storm::dd::DdType DdType>
+            void verifySymbolicModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<storm::logic::Formula> formula) {
+                storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+                
+                std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                std::unique_ptr<storm::modelchecker::CheckResult> result;
+                if (model->getType() == storm::models::ModelType::Dtmc) {
+                    std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
+                    storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
+                    if (modelchecker.canHandle(*formula.get())) {
+                        modelchecker.check(*formula.get());
+                    }
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
+                }
+                
+                if (result) {
+                    std::cout << " done." << std::endl;
+                    std::cout << "Result (initial states): ";
+                    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
+                    std::cout << *result << std::endl;
+                } else {
+                    std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                }
+            }
+            
             template<typename ValueType>
             void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
                 // Now we are ready to actually build the model.
@@ -507,8 +535,15 @@ namespace storm {
                 if (formula) {
                     if (model->isSparseModel()) {
                         verifySparseModel<ValueType>(program, model->as<storm::models::sparse::Model<ValueType>>(), formula.get());
+                    } else if (model->isSymbolicModel()) {
+                        if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
+                            verifySymbolicModel(program, model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formula.get());
+                        } else {
+                            // Not handled yet.
+                            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
+                        }
                     } else {
-                        // Not handled yet.
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
                     }
                 }
             }

src/utility/graph.h

@@ -264,7 +264,7 @@ namespace storm {
              * @return All states with positive probability.
              */
             template <storm::dd::DdType Type>
-            storm::dd::Bdd<Type> performProbGreater0(storm::models::symbolic::DeterministicModel<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+            storm::dd::Bdd<Type> performProbGreater0(storm::models::symbolic::Model<Type> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
                 // Initialize environment for backward search.
                 storm::dd::DdManager<Type> const& manager = model.getManager();
                 storm::dd::Bdd<Type> lastIterationStates = manager.getBddZero();
@@ -303,6 +303,26 @@ namespace storm {
                 return result;
             }
             
+            /*!
+             * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
+             * deterministic model.
+             *
+             * @param model The (symbolic) model for which to compute the set of states. This is used for retrieving the
+             * manager and information about the meta variables.
+             * @param phiStates The BDD containing all  phi states of the model.
+             * @param psiStates The BDD containing all psi states of the model.
+             * @return A pair of BDDs that represent all states with probability 0 and 1, respectively.
+             */
+            template <storm::dd::DdType Type>
+            static std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> performProb01(storm::models::symbolic::Model<Type> const& model, storm::dd::Add<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates) {
+                std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> result;
+                storm::dd::Bdd<Type> transitionMatrixBdd = transitionMatrix.notZero();
+                result.first = performProbGreater0(model, transitionMatrixBdd, phiStates, psiStates);
+                result.second = !performProbGreater0(model, transitionMatrixBdd, !psiStates && model.getReachableStates(), !result.first && model.getReachableStates()) && model.getReachableStates();
+                result.first = !result.first && model.getReachableStates();
+                return result;
+            }
+            
             /*!
              * Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least
              * one possible resolution of non-determinism in a non-deterministic model. Stated differently,