Documentation of abstract formulas.

src/formula/Csl/AbstractNoBoundOperator.h

@@ -43,11 +43,11 @@ class AbstractNoBoundOperator: public AbstractCslFormula<T>/*,
 										 public virtual storm::formula::abstract::IOptimizingOperator*/ {
 public:
 	AbstractNoBoundOperator() {
-		// TODO Auto-generated constructor stub
+		// Intentionally left empty
 
 	}
 	virtual ~AbstractNoBoundOperator() {
-		// TODO Auto-generated destructor stub
+		// Intentionally left empty
 	}
 
 	/*!

src/formula/Prctl/AbstractNoBoundOperator.h

@@ -43,11 +43,11 @@ class AbstractNoBoundOperator: public AbstractPrctlFormula<T>,
 										 public virtual storm::formula::abstract::IOptimizingOperator {
 public:
 	AbstractNoBoundOperator() {
-		// TODO Auto-generated constructor stub
+		// Intentionally left empty.
 
 	}
 	virtual ~AbstractNoBoundOperator() {
-		// TODO Auto-generated destructor stub
+		// Intentionally left empty
 	}
 
 	/*!

src/formula/abstract/AbstractFormula.h

@@ -27,7 +27,19 @@ namespace abstract {
 
 //abstract
 /*!
- *	@brief Abstract base class for Abstract formulas in general.
+ *	@brief Abstract base class for logic Abstract formulas in general.
+ *
+ * The namespace storm::formula::abstract contains versions of the formula classes which are logic abstract, and contain
+ * the implementation which is not directly dependent on the logics.
+ * The classes for the subtrees are referenced by the template parameter FormulaType, which is typically instantiated in
+ * the derived classes of concrete logics.
+ *
+ * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions "toString" and "conforms"
+ * of the subformulas are needed.
+ *
+ * @note
+ * 		Even though the namespace is called "abstract", its classes may be completely implemented; abstract here denotes
+ * 		the abstraction from a concrete logic.
  *
  *	@attention This class is abstract.
  *	@note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
@@ -43,7 +55,9 @@ public:
 	/*!
 	 * Virtual destructor.
 	 */
-	virtual ~AbstractFormula() { }
+	virtual ~AbstractFormula() {
+		// Intentionally left empty.
+	}
 	
 	/*!
 	 *	@brief Return string representation of this formula.

src/formula/abstract/And.h

@@ -19,9 +19,9 @@ namespace abstract {
 
 /*!
  * @brief
- * Class for a Abstract formula tree with AND node as root.
+ * Logic-abstract Class for a Abstract formula tree with AND node as root.
  *
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two formulas as sub formulas/trees; the type is the template parameter FormulaType
  *
  * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
  * the model checker works.
@@ -30,7 +30,10 @@ namespace abstract {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractFormula
- * @see AbstractFormula
+ *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  */
 template <class T, class FormulaType>
 class And : public virtual AbstractFormula<T> {

src/formula/abstract/Ap.h

@@ -18,12 +18,11 @@ namespace abstract {
 
 /*!
  * @brief
- * Class for a Abstract formula tree with atomic proposition as root.
+ * Logic-abstract Class for an abstract formula tree with atomic proposition as root.
  *
  * This class represents the leaves in the formula tree.
  *
  * @see AbstractFormula
- * @see AbstractFormula
  */
 template <class T>
 class Ap : public virtual AbstractFormula<T> {

src/formula/abstract/BoundedEventually.h

@@ -24,7 +24,7 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with a BoundedEventually node as root.
  *
- * Has one Abstract state formulas as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @par Semantics
  * The formula holds iff in at most \e bound steps, formula \e child holds.
@@ -32,7 +32,10 @@ namespace abstract {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/BoundedNaryUntil.h

@@ -24,7 +24,7 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root.
  *
- * Has at least two Abstract state formulas as sub formulas and an interval
+ * Has at least two formulas as sub formulas and an interval
  * associated with all but the first sub formula. We'll call the first one
  * \e left and all other one \e right.
  *
@@ -36,7 +36,10 @@ namespace abstract {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/BoundedUntil.h

@@ -21,7 +21,7 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with a BoundedUntil node as root.
  *
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two formulas as sub formulas/trees.
  *
  * @par Semantics
  * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
@@ -30,7 +30,10 @@ namespace abstract {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/Eventually.h

@@ -21,7 +21,7 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with an Eventually node as root.
  *
- * Has one Abstract state formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @par Semantics
  * The formula holds iff eventually \e child holds.
@@ -29,7 +29,10 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/Globally.h

@@ -20,9 +20,9 @@ namespace abstract {
 
 /*!
  * @brief
- * Class for a Abstract (path) formula tree with a Globally node as root.
+ * Class for a Abstract formula tree with a Globally node as root.
  *
- * Has one Abstract state formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @par Semantics
  * The formula holds iff globally \e child holds.
@@ -30,7 +30,10 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/InstantaneousReward.h

@@ -24,7 +24,6 @@ namespace abstract {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractPathFormula
  * @see AbstractFormula
  */
 template <class T>

src/formula/abstract/Next.h

@@ -21,7 +21,7 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with a Next node as root.
  *
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two formulas as sub formulas/trees.
  *
  * @par Semantics
  * The formula holds iff in the next step, \e child holds
@@ -29,7 +29,10 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/Not.h

@@ -22,12 +22,15 @@ namespace abstract {
  * @brief
  * Class for a Abstract formula tree with NOT node as root.
  *
- * Has one Abstract state formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/Or.h

@@ -17,9 +17,9 @@ namespace abstract {
 
 /*!
  * @brief
- * Class for a Abstract formula tree with OR node as root.
+ * Class for an abstract formula tree with OR node as root.
  *
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two formulas as sub formulas/trees.
  *
  * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
  * the model checker works.
@@ -27,7 +27,10 @@ namespace abstract {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/PathBoundOperator.h

@@ -29,7 +29,7 @@ namespace abstract {
  * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
  * as root.
  *
- * Has one Abstract path formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @par Semantics
  * 	  The formula holds iff the probability that the path formula holds is inside the bounds
@@ -38,12 +38,12 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
  * @see AbstractFormula
- * @see AbstractFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
+ * @see PathNoBoundOperator
  */
 template<class T, class FormulaType>
 class PathBoundOperator : public virtual AbstractFormula<T>, public OptimizingOperator {
@@ -87,7 +87,7 @@ public:
 	}
 
 	/*!
-	 * @returns the child node (representation of a Abstract path formula)
+	 * @returns the child node (representation of a formula)
 	 */
 	const FormulaType& getPathFormula () const {
 		return *pathFormula;

src/formula/abstract/PathNoBoundOperator.h

@@ -27,7 +27,7 @@ namespace abstract {
  * Checking a formula with this operator as root returns the probabilities that the path formula holds
  * (for each state)
  *
- * Has one Abstract path formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @note
  * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
@@ -42,12 +42,12 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
  * @see AbstractFormula
- * @see AbstractFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticIntervalOperator
- * @see AbstractFormula
+ * @see PathBoundOperator
  */
 template <class T, class FormulaType>
 class PathNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {

src/formula/abstract/ProbabilisticBoundOperator.h

@@ -31,6 +31,9 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
  * @see AbstractFormula
  * @see AbstractFormula

src/formula/abstract/ProbabilisticNoBoundOperator.h

@@ -39,12 +39,13 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
  * @see AbstractFormula
- * @see AbstractFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticIntervalOperator
- * @see AbstractFormula
+ * @see PathNoBoundOperator
+ * @see ProbabilisticBoundOperator
  */
 template <class T, class FormulaType>
 class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {

src/formula/abstract/RewardBoundOperator.h

@@ -28,12 +28,13 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
+ * @see PathBoundOperator
+ * @see RewardNoBoundOperator
  */
 template<class T, class FormulaType>
 class RewardBoundOperator : public PathBoundOperator<T, FormulaType> {
@@ -61,6 +62,13 @@ public:
 		// Intentionally left empty
 	}
 
+	/*!
+	 * Constructor
+	 * @param comparisonRelation
+	 * @param bound
+	 * @param pathFormula
+	 * @param minimumOperator
+	 */
 	RewardBoundOperator(
 			storm::formula::ComparisonType comparisonRelation,
 			T bound,
@@ -70,6 +78,13 @@ public:
 		// Intentionally left empty
 	}
 
+	/*!
+	 * Destructor
+	 */
+	virtual ~RewardBoundOperator() {
+		// Intentionally left empty
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */

src/formula/abstract/RewardNoBoundOperator.h

@@ -23,7 +23,7 @@ namespace abstract {
  * Checking a formula with this operator as root returns the reward for the reward path formula for
  * each state
  *
- * Has one Abstract path formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @note
  * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
@@ -38,12 +38,13 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticIntervalOperator
  * @see AbstractFormula
+ * @see PathNoBoundOperator
+ * @see RewardBoundOperator
  */
 template <class T, class FormulaType>
 class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
@@ -73,6 +74,13 @@ public:
 		// Intentionally left empty
 	}
 
+	/*!
+	 * Destructor
+	 */
+	virtual ~RewardBoundOperator() {
+		// Intentionally left empty
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */

src/formula/abstract/StateBoundOperator.h

@@ -24,7 +24,7 @@ namespace abstract {
  * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
  * as root.
  *
- * Has one Abstract state formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @par Semantics
  * 	  The formula holds iff the probability that the state formula holds is inside the bounds
@@ -33,12 +33,12 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
  * @see AbstractFormula
- * @see AbstractFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
+ * @see StateNoBoundOperator
  */
 template<class T, class FormulaType>
 class StateBoundOperator : public virtual AbstractFormula<T> {
@@ -70,7 +70,7 @@ public:
 	}
 
 	/*!
-	 * @returns the child node (representation of a Abstract state formula)
+	 * @returns the child node (representation of a formula)
 	 */
 	const FormulaType& getStateFormula () const {
 		return *stateFormula;

src/formula/abstract/StateNoBoundOperator.h

@@ -19,13 +19,13 @@ namespace abstract {
 
 /*!
  * @brief
- * Class for a Abstract formula tree with an operator without declaration of probabilities
+ * Class for a Abstract formula tree with an operator without declaration of bounds.
  * as root.
  *
  * Checking a formula with this operator as root returns the probabilities that the path formula holds
  * (for each state)
  *
- * Has one Abstract state formula as sub formula/tree.
+ * Has one formula as sub formula/tree.
  *
  * @note
  * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
@@ -40,11 +40,12 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with it
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
  *
  * @see AbstractFormula
- * @see AbstractFormula
- * @see SteadyStateNoBoundOperator
- * @see AbstractFormula
+ * @see StateBoundOperator
  */
 template <class T, class FormulaType>
 class StateNoBoundOperator: public virtual AbstractFormula<T> {

src/formula/abstract/SteadyStateBoundOperator.h

@@ -19,7 +19,7 @@ namespace abstract {
  * @brief
  * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root.
  *
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two formulas as sub formulas/trees.
  *
  * @par Semantics
  * The formula holds iff \e child holds  SteadyStateOperator step, \e child holds
@@ -27,7 +27,6 @@ namespace abstract {
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractPathFormula
  * @see AbstractFormula
  */
 template <class T, class FormulaType>

src/formula/abstract/SteadyStateNoBoundOperator.h

@@ -14,6 +14,19 @@ namespace storm {
 namespace formula {
 namespace abstract {
 
+/*!
+ * @brief
+ * Class for an abstract formula tree with a steady state operator as root, without explicit declaration of bounds.
+ *
+ * Checking a formula with this operator as root returns the exact bound parameter for the corresponding subformula.
+ * (for each state)
+ *
+ * Has one formula as sub formula/tree.
+ *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ */
 template <class T, class FormulaType>
 class SteadyStateNoBoundOperator: public StateNoBoundOperator<T, FormulaType> {
 public:

src/formula/abstract/SteadyStateReward.h

@@ -20,7 +20,6 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with a Steady State Reward node as root.
  *
- * @see AbstractPathFormula
  * @see AbstractFormula
  */
 template <class T>

src/formula/abstract/TimeBoundedEventually.h

@@ -14,7 +14,15 @@ namespace storm {
 namespace formula {
 namespace abstract {
 
-
+/*!
+ * Class for a formula tree with a time bounded eventually operator as root.
+ *
+ * Has two subformulas.
+ *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ */
 template<class T, class FormulaType>
 class TimeBoundedEventually: public storm::formula::abstract::TimeBoundedOperator<T> {
 public:

src/formula/abstract/TimeBoundedOperator.h

@@ -22,7 +22,7 @@ namespace abstract {
  * Class for a Abstract formula tree with a operator node as root that uses a time interval
  * (with upper and lower bound)
  *
- * This class does not provide support for sub formulas; this has to be done in concretizations of this abstract class.
+ * This class does not provide support for sub formulas; this has to be done in concrete subclasses of this abstract class.
  *
  *
  * @see AbstractFormula

src/formula/abstract/TimeBoundedUntil.h

@@ -14,6 +14,15 @@ namespace storm {
 namespace formula {
 namespace abstract {
 
+
+/**
+ * @brief
+ * Class for a Abstract formula tree with an time bounded until operator as root.
+ *
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ */
 template <class T, class FormulaType>
 class TimeBoundedUntil: public TimeBoundedOperator<T> {
 public:

src/formula/abstract/Until.h

@@ -20,7 +20,7 @@ namespace abstract {
  * @brief
  * Class for a Abstract (path) formula tree with an Until node as root.
  *
- * Has two Abstract state formulas as sub formulas/trees.
+ * Has two formulas as sub formulas/trees.
  *
  * @par Semantics
  * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
@@ -29,7 +29,10 @@ namespace abstract {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see AbstractFormula
+ * @tparam FormulaType The type of the subformula.
+ * 		  The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
+ * 		  "toString" and "conforms" of the subformulas are needed.
+ *
  * @see AbstractFormula
  */
 template <class T, class FormulaType>