From 9d65bdeef307d7732318aec85b84f099a866eff3 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sun, 27 Jan 2013 20:58:22 +0100
Subject: [PATCH] next iteration on formulas...

removed AbstractFormula::cast() in favor of AbstractModelChecker::as()
changed all formulas to use this new one
actually implement ::check(AbstractModelChecker) for all formulas
---
 src/formula/AbstractFormula.h           | 12 ------------
 src/formula/AbstractPathFormula.h       |  5 +----
 src/formula/AbstractStateFormula.h      |  4 ----
 src/formula/And.h                       |  2 +-
 src/formula/Ap.h                        |  2 +-
 src/formula/BoundOperator.h             |  2 +-
 src/formula/BoundedEventually.h         |  2 +-
 src/formula/BoundedUntil.h              |  2 +-
 src/formula/CumulativeReward.h          |  4 ++--
 src/formula/Eventually.h                |  2 +-
 src/formula/Globally.h                  |  2 +-
 src/formula/InstantaneousReward.h       |  4 ++--
 src/formula/Next.h                      |  4 ++--
 src/formula/NoBoundOperator.h           |  4 ++--
 src/formula/Not.h                       |  2 +-
 src/formula/Or.h                        |  4 ++--
 src/formula/ReachabilityReward.h        |  2 +-
 src/formula/Until.h                     |  4 ++--
 src/modelChecker/AbstractModelChecker.h | 14 ++++++++++++++
 19 files changed, 36 insertions(+), 41 deletions(-)

diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index 8bd8b8782..ee99f88f2 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -44,18 +44,6 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const = 0;
-	
-	template <template <class Type> class MC>
-	const MC<T>* cast(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		try {
-			const MC<T>& mc = dynamic_cast<const MC<T>&>(modelChecker);
-			return &mc;
-		} catch (std::bad_cast& bc) {
-			std::cerr << "Bad cast: tried to cast " << typeid(modelChecker).name() << " to " << typeid(MC<T>).name() << std::endl;
-			
-		}
-		return nullptr;
-	}
 };
 
 } //namespace formula
diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h
index cba3425fa..a12642002 100644
--- a/src/formula/AbstractPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -62,10 +62,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
-		return nullptr;
-	}
+	virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h
index e356d4325..4ce735c75 100644
--- a/src/formula/AbstractStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -60,10 +60,6 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const = 0; // {
-/*		std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
-		return nullptr;
-	}
-*/
 };
 
 } //namespace formula
diff --git a/src/formula/And.h b/src/formula/And.h
index ea017fe81..601872f79 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -150,7 +150,7 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) {
-		return this->template cast<IAndModelChecker>(modelChecker)->checkAnd(*this);
+		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
 private:
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index 8eb4dbe5b..ceca11193 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -87,7 +87,7 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		return this->template cast<IApModelChecker>(modelChecker)->checkAp(*this);
+		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
 private:
diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h
index 9a3472034..67d92df8a 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/BoundOperator.h
@@ -155,7 +155,7 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-	  return this->template cast<IBoundUntilModelChecker>(modelChecker)->checkBoundOperator(*this);
+		return modelChecker.template as<IBoundUntilModelChecker>()->checkBoundOperator(*this);
 	}
 
 private:
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 6ccc89714..5c92ea3d8 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -145,7 +145,7 @@ public:
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-	  return this->template cast<IBoundedEventuallyModelChecker>(modelChecker)->checkBoundedEventually(*this);
+		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 
 private:
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 763167cb2..89ae6e35d 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -176,7 +176,7 @@ public:
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-	  return this->template cast<IBoundedUntilModelChecker>(modelChecker)->checkBoundedUntil(*this);
+		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 
 private:
diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h
index 2587390ea..bdc1e70b1 100644
--- a/src/formula/CumulativeReward.h
+++ b/src/formula/CumulativeReward.h
@@ -108,8 +108,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const ICumulativeRewardModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkCumulativeReward(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
 	}
 
 private:
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 32e6d126a..ac9d38981 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -120,7 +120,7 @@ public:
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		return this->template cast<IEventuallyModelChecker>(modelChecker)->checkEventually(*this);
+		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 
 private:
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index 116509ed6..46d464fad 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -119,7 +119,7 @@ public:
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		return this->template cast<IGloballyModelChecker>(modelChecker)->checkGlobally(*this);  
+		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);  
 	}
 
 private:
diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h
index 319e38f49..da6d3269b 100644
--- a/src/formula/InstantaneousReward.h
+++ b/src/formula/InstantaneousReward.h
@@ -108,8 +108,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const IInstantaneousRewardModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkInstantaneousReward(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
 	}
 
 private:
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 501277bba..763d6068c 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -120,8 +120,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const INextModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkNext(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<INextModelChecker>()->checkNext(*this);
 	}
 
 private:
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index eeb8d2c54..c2cab764d 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -108,8 +108,8 @@ public:
 	 *
 	 * @returns A vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual std::vector<T>* check(const INoBoundOperatorModelChecker<T>& modelChecker) const {
-		return modelChecker.checkNoBoundOperator(*this);
+	virtual std::vector<T>* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<INoBoundOperatorModelChecker>()->checkNoBoundOperator(*this);
 	}
 
 	/*!
diff --git a/src/formula/Not.h b/src/formula/Not.h
index d79e31a34..f3f5186ec 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -115,7 +115,7 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		return this->template cast<INotModelChecker>(modelChecker)->checkNot(*this);  
+		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
 
 private:
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 79e30cdab..e5143ebeb 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -147,8 +147,8 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual storm::storage::BitVector *check(const IOrModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkOr(*this);
+	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 
 private:
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 37b7ee7e3..4c214ae12 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -117,7 +117,7 @@ public:
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-	  return this->template cast<IReachabilityRewardModelChecker>(modelChecker)->checkReachabilityReward(*this);
+		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
 	}
 
 private:
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 94f917a60..764175f1c 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -148,8 +148,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const IUntilModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkUntil(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
 
 private:
diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelChecker/AbstractModelChecker.h
index 6bac47a04..110d355dd 100644
--- a/src/modelChecker/AbstractModelChecker.h
+++ b/src/modelChecker/AbstractModelChecker.h
@@ -17,6 +17,8 @@ template <class Type> class AbstractModelChecker;
 #include "src/formula/Ap.h"
 #include "src/storage/BitVector.h"
 
+#include <iostream>
+
 namespace storm {
 namespace modelChecker {
 
@@ -34,6 +36,18 @@ class AbstractModelChecker :
 	public virtual storm::formula::IOrModelChecker<Type>,
 	public virtual storm::formula::IApModelChecker<Type>
 	{
+	
+public:
+	template <template <class T> class Target>
+	const Target<Type>* as() const {
+		try {
+			const Target<Type>* target = dynamic_cast<const Target<Type>*>(this);
+			return target;
+		} catch (std::bad_cast& bc) {
+			std::cerr << "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << std::endl;
+		}
+		return nullptr;
+	}
 };
 
 } //namespace modelChecker