Further work on MTBDD-based mc.

Former-commit-id: cf2e16850d

src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp

@@ -0,0 +1,54 @@
+#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
+
+#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Mdp.h"
+
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type>
+        SymbolicPropositionalModelChecker<Type>::SymbolicPropositionalModelChecker(storm::models::symbolic::Model<Type> const& model) : model(model) {
+            // Intentionally left empty.
+        }
+        
+        template<storm::dd::DdType Type>
+        bool SymbolicPropositionalModelChecker<Type>::canHandle(storm::logic::Formula const& formula) const {
+            return formula.isPropositionalFormula();
+        }
+        
+        template<storm::dd::DdType Type>
+        std::unique_ptr<CheckResult> SymbolicPropositionalModelChecker<Type>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
+            if (stateFormula.isTrueFormula()) {
+                return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getReachableStates()));
+            } else {
+                return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getManager().getZero()));
+            }
+        }
+        
+        template<storm::dd::DdType Type>
+        std::unique_ptr<CheckResult> SymbolicPropositionalModelChecker<Type>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+            STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
+            return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getStates(stateFormula.getLabel())));
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::models::symbolic::Model<Type> const& SymbolicPropositionalModelChecker<Type>::getModel() const {
+            return model;
+        }
+        
+        template<storm::dd::DdType Type>
+        template<typename ModelType>
+        ModelType const& SymbolicPropositionalModelChecker<Type>::getModelAs() const {
+            return dynamic_cast<ModelType const&>(model);
+        }
+        
+        // Explicitly instantiate the template class.
+        template storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD> const& SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD>::getModelAs() const;
+        template storm::models::symbolic::Mdp<storm::dd::DdType::CUDD> const& SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD>::getModelAs() const;
+        template class SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD>;
+    }
+}

src/modelchecker/propositional/SymbolicPropositionalModelChecker.h

