some more form on formulas. seems to work for formula objects changed yet...

src/formula/AbstractStateFormula.h

@@ -59,10 +59,11 @@ 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 {
-		std::cerr << "The model checker " << typeid(modelChecker).name() << " does not support " << typeid(*this).name() << std::endl;
+	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

@@ -8,7 +8,8 @@
 #ifndef STORM_FORMULA_AND_H_
 #define STORM_FORMULA_AND_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
 #include <string>
 
 namespace storm {
@@ -148,8 +149,8 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual storm::storage::BitVector *check(const IAndModelChecker<T>& modelChecker) const {
-		return modelChecker.checkAnd(*this);
+	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) {
+		return this->template cast<IAndModelChecker>(modelChecker)->checkAnd(*this);
 	}
 
 private:

src/formula/BoundOperator.h

@@ -8,9 +8,10 @@
 #ifndef STORM_FORMULA_BOUNDOPERATOR_H_
 #define STORM_FORMULA_BOUNDOPERATOR_H_
 
-#include "AbstractStateFormula.h"
-#include "AbstractPathFormula.h"
-#include "utility/ConstTemplates.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/utility/ConstTemplates.h"
 
 namespace storm {
 
@@ -153,8 +154,8 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual storm::storage::BitVector *check(const IBoundUntilModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkBoundOperator(*this);
+	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+	  return this->template cast<IBoundUntilModelChecker>(modelChecker)->checkBoundOperator(*this);
 	}
 
 private:

src/formula/BoundedEventually.h

@@ -12,6 +12,7 @@
 #include "AbstractStateFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
+#include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
 
@@ -143,8 +144,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const IBoundedEventuallyModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkBoundedEventually(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+	  return this->template cast<IBoundedEventuallyModelChecker>(modelChecker)->checkBoundedEventually(*this);
 	}
 
 private:

src/formula/BoundedUntil.h

@@ -10,6 +10,7 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 
@@ -174,8 +175,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const IBoundedUntilModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkBoundedUntil(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+	  return this->template cast<IBoundedUntilModelChecker>(modelChecker)->checkBoundedUntil(*this);
 	}
 
 private:

src/formula/Globally.h

@@ -118,8 +118,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const IGloballyModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkGlobally(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return this->template cast<IGloballyModelChecker>(modelChecker)->checkGlobally(*this);  
 	}
 
 private:

src/formula/Not.h

@@ -9,6 +9,7 @@
 #define STORM_FORMULA_NOT_H_
 
 #include "AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
 
@@ -113,8 +114,8 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual storm::storage::BitVector *check(const INotModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkNot(*this);
+	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return this->template cast<INotModelChecker>(modelChecker)->checkNot(*this);  
 	}
 
 private:

src/formula/ReachabilityReward.h

@@ -8,8 +8,9 @@
 #ifndef STORM_FORMULA_REACHABILITYREWARD_H_
 #define STORM_FORMULA_REACHABILITYREWARD_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
 
@@ -115,8 +116,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const IReachabilityRewardModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkReachabilityReward(*this);
+	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+	  return this->template cast<IReachabilityRewardModelChecker>(modelChecker)->checkReachabilityReward(*this);
 	}
 
 private:

src/modelChecker/DtmcPrctlModelChecker.h

@@ -54,6 +54,7 @@ template<class Type>
 class DtmcPrctlModelChecker : 
 	public virtual AbstractModelChecker<Type>, 
 	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
 	public virtual storm::formula::IEventuallyModelChecker<Type>
 	{
 public: