Created new class for storing hybrid check results (symbolic as well as explicit parts) and the surrounding functionality.

Former-commit-id: d4ad6da5a1

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -7,6 +7,7 @@
 
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
 
 #include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/InvalidPropertyException.h"
@@ -29,7 +30,7 @@ namespace storm {
         }
         
         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) {
+        std::unique_ptr<CheckResult> 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);
@@ -46,7 +47,7 @@ namespace storm {
             // 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);
+                return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), 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()) {
@@ -86,17 +87,11 @@ namespace storm {
                     solver->solveEquationSystem(x, b);
                     
                     // Now that we have the explicit solution of the system, we need to transform it to a symbolic representation.
-                    STORM_LOG_DEBUG("Converting the explicit result to a symbolic form.");
-                    storm::dd::Add<DdType> numericResult(model.getManager().asSharedPointer(), x, odd, model.getRowVariables());
-                    
-                    return statesWithProbability01.second.toAdd() + numericResult;
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x));
                 } else {
-                    return statesWithProbability01.second.toAdd();
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd()));
                 }
             }
-            
-            exit(-1);
-            return storm::dd::Add<DdType>();
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
@@ -105,7 +100,7 @@ namespace storm {
             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)));
+            return this->computeUntilProbabilitiesHelper(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory);
         }
         
         template<storm::dd::DdType DdType, typename ValueType>

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h

@@ -22,7 +22,7 @@ namespace storm {
             
         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);
+            static std::unique_ptr<CheckResult> 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;

src/modelchecker/results/CheckResult.cpp

@@ -8,6 +8,7 @@
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
@@ -22,6 +23,10 @@ namespace storm {
             return false;
         }
         
+        bool CheckResult::isHybrid() const {
+            return false;
+        }
+        
         bool CheckResult::isQuantitative() const {
             return false;
         }
@@ -55,6 +60,10 @@ namespace storm {
             return false;
         }
         
+        bool CheckResult::isHybridQuantitativeCheckResult() const {
+            return false;
+        }
+        
         ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() {
             return dynamic_cast<ExplicitQualitativeCheckResult&>(*this);
         }