@@ -0,0 +1,44 @@
+#ifndef STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
+#define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
+
+#include "src/modelchecker/AbstractModelChecker.h"
+
+#include "src/models/symbolic/Model.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<storm::dd::DdType Type>
+        class SymbolicPropositionalModelChecker : public AbstractModelChecker {
+        public:
+            explicit SymbolicPropositionalModelChecker(storm::models::symbolic::Model<Type> const& model);
+            
+            // The implemented methods of the AbstractModelChecker interface.
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
+            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
+            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+            
+        protected:
+            /*!
+             * Retrieves the model associated with this model checker instance.
+             *
+             * @return The model associated with this model checker instance.
+             */
+            virtual storm::models::symbolic::Model<Type> const& getModel() const;
+            
+            /*!
+             * Retrieves the model associated with this model checker instance as the given template parameter type.
+             *
+             * @return The model associated with this model checker instance.
+             */
+            template<typename ModelType>
+            ModelType const& getModelAs() const;
+            
+        private:
+            // The model that is to be analyzed by the model checker.
+            storm::models::symbolic::Model<Type> const& model;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_ */

src/modelchecker/results/CheckResult.cpp

@@ -73,6 +73,14 @@ namespace storm {
             return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType> const&>(*this);
         }
         
+        QualitativeCheckResult& CheckResult::asQualitativeCheckResult() {
+            return dynamic_cast<QualitativeCheckResult&>(*this);
+        }
+        
+        QualitativeCheckResult const& CheckResult::asQualitativeCheckResult() const {
+            return dynamic_cast<QualitativeCheckResult const&>(*this);
+        }
+        
         QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() {
             return dynamic_cast<QuantitativeCheckResult&>(*this);
         }

src/modelchecker/results/ExplicitQualitativeCheckResult.cpp

@@ -30,7 +30,7 @@ namespace storm {
         }
         
         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(second.isExplicitQualitativeCheckResult(), 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);
             if (first.isResultForAllStates()) {
@@ -104,6 +104,7 @@ namespace storm {
         }
         
         std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const {
+            out << "[";
             if (this->isResultForAllStates()) {
                 out << boost::get<vector_type>(truthValues);
             } else {
@@ -111,27 +112,18 @@ namespace storm {
                 out << std::boolalpha;
                 
                 map_type const& map = boost::get<map_type>(truthValues);
-                
-#ifndef WINDOWS
-                typename map_type::const_iterator it = map.begin();
-                typename map_type::const_iterator itPlusOne = map.begin();
-                ++itPlusOne;
-                typename map_type::const_iterator ite = map.end();
-#else
-                map_type::const_iterator it = map.begin();
-                map_type::const_iterator itPlusOne = map.begin();
-                ++itPlusOne;
-                map_type::const_iterator ite = map.end();
-#endif
-                
-                for (; it != ite; ++itPlusOne, ++it) {
-                    out << it->second;
-                    if (itPlusOne != ite) {
+                bool first = true;
+                for (auto const& element : map) {
+                    if (!first) {
                         out << ", ";
+                    } else {
+                        first = false;
                     }
+                    out << element.second;
                 }
                 std::cout.flags(oldflags);
             }
+            out << "]";
             return out;
         }
         

src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@@ -83,29 +83,25 @@ namespace storm {
             out << "[";
             if (this->isResultForAllStates()) {
                 vector_type const& valuesAsVector = boost::get<vector_type>(values);
-                typename vector_type::const_iterator it = valuesAsVector.begin();
-                typename vector_type::const_iterator itPlusOne = valuesAsVector.begin();
-                ++itPlusOne;
-                typename vector_type::const_iterator ite = valuesAsVector.end();
-                
-                for (; it != ite; ++itPlusOne, ++it) {
-                    out << *it;
-                    if (itPlusOne != ite) {
+                bool first = true;
+                for (auto const& element : valuesAsVector) {
+                    if (!first) {
                         out << ", ";
+                    } else {
+                        first = false;
                     }
+                    out << element;
                 }
             } else {
                 map_type const& valuesAsMap = boost::get<map_type>(values);
-                typename map_type::const_iterator it = valuesAsMap.begin();
-                typename map_type::const_iterator itPlusOne = valuesAsMap.begin();
-                ++itPlusOne;
-                typename map_type::const_iterator ite = valuesAsMap.end();
-                
-                for (; it != ite; ++itPlusOne, ++it) {
-                    out << it->second;
-                    if (itPlusOne != ite) {
+                bool first = true;
+                for (auto const& element : valuesAsMap) {
+                    if (!first) {
                         out << ", ";
+                    } else {
+                        first = false;
                     }
+                    out << element.second;
                 }
             }
             out << "]";

src/modelchecker/results/SymbolicQualitativeCheckResult.cpp

@@ -1,55 +1,66 @@
-#include "src/modelcheckers/result/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/storage/dd/CuddDd.h"
+#include "src/exceptions/InvalidOperationException.h"
 
 namespace storm {
-    namespace modelcheckers {
+    namespace modelchecker {
         template <storm::dd::DdType Type>
-        SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& values) {
-            
+        SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& truthValues) : allStates(allStates), truthValues(truthValues) {
+            // Intentionally left empty.
         }
         
         template <storm::dd::DdType Type>
-        bool isSymbolic() const {
-            
+        bool SymbolicQualitativeCheckResult<Type>::isSymbolic() const {
+            return true;
         }
 
         template <storm::dd::DdType Type>
-        bool isResultForAllStates() const {
-            
+        bool SymbolicQualitativeCheckResult<Type>::isResultForAllStates() const {
+            return true;
         }
         
         template <storm::dd::DdType Type>
-        bool isSymbolicQualitativeCheckResult() const {
-            
+        bool SymbolicQualitativeCheckResult<Type>::isSymbolicQualitativeCheckResult() const {
+            return true;
         }
         
         template <storm::dd::DdType Type>
-        QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) {
-            
+        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();
         }
 
         template <storm::dd::DdType Type>
-        QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) {
-            
+        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();
         }
 
         template <storm::dd::DdType Type>
-        void complement() {
-            
+        void SymbolicQualitativeCheckResult<Type>::complement() {
+            this->truthValues = !this->truthValues && allStates;
         }
         
         template <storm::dd::DdType Type>
-        storm::dd::Dd<Type> const& getTruthValuesVector() const {
-            
+        storm::dd::Dd<Type> const& SymbolicQualitativeCheckResult<Type>::getTruthValuesVector() const {
+            return truthValues;
         }
         
         template <storm::dd::DdType Type>
-        std::ostream& writeToStream(std::ostream& out) const {
-            
+        std::ostream& SymbolicQualitativeCheckResult<Type>::writeToStream(std::ostream& out) const {
+            if (this->truthValues.isZero()) {
+                out << "[false]" << std::endl;
+            } else {
+                out << "[true]" << std::endl;
+            }
+            return out;
         }
         
         template <storm::dd::DdType Type>
-        void filter(QualitativeCheckResult const& filter) {
-            
+        void SymbolicQualitativeCheckResult<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();
         }
     }
 }

src/modelchecker/results/SymbolicQualitativeCheckResult.h

@@ -2,6 +2,7 @@
 #define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
 
 #include "src/storage/dd/DdType.h"
+#include "src/storage/dd/Dd.h"
 #include "src/modelchecker/results/QualitativeCheckResult.h"
 #include "src/utility/OsDetection.h"
 
@@ -11,7 +12,7 @@ namespace storm {
         class SymbolicQualitativeCheckResult : public QualitativeCheckResult {
         public:
             SymbolicQualitativeCheckResult() = default;
-            SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& values);
+            SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& truthValues);
             
             SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default;
             SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default;
@@ -36,6 +37,9 @@ namespace storm {
             virtual void filter(QualitativeCheckResult const& filter) override;
             
         private:
+            // The set of all states.
+            storm::dd::Dd<Type> allStates;
+            
             // The values of the qualitative check result.
             storm::dd::Dd<Type> truthValues;
         };

src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -0,0 +1,70 @@
+#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/storage/dd/CuddDd.h"
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type>
+        SymbolicQuantitativeCheckResult<Type>::SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& values) : allStates(allStates), 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)));
+            }
+            if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
+                result->complement();
+            }
+            return result;
+        }
+        
+        template<storm::dd::DdType Type>
+        bool SymbolicQuantitativeCheckResult<Type>::isSymbolic() const {
+            return true;
+        }
+
+        template<storm::dd::DdType Type>
+        bool SymbolicQuantitativeCheckResult<Type>::isResultForAllStates() const {
+            return true;
+        }
+        
+        template<storm::dd::DdType Type>
+        bool SymbolicQuantitativeCheckResult<Type>::isSymbolicQuantitativeCheckResult() const {
+            return true;
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::dd::Dd<Type> const& SymbolicQuantitativeCheckResult<Type>::getValueVector() const {
+            return values;
+        }
+        
+        template<storm::dd::DdType Type>
+        std::ostream& SymbolicQuantitativeCheckResult<Type>::writeToStream(std::ostream& out) const {
+            out << "[";
+            bool first = true;
+            for (auto valuationValuePair : this->values) {
+                if (!first) {
+                    out << ", ";
+                } else {
+                    first = false;
+                }
+                out << valuationValuePair.second;
+            }
+            out << "]";
+            return out;
+        }
+        
+        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();
+        }
+    }
+}

src/modelchecker/results/SymbolicQuantitativeCheckResult.h

@@ -2,6 +2,7 @@
 #define STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_
 
 #include "src/storage/dd/DdType.h"
+#include "src/storage/dd/Dd.h"
 #include "src/modelchecker/results/QuantitativeCheckResult.h"
 #include "src/utility/OsDetection.h"
 
@@ -10,8 +11,8 @@ namespace storm {
         template<storm::dd::DdType Type>
         class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult {
         public:
-            SymbolicQuantitativeCheckResult();
-            SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& values);
+            SymbolicQuantitativeCheckResult() = default;
+            SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& values);
             
             SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default;
             SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default;
@@ -34,6 +35,9 @@ namespace storm {
             virtual void filter(QualitativeCheckResult const& filter) override;
             
         private:
+            // The set of all states.
+            storm::dd::Dd<Type> allStates;
+            
             // The values of the quantitative check result.
             storm::dd::Dd<Type> values;
         };

src/utility/cli.h

@@ -440,8 +440,8 @@ namespace storm {
                     if (result) {
                         std::cout << " done." << std::endl;
                         std::cout << "Result (initial states): ";
-                        result->writeToStream(std::cout, sparseModel->getInitialStates());
-                        std::cout << std::endl << std::endl;
+                        result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+                        std::cout << *result << std::endl;
                     } else {
                         std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
                     }
@@ -470,8 +470,8 @@ namespace storm {
                 if (result) {
                     std::cout << " done." << std::endl;
                     std::cout << "Result (initial states): ";
-                    result->writeToStream(std::cout, model->getInitialStates());
-                    std::cout << std::endl << std::endl;
+                    result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates()));
+                    std::cout << *result << std::endl;
                 } else {
                     std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
                 }