From 4cddd9ad78b5afdcc576bc176196f452a61203e1 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Fri, 3 May 2013 11:02:56 +0200
Subject: [PATCH] Changing AbstractFormulaChecker and PrctlFormulaChecker to
 completely work with the new structure of formulas.

---
 src/formula/AbstractFormulaChecker.h |  9 +++++++++
 src/formula/PrctlFormulaChecker.h    | 26 +++++++++++++-------------
 2 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index 3de6494cd..d79477b48 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -1,6 +1,15 @@
 #ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
 #define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
 
+namespace storm {
+namespace formula {
+
+template <class T> class AbstractFormulaChecker;
+
+} //namespace formula
+} //namespace storm
+
+
 #include "src/formula/abstract/AbstractFormula.h"
 
 namespace storm {
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
index b3ff944a2..493e4dcf9 100644
--- a/src/formula/PrctlFormulaChecker.h
+++ b/src/formula/PrctlFormulaChecker.h
@@ -22,20 +22,20 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 		 *	Implementation of AbstractFormulaChecker::conforms() using code
 		 *	looking exactly like the sample code given there.
 		 */
-		virtual bool conforms(const AbstractFormula<T>* formula) const {
+		virtual bool conforms(const storm::formula::abstract::AbstractFormula<T>* formula) const {
 			// What to support: Principles of Model Checking Def. 10.76 + syntactic sugar
 			if (
-					dynamic_cast<const And<T>*>(formula) ||
-					dynamic_cast<const Ap<T>*>(formula) ||
-					dynamic_cast<const BoundedUntil<T>*>(formula) ||
-					dynamic_cast<const Eventually<T>*>(formula) ||
-					dynamic_cast<const Globally<T>*>(formula) ||
-					dynamic_cast<const Next<T>*>(formula) ||
-					dynamic_cast<const Not<T>*>(formula) ||
-					dynamic_cast<const Or<T>*>(formula) ||
-					dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula) ||
-					dynamic_cast<const ProbabilisticBoundOperator<T>*>(formula) ||
-					dynamic_cast<const Until<T>*>(formula)
+					dynamic_cast<const storm::formula::prctl::And<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Ap<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::BoundedUntil<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Eventually<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Globally<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Next<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Not<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Or<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::ProbabilisticNoBoundOperator<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::ProbabilisticBoundOperator<T>*>(formula) ||
+					dynamic_cast<const storm::formula::prctl::Until<T>*>(formula)
 				) {
 				return formula->conforms(*this);
 			}
@@ -46,4 +46,4 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 } // namespace formula
 } // namespace storm
 
-#endif
\ No newline at end of file
+#endif