@@ -108,6 +117,16 @@ namespace storm {
         SymbolicQuantitativeCheckResult<Type> const& CheckResult::asSymbolicQuantitativeCheckResult() const {
             return dynamic_cast<SymbolicQuantitativeCheckResult<Type> const&>(*this);
         }
+
+        template <storm::dd::DdType Type>
+        HybridQuantitativeCheckResult<Type>& CheckResult::asHybridQuantitativeCheckResult() {
+            return dynamic_cast<HybridQuantitativeCheckResult<Type>&>(*this);
+        }
+        
+        template <storm::dd::DdType Type>
+        HybridQuantitativeCheckResult<Type> const& CheckResult::asHybridQuantitativeCheckResult() const {
+            return dynamic_cast<HybridQuantitativeCheckResult<Type> const&>(*this);
+        }
         
         // Explicitly instantiate the template functions.
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
@@ -116,6 +135,8 @@ namespace storm {
         template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQualitativeCheckResult() const;
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asSymbolicQuantitativeCheckResult();
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+        template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asHybridQuantitativeCheckResult();
+        template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asHybridQuantitativeCheckResult() const;
 
 #ifdef STORM_HAVE_CARL
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();

src/modelchecker/results/CheckResult.h

@@ -16,6 +16,7 @@ namespace storm {
         template <typename ValueType> class ExplicitQuantitativeCheckResult;
         template <storm::dd::DdType Type> class SymbolicQualitativeCheckResult;
         template <storm::dd::DdType Type> class SymbolicQuantitativeCheckResult;
+        template <storm::dd::DdType Type> class HybridQuantitativeCheckResult;
         
         // The base class of all check results.
         class CheckResult {
@@ -31,12 +32,14 @@ namespace storm {
             // Methods to retrieve the actual type of the check result.
             virtual bool isExplicit() const;
             virtual bool isSymbolic() const;
+            virtual bool isHybrid() const;
             virtual bool isQuantitative() const;
             virtual bool isQualitative() const;
             virtual bool isExplicitQualitativeCheckResult() const;
             virtual bool isExplicitQuantitativeCheckResult() const;
             virtual bool isSymbolicQualitativeCheckResult() const;
             virtual bool isSymbolicQuantitativeCheckResult() const;
+            virtual bool isHybridQuantitativeCheckResult() const;
             virtual bool isResultForAllStates() const;
             
             QualitativeCheckResult& asQualitativeCheckResult();
@@ -65,6 +68,12 @@ namespace storm {
 
             template <storm::dd::DdType Type>
             SymbolicQuantitativeCheckResult<Type> const& asSymbolicQuantitativeCheckResult() const;
+
+            template <storm::dd::DdType Type>
+            HybridQuantitativeCheckResult<Type>& asHybridQuantitativeCheckResult();
+            
+            template <storm::dd::DdType Type>
+            HybridQuantitativeCheckResult<Type> const& asHybridQuantitativeCheckResult() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
         };

src/modelchecker/results/HybridQuantitativeCheckResult.cpp

@@ -0,0 +1,128 @@
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type>
+        HybridQuantitativeCheckResult<Type>::HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd<Type> const& odd, std::vector<double> const& explicitValues) : reachableStates(reachableStates), symbolicStates(symbolicStates), symbolicValues(symbolicValues), explicitStates(explicitStates), odd(odd), explicitValues(explicitValues) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType Type>
+        std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+            storm::dd::Bdd<Type> symbolicResult;
+
+            // First compute the symbolic part of the result.
+            if (comparisonType == storm::logic::ComparisonType::Less) {
+                symbolicResult = symbolicValues.less(bound);
+            } else if (comparisonType == storm::logic::ComparisonType::LessEqual) {
+                symbolicResult = symbolicValues.lessOrEqual(bound);
+            } else if (comparisonType == storm::logic::ComparisonType::Greater) {
+                symbolicResult = symbolicValues.greater(bound);
+            } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) {
+                symbolicResult = symbolicValues.greaterOrEqual(bound);
+            }
+            
+            // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result.
+            symbolicResult |= storm::dd::Bdd<Type>(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, bound);
+            
+            return std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(reachableStates, symbolicResult));
+        }
+        
+        template<storm::dd::DdType Type>
+        bool HybridQuantitativeCheckResult<Type>::isHybrid() const {
+            return true;
+        }
+        
+        template<storm::dd::DdType Type>
+        bool HybridQuantitativeCheckResult<Type>::isResultForAllStates() const {
+            return true;
+        }
+        
+        template<storm::dd::DdType Type>
+        bool HybridQuantitativeCheckResult<Type>::isHybridQuantitativeCheckResult() const {
+            return true;
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::dd::Bdd<Type> const& HybridQuantitativeCheckResult<Type>::getSymbolicStates() const {
+            return symbolicStates;
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::dd::Add<Type> const& HybridQuantitativeCheckResult<Type>::getSymbolicValueVector() const {
+            return symbolicValues;
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::dd::Bdd<Type> const& HybridQuantitativeCheckResult<Type>::getExplicitStates() const {
+            return explicitStates;
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::dd::Odd<Type> const& HybridQuantitativeCheckResult<Type>::getOdd() const {
+            return odd;
+        }
+        
+        template<storm::dd::DdType Type>
+        std::vector<double> const& HybridQuantitativeCheckResult<Type>::getExplicitValueVector() const {
+            return explicitValues;
+        }
+        
+        template<storm::dd::DdType Type>
+        std::ostream& HybridQuantitativeCheckResult<Type>::writeToStream(std::ostream& out) const {
+            out << "[";
+            bool first = true;
+            if (!this->symbolicStates.isZero()) {
+                if (this->symbolicValues.isZero()) {
+                    out << "0";
+                } else {
+                    for (auto valuationValuePair : this->symbolicValues) {
+                        if (!first) {
+                            out << ", ";
+                        } else {
+                            first = false;
+                        }
+                        out << valuationValuePair.second;
+                    }
+                }
+            }
+            if (!this->explicitStates.isZero()) {
+                for (auto const& element : this->explicitValues) {
+                    if (!first) {
+                        out << ", ";
+                    } else {
+                        first = false;
+                    }
+                    out << element;
+                }
+            }
+            out << "]";
+            return out;
+        }
+        
+        template<storm::dd::DdType Type>
+        void HybridQuantitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) {
+            STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter hybrid check result with non-symbolic filter.");
+            
+            // First, we filter the symbolic values.
+            this->symbolicStates = this->symbolicStates && filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
+            this->symbolicValues *= symbolicStates.toAdd();
+            
+            // Next, we filter the explicit values.
+
+            // Start by computing the new set of states that is stored explictly and the corresponding ODD.
+            this->explicitStates = this->explicitStates && filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
+            storm::dd::Odd<Type> newOdd(explicitStates);
+            
+            // Then compute the new vector of explicit values and set the new data fields.
+            this->explicitValues = this->odd.filterExplicitVector(explicitStates, this->explicitValues);
+            this->odd = newOdd;
+        }
+        
+        // Explicitly instantiate the class.
+        template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>;
+    }
+}

src/modelchecker/results/HybridQuantitativeCheckResult.h

@@ -0,0 +1,69 @@
+#ifndef STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_
+#define STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddOdd.h"
+#include "src/modelchecker/results/QuantitativeCheckResult.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type>
+        class HybridQuantitativeCheckResult : public QuantitativeCheckResult {
+        public:
+            HybridQuantitativeCheckResult() = default;
+            HybridQuantitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& symbolicStates, storm::dd::Add<Type> const& symbolicValues, storm::dd::Bdd<Type> const& explicitStates, storm::dd::Odd<Type> const& odd, std::vector<double> const& explicitValues);
+            
+            HybridQuantitativeCheckResult(HybridQuantitativeCheckResult const& other) = default;
+            HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult const& other) = default;
+#ifndef WINDOWS
+            HybridQuantitativeCheckResult(HybridQuantitativeCheckResult&& other) = default;
+            HybridQuantitativeCheckResult& operator=(HybridQuantitativeCheckResult&& other) = default;
+#endif
+            
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
+            
+            virtual bool isHybrid() const override;
+            virtual bool isResultForAllStates() const override;
+            
+            virtual bool isHybridQuantitativeCheckResult() const override;
+            
+            storm::dd::Bdd<Type> const& getSymbolicStates() const;
+            
+            storm::dd::Add<Type> const& getSymbolicValueVector() const;
+            
+            storm::dd::Bdd<Type> const& getExplicitStates() const;
+            
+            storm::dd::Odd<Type> const& getOdd() const;
+            
+            std::vector<double> const& getExplicitValueVector() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+            virtual void filter(QualitativeCheckResult const& filter) override;
+            
+        private:
+            // The set of all reachable states.
+            storm::dd::Bdd<Type> reachableStates;
+            
+            // The set of all states whose result is stored symbolically.
+            storm::dd::Bdd<Type> symbolicStates;
+
+            // The symbolic value vector.
+            storm::dd::Add<Type> symbolicValues;
+            
+            // The set of all states whose result is stored explicitly.
+            storm::dd::Bdd<Type> explicitStates;
+            
+            // The ODD that enables translation of the explicit values to a symbolic format.
+            storm::dd::Odd<Type> odd;
+
+            // The explicit value vector.
+            std::vector<double> explicitValues;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */

src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -42,7 +42,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type>
-        storm::dd::Dd<Type> const& SymbolicQuantitativeCheckResult<Type>::getValueVector() const {
+        storm::dd::Add<Type> const& SymbolicQuantitativeCheckResult<Type>::getValueVector() const {
             return values;
         }
         

src/modelchecker/results/SymbolicQuantitativeCheckResult.h

@@ -28,7 +28,7 @@ namespace storm {
             
             virtual bool isSymbolicQuantitativeCheckResult() const override;
             
-            storm::dd::Dd<Type> const& getValueVector() const;
+            storm::dd::Add<Type> const& getValueVector() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             

src/storage/SparseMatrix.cpp

@@ -730,7 +730,6 @@ namespace storm {
         }
 #endif
         
-        
         template<typename ValueType>
         std::vector<ValueType> SparseMatrix<ValueType>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<ValueType> const& otherMatrix) const {
             std::vector<ValueType> result(rowCount, storm::utility::zero<ValueType>());
@@ -755,7 +754,6 @@ namespace storm {
             return result;
         }
         
-        
         template<typename ValueType>
         void SparseMatrix<ValueType>::multiplyWithVector(std::vector<ValueType> const& vector, std::vector<ValueType>& result) const {
 #ifdef STORM_HAVE_INTELTBB

src/storage/dd/CuddBdd.cpp

@@ -1,8 +1,10 @@
 #include <cstring>
 #include <algorithm>
+#include <functional>
 
-#include "src/storage/dd/CuddBdd.h"
 #include "src/storage/dd/CuddAdd.h"
+#include "src/storage/dd/CuddBdd.h"
+#include "src/storage/dd/CuddOdd.h"
 #include "src/storage/dd/CuddDdManager.h"
 
 #include "src/utility/macros.h"
@@ -14,6 +16,24 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        Bdd<DdType::CUDD>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd<DdType::CUDD>(ddManager, metaVariables) {
+            switch (comparisonType) {
+                case storm::logic::ComparisonType::Less:
+                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
+                    break;
+                case storm::logic::ComparisonType::LessEqual:
+                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
+                    break;
+                case storm::logic::ComparisonType::Greater:
+                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
+                    break;
+                case storm::logic::ComparisonType::GreaterEqual:
+                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
+                    break;
+            }
+
+        }
+        
         Add<DdType::CUDD> Bdd<DdType::CUDD>::toAdd() const {
             return Add<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables());
         }
@@ -253,6 +273,70 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        BDD Bdd<DdType::CUDD>::fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter) {
+            std::vector<uint_fast64_t> ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables);
+            uint_fast64_t offset = 0;
+            return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter));
+        }
+        
+        template<typename ValueType>
+        DdNode* Bdd<DdType::CUDD>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter) {
+            if (currentLevel == maxLevel) {
+                // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
+                // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
+                // need to copy the next value of the vector iff the then-offset is greater than zero.
+                if (odd.getThenOffset() > 0) {
+                    if (filter(values[currentOffset++])) {
+                        return Cudd_ReadOne(manager);
+                    } else {
+                        return Cudd_ReadLogicZero(manager);
+                    }
+                } else {
+                    return Cudd_ReadZero(manager);
+                }
+            } else {
+                // If the total offset is zero, we can just return the constant zero DD.
+                if (odd.getThenOffset() + odd.getElseOffset() == 0) {
+                    return Cudd_ReadZero(manager);
+                }
+                
+                // Determine the new else-successor.
+                DdNode* elseSuccessor = nullptr;
+                if (odd.getElseOffset() > 0) {
+                    elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter);
+                } else {
+                    elseSuccessor = Cudd_ReadLogicZero(manager);
+                }
+                Cudd_Ref(elseSuccessor);
+                
+                // Determine the new then-successor.
+                DdNode* thenSuccessor = nullptr;
+                if (odd.getThenOffset() > 0) {
+                    thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter);
+                } else {
+                    thenSuccessor = Cudd_ReadLogicZero(manager);
+                }
+                Cudd_Ref(thenSuccessor);
+                
+                // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
+                DdNode* result = Cudd_bddIthVar(manager, static_cast<int>(ddVariableIndices[currentLevel]));
+                Cudd_Ref(result);
+                DdNode* newResult = Cudd_bddIte(manager, result, thenSuccessor, elseSuccessor);
+                Cudd_Ref(newResult);
+                
+                // Dispose of the intermediate results
+                Cudd_RecursiveDeref(manager, result);
+                Cudd_RecursiveDeref(manager, thenSuccessor);
+                Cudd_RecursiveDeref(manager, elseSuccessor);
+                
+                // Before returning, we remove the protection imposed by the previous call to Cudd_Ref.
+                Cudd_Deref(newResult);
+                
+                return newResult;
+            }
+        }
+        
         std::ostream& operator<<(std::ostream& out, const Bdd<DdType::CUDD>& bdd) {
             bdd.exportToDot();
             return out;

src/storage/dd/CuddBdd.h

@@ -1,6 +1,7 @@
 #ifndef STORM_STORAGE_DD_CUDDBDD_H_
 #define STORM_STORAGE_DD_CUDDBDD_H_
 
+#include "src/logic/ComparisonType.h"
 #include "src/storage/dd/Bdd.h"
 #include "src/storage/dd/CuddDd.h"
 #include "src/storage/dd/CuddAdd.h"
@@ -20,6 +21,18 @@ namespace storm {
         template<>
         class Bdd<DdType::CUDD> : public Dd<DdType::CUDD> {
         public:
+            /*!
+             * Constructs a BDD representation of all encodings that are in the requested relation with the given value.
+             *
+             * @param ddManager The DD manager responsible for the resulting BDD.
+             * @param explicitValues The explicit values to compare to the given value.
+             * @param odd The ODD used for the translation from the explicit representation to a symbolic one.
+             * @param metaVariables The meta variables to use for the symbolic encoding.
+             * @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
+             * @param value The value to compare with.
+             */
+            Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+            
             // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
             friend class DdManager<DdType::CUDD>;
             friend class DdForwardIterator<DdType::CUDD>;
@@ -274,6 +287,34 @@ namespace storm {
              */
             Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
             
+            /*!
+             * Builds a BDD representing the values that make the given filter function evaluate to true.
+             *
+             * @param ddManager The manager responsible for the BDD.
+             * @param values The values that are to be checked against the filter function.
+             * @param odd The ODD used for the translation.
+             * @param metaVariables The meta variables used for the translation.
+             * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
+             * @return The resulting (CUDD) BDD.
+             */
+            template<typename ValueType>
+            static BDD fromVector(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);
+            
+            /*!
+             * Builds a BDD representing the values that make the given filter function evaluate to true.
+             *
+             * @param manager The manager responsible for the BDD.
+             * @param currentOffset The current offset in the vector.
+             * @param currentLevel The current level in the DD.
+             * @param maxLevel The maximal level in the DD.
+             * @param values The values that are to be checked against the filter function.
+             * @param odd The ODD used for the translation.
+             * @param ddVariableIndices The (sorted) list of DD variable indices to use.
+             * @return The resulting (CUDD) BDD node.
+             */
+            template<typename ValueType>
+            static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter);
+            
             // The BDD created by CUDD.
             BDD cuddBdd;
         };

src/storage/dd/CuddOdd.cpp

@@ -37,7 +37,7 @@ namespace storm {
             
             // Now construct the ODD structure from the BDD.
             std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
-
+            
             // Finally, move the children of the root ODD into this ODD.
             this->elseNode = std::move(rootOdd->elseNode);
             this->thenNode = std::move(rootOdd->thenNode);
@@ -95,6 +95,54 @@ namespace storm {
             return this->elseNode == nullptr && this->thenNode == nullptr;
         }
         
+        std::vector<double> Odd<DdType::CUDD>::filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> const& values) const {
+            std::vector<double> result(selectedValues.getNonZeroCount());
+            
+            // First, we need to determine the involved DD variables indices.
+            std::vector<uint_fast64_t> ddVariableIndices = selectedValues.getSortedVariableIndices();
+            
+            uint_fast64_t currentIndex = 0;
+            addSelectedValuesToVectorRec(selectedValues.getCuddDdNode(), selectedValues.getDdManager()->getCuddManager(), 0, Cudd_IsComplement(selectedValues.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, 0, *this, result, currentIndex, values);
+            return result;
+        }
+        
+        void Odd<DdType::CUDD>::addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values) {
+            // If there are no more values to select, we can directly return.
+            if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
+                return;
+            } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
+                return;
+            }
+            
+            if (currentLevel == maxLevel) {
+                // If the DD is not the zero leaf, then the then-offset is 1.
+                bool selected = false;
+                if (dd != Cudd_ReadLogicZero(manager.getManager())) {
+                    selected = !complement;
+                }
+                
+                if (selected) {
+                    result[currentIndex++] = values[currentOffset];
+                }
+            } else if (ddVariableIndices[currentLevel] < dd->index) {
+                // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
+                // and for the one in which it is not set.
+                addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
+                addSelectedValuesToVectorRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
+            } else {
+                // Otherwise, we compute the ODDs for both the then- and else successors.
+                DdNode* thenDdNode = Cudd_T(dd);
+                DdNode* elseDdNode = Cudd_E(dd);
+                
+                // Determine whether we have to evaluate the successors as if they were complemented.
+                bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
+                bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
+                
+                addSelectedValuesToVectorRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, currentOffset, odd.getElseSuccessor(), result, currentIndex, values);
+                addSelectedValuesToVectorRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), result, currentIndex, values);
+            }
+        }
+        
         std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
             // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
             auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
