Restructuring formula classes, part I

Sorted formulas into respective folders, depending on which logic they
belong to (or if they are abstract).

The Code is NOTadapted to the new structure yet.

src/formula/Ltl/AbstractLtlFormula.h

@@ -0,0 +1,39 @@
+/*
+ * AbstractLtlFormula.h
+ *
+ *  Created on: 15.04.2013
+ *      Author: thomas
+ */
+
+#ifndef ABSTRACTLTLFORMULA_H_
+#define ABSTRACTLTLFORMULA_H_
+
+namespace storm {
+namespace formula {
+
+class AbstractLtlFormula {
+public:
+	/**
+	 * Empty destructor
+	 */
+	virtual ~AbstractLtlFormula() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @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;
+};
+
+} /* namespace formula */
+} /* namespace storm */
+#endif /* ABSTRACTLTLFORMULA_H_ */

src/formula/Prtl/AbstractPathFormula.h

@@ -0,0 +1,70 @@
+/*
+ * AbstractPathFormula.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_
+#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_
+
+namespace storm { namespace formula {
+template <class T> class AbstractPathFormula;
+}}
+
+#include "src/formula/AbstractFormula.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+#include <vector>
+#include <iostream>
+#include <typeinfo>
+
+namespace storm {
+namespace formula {
+
+/*!
+ * @brief
+ * Abstract base class for Abstract path formulas.
+ *
+ * @attention This class is abstract.
+ * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
+ * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
+ * 	   clone().
+ */
+template <class T>
+class AbstractPathFormula : public virtual AbstractFormula<T> {
+
+public:
+	/*!
+	 * empty destructor
+	 */
+	virtual ~AbstractPathFormula() { }
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @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;
+};
+
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */

src/formula/Prtl/AbstractStateFormula.h

@@ -0,0 +1,68 @@
+/*
+ * AbstractStateFormula.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
+#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
+
+namespace storm { namespace formula {
+template <class T> class AbstractStateFormula;
+}}
+
+#include "src/formula/AbstractFormula.h"
+#include "src/storage/BitVector.h"
+#include "src/modelchecker/ForwardDeclarations.h"
+
+namespace storm {
+namespace formula {
+
+/*!
+ * @brief
+ * Abstract base class for Abstract state formulas.
+ *
+ * @attention This class is abstract.
+ * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
+ * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
+ * 	   clone().
+ */
+template <class T>
+class AbstractStateFormula : public AbstractFormula<T> {
+
+public:
+	/*!
+	 * empty destructor
+	 */
+	virtual ~AbstractStateFormula() { }
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @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; // {
+};
+
+} //namespace formula
+} //namespace storm
+
+
+#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */

src/formula/AbstractFormula.h → src/formula/abstract/AbstractFormula.h

@@ -5,21 +5,25 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_
-#define STORM_FORMULA_ABSTRACTFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_
+#define STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_
 
 #include <string>
 
-namespace storm { namespace formula {
+namespace storm {
+namespace formula {
+namespace abstract {
 template <class T> class AbstractFormula;
-}}
+}
+}
+}
 
 #include "src/modelchecker/ForwardDeclarations.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace formula {
-
+namespace abstract {
 
 //abstract
 /*!
@@ -67,7 +71,8 @@ public:
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0;
 };
 
+} // namespace abstract
 } // namespace formula
 } // namespace storm
 
-#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_ */

src/formula/And.h → src/formula/abstract/And.h

@@ -5,10 +5,10 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_AND_H_
-#define STORM_FORMULA_AND_H_
+#ifndef STORM_FORMULA_ABSTRACT_AND_H_
+#define STORM_FORMULA_ABSTRACT_AND_H_
 
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 #include <string>
@@ -52,7 +52,7 @@ class IAndModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class And : public AbstractStateFormula<T> {
+class And : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -71,7 +71,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+	And(AbstractFormula<T>* left, AbstractFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -177,12 +177,12 @@ public:
     }
 
 private:
-	AbstractStateFormula<T>* left;
-	AbstractStateFormula<T>* right;
+	AbstractFormula<T>* left;
+	AbstractFormula<T>* right;
 };
 
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_AND_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_AND_H_ */