Compiling implementation of LTL parser

src/formula/Ltl.h

@@ -5,8 +5,10 @@
  *      Author: thomas
  */
 
-#ifndef LTL_H_
-#define LTL_H_
+#ifndef STORM_FORMULA_LTL_H_
+#define STORM_FORMULA_LTL_H_
+
+#include "src/modelchecker/ForwardDeclarations.h"
 
 #include "Ltl/And.h"
 #include "Ltl/Ap.h"
@@ -19,4 +21,6 @@
 #include "Ltl/Or.h"
 #include "Ltl/Until.h"
 
-#endif /* LTL_H_ */
+#include "modelchecker/AbstractModelChecker.h"
+
+#endif /* STORM_FORMULA_LTL_H_ */

src/formula/Ltl/AbstractLtlFormula.h

@@ -10,13 +10,14 @@
 
 #include <vector>
 #include "src/modelchecker/ForwardDeclarations.h"
+#include "src/formula/abstract/AbstractFormula.h"
 
 namespace storm {
 namespace formula {
 namespace ltl {
 
 template <class T>
-class AbstractLtlFormula {
+class AbstractLtlFormula : public virtual storm::formula::abstract::AbstractFormula<T> {
 public:
 	/**
 	 * Empty destructor
@@ -36,7 +37,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, bool qualitative) const = 0;
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const = 0;
 
 	/*!
 	 * Clones the called object.

src/formula/Ltl/Ap.h

@@ -76,8 +76,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<IApModelChecker<T>>.check(*this);
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
 	/*!

src/formula/Ltl/BoundedEventually.h

@@ -36,7 +36,7 @@ class IBoundedEventuallyModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
+        virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
 };
 
 /*!
@@ -113,8 +113,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 };
 

src/formula/Ltl/BoundedUntil.h

@@ -35,7 +35,7 @@ class IBoundedUntilModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
+        virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
 };
 
 /*!
@@ -118,8 +118,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 };
 

src/formula/Ltl/Eventually.h

@@ -33,7 +33,7 @@ class IEventuallyModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
+        virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
 };
 
 /*!
@@ -107,8 +107,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 };
 

src/formula/Ltl/Globally.h

@@ -34,7 +34,7 @@ class IGloballyModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
+        virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
 };
 
 /*!
@@ -109,8 +109,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
 	}
 };
 

src/formula/Ltl/Next.h

@@ -33,7 +33,7 @@ class INextModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkNext(const Next<T>& obj, bool qualitative) const = 0;
+        virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
 };
 
 /*!
@@ -107,8 +107,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<INextModelChecker>()->checkNext(*this);
 	}
 };
 

src/formula/Ltl/Not.h

@@ -11,7 +11,6 @@
 #include "AbstractLtlFormula.h"
 #include "src/formula/abstract/Not.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
@@ -104,7 +103,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);
 	}
 };

src/formula/Ltl/Or.h

@@ -15,7 +15,7 @@ namespace storm {
 namespace formula {
 namespace ltl {
 
-template <class T> class And;
+template <class T> class Or;
 
 /*!
  *	@brief Interface class for model checkers that support And.
@@ -32,7 +32,7 @@ class IOrModelChecker {
 		 *	@param obj Formula object with subformulas.
 		 *	@return Result of the formula for every node.
 		 */
-		virtual std::vector<T>* checkOr(const And<T>& obj) const = 0;
+		virtual std::vector<T>* checkOr(const Or<T>& obj) const = 0;
 };
 
 template <class T>
@@ -54,7 +54,7 @@ public:
 	 * @param left The left subformula
 	 * @param right The right subformula
 	 */
-	Or(AbstractLtlFormula<T> left, AbstractLtlFormula<T> right)
+	Or(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
 		: storm::formula::abstract::Or<T,AbstractLtlFormula<T>>(left, right) {
 		// Intentionally left empty
 	}

src/formula/Ltl/Until.h

@@ -33,7 +33,7 @@ class IUntilModelChecker {
          *  @param obj Formula object with subformulas.
          *  @return Result of the formula for every node.
          */
-        virtual std::vector<T>* checkUntil(const Until<T>& obj, bool qualitative) const = 0;
+        virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
 };
 
 /*!
@@ -112,8 +112,8 @@ 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, bool qualitative) const {
-		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
+	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
 };