implemented formula checker

src/formula/AbstractFormula.h

@@ -15,6 +15,7 @@ template <class T> class AbstractFormula;
 }}
 
 #include "src/modelChecker/AbstractModelChecker.h"
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace formula {
@@ -44,6 +45,8 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const = 0;
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0;
 };
 
 } //namespace formula

src/formula/AbstractFormulaChecker.h

@@ -0,0 +1,18 @@
+#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
+#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
+
+#include "src/formula/AbstractFormula.h"
+
+namespace storm {
+namespace formula {
+
+template <class T>
+class AbstractFormulaChecker {
+	public:
+		virtual bool conforms(const AbstractFormula<T>* formula) const = 0;
+};
+
+}
+}
+
+#endif

src/formula/Ap.h

@@ -8,7 +8,8 @@
 #ifndef STORM_FORMULA_AP_H_
 #define STORM_FORMULA_AP_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -90,6 +91,10 @@ public:
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return true;
+	}
+
 private:
 	std::string ap;
 };

src/formula/BoundedUntil.h

@@ -8,11 +8,12 @@
 #ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
 #define STORM_FORMULA_BOUNDEDUNTIL_H_
 
-#include "AbstractPathFormula.h"
+#include "src/formula/AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
@@ -179,6 +180,10 @@ public:
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->left) && checker.conforms(this->right);
+	}
+
 private:
 	AbstractStateFormula<T>* left;
 	AbstractStateFormula<T>* right;

src/formula/Eventually.h

@@ -123,6 +123,10 @@ public:
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+
 private:
 	AbstractStateFormula<T>* child;
 };

src/formula/NoBoundOperator.h

@@ -10,6 +10,7 @@
 
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
@@ -117,6 +118,10 @@ public:
 	 */
 	virtual std::string toString() const = 0;
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->pathFormula);
+	}
+
 private:
 	AbstractPathFormula<T>* pathFormula;
 };

src/formula/Not.h

@@ -9,6 +9,7 @@
 #define STORM_FORMULA_NOT_H_
 
 #include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -118,6 +119,10 @@ public:
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+
 private:
 	AbstractStateFormula<T>* child;
 };

src/formula/PrctlFormulaChecker.h

@@ -0,0 +1,35 @@
+#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_
+#define STORM_FORMULA_PRCTLFORMULACHECKER_H_
+
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/Formulas.h"
+
+#include <iostream>
+
+namespace storm {
+namespace formula {
+
+template <class T>
+class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
+	public:
+		virtual bool conforms(const AbstractFormula<T>* formula) const {
+			if (
+					dynamic_cast<const And<T>*>(formula) ||
+					dynamic_cast<const Ap<T>*>(formula) ||
+					dynamic_cast<const Eventually<T>*>(formula) ||
+					dynamic_cast<const Not<T>*>(formula) ||
+					dynamic_cast<const Or<T>*>(formula) ||
+					dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula)
+				) {
+				return formula->conforms(*this);
+			}
+			return false;
+		}
+	
+	private:
+};
+
+}
+}
+
+#endif

src/formula/ReachabilityReward.h

@@ -10,6 +10,7 @@
 
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -120,6 +121,10 @@ public:
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
 	}
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+
 private:
 	AbstractStateFormula<T>* child;
 };

src/formula/Until.h

@@ -10,6 +10,7 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
@@ -152,6 +153,10 @@ public:
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
 	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
+
 private:
 	AbstractStateFormula<T>* left;
 	AbstractStateFormula<T>* right;