@@ -140,7 +188,7 @@ namespace storm {
             boost::hash_combine(result, key.second);
             return result;
         }
-    
+        
         std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels) {
             // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
             auto const& iterator = uniqueTableForLevels[currentLevel].find(std::make_pair(dd, complement));

src/storage/dd/CuddOdd.h

@@ -103,6 +103,15 @@ namespace storm {
              */
             bool isTerminalNode() const;
             
+            /*!
+             * Filters the given explicit vector using the symbolic representation of which values to select.
+             *
+             * @param selectedValues A symbolic representation of which values to select.
+             * @param values The value vector from which to select the values.
+             * @return The resulting vector.
+             */
+            std::vector<double> filterExplicitVector(storm::dd::Bdd<DdType::CUDD> const& selectedValues, std::vector<double> const& values) const;
+            
         private:
             // Declare a hash functor that is used for the unique tables in the construction process.
             class HashFunctor {
@@ -150,6 +159,23 @@ namespace storm {
              */
             static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::unordered_map<std::pair<DdNode*, bool>, std::shared_ptr<Odd<DdType::CUDD>>, HashFunctor>>& uniqueTableForLevels);
             
+            
+            /*!
+             * Adds the selected values the target vector.
+             *
+             * @param dd The current node of the DD representing the selected values.
+             * @param manager The manager responsible for the DD.
+             * @param currentLevel The currently considered level in the DD.
+             * @param maxLevel The number of levels that need to be considered.
+             * @param ddVariableIndices The sorted list of variable indices to use.
+             * @param currentOffset The offset along the path taken in the DD representing the selected values.
+             * @param odd The current ODD node.
+             * @param result The target vector to which to write the values.
+             * @param currentIndex The index at which the next element is to be written.
+             * @param values The value vector from which to select the values.
+             */
+            static void addSelectedValuesToVectorRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd<DdType::CUDD> const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values);
+            
             // The then- and else-nodes.
             std::shared_ptr<Odd<DdType::CUDD>> elseNode;
             std::shared_ptr<Odd<DdType::CUDD>> thenNode;