From 4389f6ba5bac2145f91521c2533003b7eb3cffe4 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Thu, 7 Feb 2013 20:55:10 +0100
Subject: [PATCH] finished PrctlFormulaChecker.

I hope it checks the correct set of operators now...
---
 src/formula/PrctlFormulaChecker.h | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
index e99cb0666..ddb9d90ab 100644
--- a/src/formula/PrctlFormulaChecker.h
+++ b/src/formula/PrctlFormulaChecker.h
@@ -21,18 +21,21 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 		/*!
 		 *	Implementation of AbstractFormulaChecker::conforms() using code
 		 *	looking exactly like the sample code given there.
-		 *
-		 *	We currently allow And, Ap, Eventually, Not, Or,
-		 *	ProbabilisticNoBoundOperator.
 		 */
 		virtual bool conforms(const 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 ProbabilisticNoBoundOperator<T>*>(formula) ||
+					dynamic_cast<const ProbabilisticBoundOperator<T>*>(formula) ||
+					dynamic_cast<const Until<T>*>(formula)
 				) {
 				return formula->conforms(*this);
 			}