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

@@ -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

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

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

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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);
 	}
 
 	/*!

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:

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:

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:

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:

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