Merge branch 'mtbddIntegration' of https://sselab.de/lab9/private/git/storm into mtbddIntegration

Former-commit-id: 115d7a6c3b

src/logic/Formula.h

@@ -2,6 +2,7 @@
 #define STORM_LOGIC_FORMULA_H_
 
 #include <memory>
+#include <vector>
 #include <iostream>
 
 #include "src/modelchecker/results/CheckResult.h"

src/modelchecker/AbstractModelChecker.cpp

@@ -1,5 +1,7 @@
 #include "src/modelchecker/AbstractModelChecker.h"
 
+#include "src/modelchecker/results/QualitativeCheckResult.h"
+#include "src/modelchecker/results/QuantitativeCheckResult.h"
 #include "src/utility/constants.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
@@ -131,10 +133,12 @@ namespace storm {
             std::unique_ptr<CheckResult> leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula());
             std::unique_ptr<CheckResult> rightResult = this->check(stateFormula.getRightSubformula().asStateFormula());
             
+            STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results.");
+            
             if (stateFormula.isAnd()) {
-                *leftResult &= *rightResult;
+                leftResult->asQualitativeCheckResult() &= rightResult->asQualitativeCheckResult();
             } else if (stateFormula.isOr()) {
-                *leftResult |= *rightResult;
+                leftResult->asQualitativeCheckResult() |= rightResult->asQualitativeCheckResult();
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
             }
@@ -166,7 +170,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }
@@ -192,7 +196,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }
@@ -218,7 +222,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }
@@ -235,7 +239,7 @@ namespace storm {
             
             std::unique_ptr<CheckResult> result;
             if (stateFormula.hasBound()) {
-                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+                return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
                 return result;
             }
@@ -243,8 +247,9 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) {
             std::unique_ptr<CheckResult> subResult = this->check(stateFormula.getSubformula());
+            STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result.");
             if (stateFormula.isNot()) {
-                subResult->complement();
+                subResult->asQualitativeCheckResult().complement();
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
             }

src/modelchecker/results/CheckResult.cpp

@@ -3,31 +3,22 @@
 #include "storm-config.h"
 #include "src/adapters/CarlAdapter.h"
 
+#include "src/storage/dd/CuddDd.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
 
 namespace storm {
     namespace modelchecker {        
-        CheckResult& CheckResult::operator&=(CheckResult const& other) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results.");
-        }
-        
-        CheckResult& CheckResult::operator|=(CheckResult const& other) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results.");
-        }
-        
-        void CheckResult::complement() {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result.");
-        }
-        
-        std::unique_ptr<CheckResult> CheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result.");
+        bool CheckResult::isExplicit() const {
+            return false;
         }
         
-        bool CheckResult::isExplicit() const {
+        bool CheckResult::isSymbolic() const {
             return false;
         }
         
@@ -56,6 +47,14 @@ namespace storm {
             return false;
         }
         
+        bool CheckResult::isSymbolicQualitativeCheckResult() const {
+            return false;
+        }
+        
+        bool CheckResult::isSymbolicQuantitativeCheckResult() const {
+            return false;
+        }
+        
         ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() {
             return dynamic_cast<ExplicitQualitativeCheckResult&>(*this);
         }
@@ -74,25 +73,43 @@ namespace storm {
             return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType> const&>(*this);
         }
         
-        template<typename ValueType>
-        QuantitativeCheckResult<ValueType>& CheckResult::asQuantitativeCheckResult() {
-            return dynamic_cast<QuantitativeCheckResult<ValueType>&>(*this);
+        QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() {
+            return dynamic_cast<QuantitativeCheckResult&>(*this);
         }
         
-        template<typename ValueType>
-        QuantitativeCheckResult<ValueType> const& CheckResult::asQuantitativeCheckResult() const {
-            return dynamic_cast<QuantitativeCheckResult<ValueType> const&>(*this);
+        QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const {
+            return dynamic_cast<QuantitativeCheckResult const&>(*this);
+        }
+        
+        template <storm::dd::DdType Type>
+        SymbolicQualitativeCheckResult<Type>& CheckResult::asSymbolicQualitativeCheckResult() {
+            return dynamic_cast<SymbolicQualitativeCheckResult<Type>&>(*this);
+        }
+        
+        template <storm::dd::DdType Type>
+        SymbolicQualitativeCheckResult<Type> const& CheckResult::asSymbolicQualitativeCheckResult() const {
+            return dynamic_cast<SymbolicQualitativeCheckResult<Type> const&>(*this);
+        }
+        
+        template <storm::dd::DdType Type>
+        SymbolicQuantitativeCheckResult<Type>& CheckResult::asSymbolicQuantitativeCheckResult() {
+            return dynamic_cast<SymbolicQuantitativeCheckResult<Type>&>(*this);
+        }
+        
+        template <storm::dd::DdType Type>
+        SymbolicQuantitativeCheckResult<Type> const& CheckResult::asSymbolicQuantitativeCheckResult() const {
+            return dynamic_cast<SymbolicQuantitativeCheckResult<Type> const&>(*this);
         }
         
         // Explicitly instantiate the template functions.
-        template QuantitativeCheckResult<double>& CheckResult::asQuantitativeCheckResult();
-        template QuantitativeCheckResult<double> const& CheckResult::asQuantitativeCheckResult() const;
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+        template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asSymbolicQualitativeCheckResult();
+        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;
 
 #ifdef STORM_HAVE_CARL
-        template QuantitativeCheckResult<storm::RationalFunction>& CheckResult::asQuantitativeCheckResult();
-        template QuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asQuantitativeCheckResult() const;
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
 #endif

src/modelchecker/results/CheckResult.h

@@ -4,40 +4,46 @@
 #include <iostream>
 #include <memory>
 
-#include "src/storage/BitVector.h"
+#include "src/storage/dd/DdType.h"
 #include "src/logic/ComparisonType.h"
 
 namespace storm {
     namespace modelchecker {
         // Forward-declare the existing subclasses.
         class QualitativeCheckResult;
-        template <typename ValueType> class QuantitativeCheckResult;
+        class QuantitativeCheckResult;
         class ExplicitQualitativeCheckResult;
         template <typename ValueType> class ExplicitQuantitativeCheckResult;
+        template <storm::dd::DdType Type> class SymbolicQualitativeCheckResult;
+        template <storm::dd::DdType Type> class SymbolicQuantitativeCheckResult;
         
         // The base class of all check results.
         class CheckResult {
         public:
-            virtual CheckResult& operator&=(CheckResult const& other);
-            virtual CheckResult& operator|=(CheckResult const& other);
-            virtual void complement();
-            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
+            /*!
+             * Filters the current result wrt. to the filter, i.e. only keeps the entries that are selected by the filter.
+             * This means that the filter must be a qualitative result of proper type (symbolic/explicit).
+             *
+             * @param filter A qualitative result that serves as a filter.
+             */
+            virtual void filter(QualitativeCheckResult const& filter) = 0;
             
+            // Methods to retrieve the actual type of the check result.
             virtual bool isExplicit() const;
+            virtual bool isSymbolic() const;
             virtual bool isQuantitative() const;
             virtual bool isQualitative() const;
-            virtual bool isResultForAllStates() const;
-            
             virtual bool isExplicitQualitativeCheckResult() const;
             virtual bool isExplicitQuantitativeCheckResult() const;
+            virtual bool isSymbolicQualitativeCheckResult() const;
+            virtual bool isSymbolicQuantitativeCheckResult() const;
+            virtual bool isResultForAllStates() const;
             
             QualitativeCheckResult& asQualitativeCheckResult();
             QualitativeCheckResult const& asQualitativeCheckResult() const;
 
-            template<typename ValueType>
-            QuantitativeCheckResult<ValueType>& asQuantitativeCheckResult();
-            template<typename ValueType>
-            QuantitativeCheckResult<ValueType> const& asQuantitativeCheckResult() const;
+            QuantitativeCheckResult& asQuantitativeCheckResult();
+            QuantitativeCheckResult const& asQuantitativeCheckResult() const;
             
             ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;
@@ -48,8 +54,19 @@ namespace storm {
             template<typename ValueType>
             ExplicitQuantitativeCheckResult<ValueType> const& asExplicitQuantitativeCheckResult() const;
             
+            template <storm::dd::DdType Type>
+            SymbolicQualitativeCheckResult<Type>& asSymbolicQualitativeCheckResult();
+
+            template <storm::dd::DdType Type>
+            SymbolicQualitativeCheckResult<Type> const& asSymbolicQualitativeCheckResult() const;
+
+            template <storm::dd::DdType Type>
+            SymbolicQuantitativeCheckResult<Type>& asSymbolicQuantitativeCheckResult();
+
+            template <storm::dd::DdType Type>
+            SymbolicQuantitativeCheckResult<Type> const& asSymbolicQuantitativeCheckResult() const;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
-            virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const = 0;
         };
         
         std::ostream& operator<<(std::ostream& out, CheckResult& checkResult);

src/modelchecker/results/ExplicitQualitativeCheckResult.cpp

@@ -29,7 +29,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, CheckResult const& second, std::function<bool (bool, bool)> const& function) {
+        void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function<bool (bool, bool)> const& function) {
             STORM_LOG_THROW(typeid(second) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
             STORM_LOG_THROW(first.isResultForAllStates() == second.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
             ExplicitQualitativeCheckResult const& secondCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(second);
@@ -52,12 +52,12 @@ namespace storm {
             }
         }
         
-        CheckResult& ExplicitQualitativeCheckResult::operator&=(CheckResult const& other) {
+        QualitativeCheckResult& ExplicitQualitativeCheckResult::operator&=(QualitativeCheckResult const& other) {
             performLogicalOperation(*this, other, [] (bool a, bool b) { return a && b; });
             return *this;
         }
         
-        CheckResult& ExplicitQualitativeCheckResult::operator|=(CheckResult const& other) {
+        QualitativeCheckResult& ExplicitQualitativeCheckResult::operator|=(QualitativeCheckResult const& other) {
             performLogicalOperation(*this, other, [] (bool a, bool b) { return a || b; });
             return *this;
         }
@@ -135,43 +135,32 @@ namespace storm {
             return out;
         }
         
-        std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const {
-            std::ios::fmtflags oldflags(std::cout.flags());
-            
-            out << "[";
-            storm::storage::BitVector::const_iterator it = filter.begin();
-            storm::storage::BitVector::const_iterator itPlusOne = filter.begin();
-            ++itPlusOne;
-            storm::storage::BitVector::const_iterator ite = filter.end();
+        void ExplicitQualitativeCheckResult::filter(QualitativeCheckResult const& filter) {
+            STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter.");
+            STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
+            ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult();
+            vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector();
             
-            out << std::boolalpha;
             if (this->isResultForAllStates()) {
-                vector_type const& vector = boost::get<vector_type>(truthValues);
-                for (; it != ite; ++itPlusOne, ++it) {
-                    out << vector[*it];
-                    if (itPlusOne != ite) {
-                        out << ", ";
-                    }
+                map_type newMap;
+                for (auto const& element : filterTruthValues) {
+                    newMap.emplace(element, this->getTruthValuesVector().get(element));
                 }
+                this->truthValues = newMap;
             } else {
                 map_type const& map = boost::get<map_type>(truthValues);
-                bool allResultsAvailable = true;
-                for (; it != ite; ++itPlusOne, ++it) {
-                    auto const& keyValuePair = map.find(*it);
-                    if (keyValuePair != map.end()) {
-                        out << keyValuePair->second;
-                        if (itPlusOne != ite) {
-                            out << ", ";
-                        }
-                    } else {
-                        allResultsAvailable = false;
-                    }
+                
+                map_type newMap;
+                for (auto const& element : map) {
+                    if (filterTruthValues.get(element.first)) {
+                        newMap.insert(element);
                     }
                 }
-            out << "]";
                 
-            std::cout.flags(oldflags);
-            return out;
+                STORM_LOG_THROW(newMap.size() == filterTruthValues.getNumberOfSetBits(), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
+                
+                this->truthValues = newMap;
+            }
         }
     }
 }

src/modelchecker/results/ExplicitQualitativeCheckResult.h

@@ -39,18 +39,19 @@ namespace storm {
             
             virtual bool isExplicitQualitativeCheckResult() const override;
             
-            virtual CheckResult& operator&=(CheckResult const& other) override;
-            virtual CheckResult& operator|=(CheckResult const& other) override;
+            virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override;
+            virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override;
             virtual void complement() override;
 
             vector_type const& getTruthValuesVector() const;
             map_type const& getTruthValuesVectorMap() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
-            virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override;
+            
+            virtual void filter(QualitativeCheckResult const& filter) override;
 
         private:
-            static void performLogicalOperation(ExplicitQualitativeCheckResult& first, CheckResult const& second, std::function<bool (bool, bool)> const& function);
+            static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function<bool (bool, bool)> const& function);
             
             // The values of the quantitative check result.
             boost::variant<vector_type, map_type> truthValues;

src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -3,6 +3,7 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/storage/BitVector.h"
 #include "src/utility/macros.h"
+#include "src/utility/vector.h"
 #include "src/exceptions/InvalidOperationException.h"
 #include "src/adapters/CarlAdapter.h"
 
@@ -49,40 +50,32 @@ namespace storm {
         }
         
         template<typename ValueType>
-        std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const {
-            out << "[";
-            storm::storage::BitVector::const_iterator it = filter.begin();
-            storm::storage::BitVector::const_iterator itPlusOne = filter.begin();
-            ++itPlusOne;
-            storm::storage::BitVector::const_iterator ite = filter.end();
+        void ExplicitQuantitativeCheckResult<ValueType>::filter(QualitativeCheckResult const& filter) {
+            STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter.");
+            STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
+            ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector();
 
             if (this->isResultForAllStates()) {
-                vector_type const& valuesAsVector = boost::get<vector_type>(values);
-                for (; it != ite; ++itPlusOne, ++it) {
-                    out << valuesAsVector[*it];
-                    if (itPlusOne != ite) {
-                        out << ", ";
-                    }
+                map_type newMap;
+                for (auto const& element : filterTruthValues) {
+                    newMap.emplace(element, this->getValueVector()[element]);
                 }
+                this->values = newMap;
             } else {
-                map_type const& valuesAsMap = boost::get<map_type>(values);
-                bool allResultsAvailable = true;
-                for (; it != ite; ++itPlusOne, ++it) {
-                    auto const& keyValuePair = valuesAsMap.find(*it);
-                    if (keyValuePair != valuesAsMap.end()) {
-                        out << keyValuePair->second;
-                        if (itPlusOne != ite) {
-                            out << ", ";
-                        }
-                    } else {
-                        allResultsAvailable = false;
-                    }
+                map_type const& map = boost::get<map_type>(values);
+                
+                map_type newMap;
+                for (auto const& element : map) {
+                    if (filterTruthValues.get(element.first)) {
+                        newMap.insert(element);
                     }
-                STORM_LOG_THROW(allResultsAvailable, storm::exceptions::InvalidOperationException, "Unable to print result for some states, because the result is not available.");
                 }
                 
-            out << "]";
-            return out;
+                STORM_LOG_THROW(newMap.size() == filterTruthValues.getNumberOfSetBits(), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
+                
+                this->values = newMap;
+            }
         }
         
         template<typename ValueType>

src/modelchecker/results/ExplicitQuantitativeCheckResult.h

@@ -12,7 +12,7 @@
 namespace storm {
     namespace modelchecker {
         template<typename ValueType>
-        class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType> {
+        class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult {
         public:
             typedef std::vector<ValueType> vector_type;
             typedef std::map<storm::storage::sparse::state_type, ValueType> map_type;
@@ -45,7 +45,8 @@ namespace storm {
             map_type const& getValueMap() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
-            virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override;
+
+            virtual void filter(QualitativeCheckResult const& filter) override;
 
         private:
             // The values of the quantitative check result.

src/modelchecker/results/QualitativeCheckResult.cpp

@@ -1,7 +1,22 @@
 #include "src/modelchecker/results/QualitativeCheckResult.h"
 
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidOperationException.h"
+
 namespace storm {
     namespace modelchecker {
+        QualitativeCheckResult& QualitativeCheckResult::operator&=(QualitativeCheckResult const& other) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results.");
+        }
+        
+        QualitativeCheckResult& QualitativeCheckResult::operator|=(QualitativeCheckResult const& other) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results.");
+        }
+        
+        void QualitativeCheckResult::complement() {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result.");
+        }
+        
         bool QualitativeCheckResult::isQualitative() const {
             return true;
         }

src/modelchecker/results/QualitativeCheckResult.h

@@ -7,6 +7,10 @@ namespace storm {
     namespace modelchecker {
         class QualitativeCheckResult : public CheckResult {
         public:
+            virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other);
+            virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other);
+            virtual void complement();
+            
             virtual bool isQualitative() const override;
         };
     }

src/modelchecker/results/QuantitativeCheckResult.cpp

@@ -8,15 +8,12 @@
 
 namespace storm {
     namespace modelchecker {
-        template<typename ValueType>
-        bool QuantitativeCheckResult<ValueType>::isQuantitative() const {
-            return true;
+        std::unique_ptr<CheckResult> QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result.");
         }
         
-        template class QuantitativeCheckResult<double>;
-        
-#ifdef STORM_HAVE_CARL
-        template class QuantitativeCheckResult<storm::RationalFunction>;
-#endif
+        bool QuantitativeCheckResult::isQuantitative() const {
+            return true;
+        }
     }
 }

src/modelchecker/results/QuantitativeCheckResult.h

@@ -5,9 +5,10 @@
 
 namespace storm {
     namespace modelchecker {
-        template<typename ValueType>
         class QuantitativeCheckResult : public CheckResult {
         public:
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
+            
             virtual bool isQuantitative() const override;
         };
     }

src/modelchecker/results/SymbolicQualitativeCheckResult.cpp

@@ -0,0 +1,55 @@
+#include "src/modelcheckers/result/SymbolicQualitativeCheckResult.h"
+
+namespace storm {
+    namespace modelcheckers {
+        template <storm::dd::DdType Type>
+        SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& values) {
+            
+        }
+        
+        template <storm::dd::DdType Type>
+        bool isSymbolic() const {
+            
+        }
+
+        template <storm::dd::DdType Type>
+        bool isResultForAllStates() const {
+            
+        }
+        
+        template <storm::dd::DdType Type>
+        bool isSymbolicQualitativeCheckResult() const {
+            
+        }
+        
+        template <storm::dd::DdType Type>
+        QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) {
+            
+        }
+
+        template <storm::dd::DdType Type>
+        QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) {
+            
+        }
+
+        template <storm::dd::DdType Type>
+        void complement() {
+            
+        }
+        
+        template <storm::dd::DdType Type>
+        storm::dd::Dd<Type> const& getTruthValuesVector() const {
+            
+        }
+        
+        template <storm::dd::DdType Type>
+        std::ostream& writeToStream(std::ostream& out) const {
+            
+        }
+        
+        template <storm::dd::DdType Type>
+        void filter(QualitativeCheckResult const& filter) {
+            
+        }
+    }
+}

src/modelchecker/results/SymbolicQualitativeCheckResult.h

@@ -0,0 +1,45 @@
+#ifndef STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
+#define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
+
+#include "src/storage/dd/DdType.h"
+#include "src/modelchecker/results/QualitativeCheckResult.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace modelchecker {
+        template <storm::dd::DdType Type>
+        class SymbolicQualitativeCheckResult : public QualitativeCheckResult {
+        public:
+            SymbolicQualitativeCheckResult() = default;
+            SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& values);
+            
+            SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default;
+            SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default;
+#ifndef WINDOWS
+            SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult&& other) = default;
+            SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult&& other) = default;
+#endif
+            
+            virtual bool isSymbolic() const override;
+            virtual bool isResultForAllStates() const override;
+            
+            virtual bool isSymbolicQualitativeCheckResult() const override;
+            
+            virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override;
+            virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override;
+            virtual void complement() override;
+            
+            storm::dd::Dd<Type> const& getTruthValuesVector() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+            virtual void filter(QualitativeCheckResult const& filter) override;
+            
+        private:
+            // The values of the qualitative check result.
+            storm::dd::Dd<Type> truthValues;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */

src/modelchecker/results/SymbolicQuantitativeCheckResult.h

@@ -0,0 +1,43 @@
+#ifndef STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_
+#define STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_
+
+#include "src/storage/dd/DdType.h"
+#include "src/modelchecker/results/QuantitativeCheckResult.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type>
+        class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult {
+        public:
+            SymbolicQuantitativeCheckResult();
+            SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& values);
+            
+            SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default;
+            SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default;
+#ifndef WINDOWS
+            SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult&& other) = default;
+            SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default;
+#endif
+            
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
+            
+            virtual bool isSymbolic() const override;
+            virtual bool isResultForAllStates() const override;
+            
+            virtual bool isSymbolicQuantitativeCheckResult() const override;
+            
+            storm::dd::Dd<Type> const& getValueVector() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+            virtual void filter(QualitativeCheckResult const& filter) override;
+            
+        private:
+            // The values of the quantitative check result.
+            storm::dd::Dd<Type> values;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_ */