first half of documentation.

src/formula/AbstractFormula.h

@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_AbstractFORMULA_H_
-#define STORM_FORMULA_AbstractFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_
+#define STORM_FORMULA_ABSTRACTFORMULA_H_
 
 #include <string>
 
@@ -23,34 +23,51 @@ namespace formula {
 
 //abstract
 /*!
- * @brief
- * Abstract base class for Abstract formulas in general.
+ *	@brief Abstract base class for Abstract formulas in general.
  *
- * @attention This class is abstract.
- * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
+ *	@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, the classes
  * 	   AbstractPathFormula and AbstractStateFormula offer the method clone().
+ *
+ *	This is the base class for every formula class in every logic.
  */
 template <class T>
 class AbstractFormula {
 
 public:
 	/*!
-	 * virtual destructor
+	 * Virtual destructor.
 	 */
 	virtual ~AbstractFormula() { }
 	
 	/*!
-	 * @note This function is not implemented in this class.
-	 * @returns a string representation of the formula
+	 *	@brief Return string representation of this formula.
+	 *
+	 *	@note very subclass must implement this method.
+	 *
+	 *	@returns a string representation of the formula
 	 */
 	virtual std::string toString() const = 0;
 	
+	/*!
+	 *	@brief Checks if all subtrees are valid in some logic.
+	 *
+	 *	@note Every subclass must implement this method.
+	 *
+	 *	This method is given a checker object that knows which formula
+	 *	classes are allowed within the logic the checker represents. Every
+	 *	subclass is supposed to call checker.conforms() for all child
+	 *	formulas and return true if and only if all those calls returned
+	 *	true.
+	 *
+	 *	@param checker Checker object.
+	 *	@return true iff all subtrees are valid.
+	 */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0;
 };
 
-} //namespace formula
-
-} //namespace storm
+} // namespace formula
+} // namespace storm
 
-#endif /* STORM_FORMULA_AbstractFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */

src/formula/AbstractFormulaChecker.h

@@ -6,13 +6,51 @@
 namespace storm {
 namespace formula {
 
+/*!
+ *	@brief	Base class for all formula checkers.
+ *
+ *	A formula checker is used to check if a given formula is valid in some
+ *	logic. Hence, this pure virtual base class should be subclassed for
+ *	every logic we support.
+ *
+ *	Every subclass must implement conforms(). It gets a pointer to an
+ *	AbstractFormula object and should return if the subtree represented by
+ *	this formula is valid in the logic.
+ *
+ *	Usually, this will be implemented like this:
+ *	@code
+ *	if (
+ *			dynamic_cast<const And<T>*>(formula) ||
+ *			dynamic_cast<const Not<T>*>(formula) ||
+ *			dynamic_cast<const Or<T>*>(formula)
+ *		) {
+ *		return formula->conforms(*this);
+ *	} else return false;
+ *	@endcode
+ *
+ *	Every formula class implements a conforms() method itself which calls
+ *	conforms() on the given checker for every child in the formula tree.
+ *
+ *	If the formula structure is not an actual tree, but an directed acyclic
+ *	graph, the shared subtrees will be checked twice. If we have directed
+ *	cycles, we will have infinite recursions.
+ */
 template <class T>
 class AbstractFormulaChecker {
 	public:
+		/*!
+		 *	@brief Checks if the given formula is valid in some logic.
+		 *
+		 *	Every subclass must implement this method and check, if the
+		 *	formula object is valid in the logic of the subclass.
+		 *
+		 *	@param formula A pointer to some formula object.
+		 *	@return true iff the formula is valid.
+		 */
 		virtual bool conforms(const AbstractFormula<T>* formula) const = 0;
 };
 
-}
-}
+} // namespace formula
+} // namespace storm
 
 #endif

src/formula/AbstractPathFormula.h

@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_AbstractPATHFORMULA_H_
-#define STORM_FORMULA_AbstractPATHFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_
+#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_
 
 namespace storm { namespace formula {
 template <class T> class AbstractPathFormula;
@@ -20,7 +20,6 @@ template <class T> class AbstractPathFormula;
 #include <typeinfo>
 
 namespace storm {
-
 namespace formula {
 
 /*!
@@ -66,7 +65,6 @@ public:
 };
 
 } //namespace formula
-
 } //namespace storm
 
-#endif /* STORM_FORMULA_AbstractPATHFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */

src/formula/AbstractStateFormula.h

@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_AbstractSTATEFORMULA_H_
-#define STORM_FORMULA_AbstractSTATEFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
+#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
 
 namespace storm { namespace formula {
 template <class T> class AbstractStateFormula;
@@ -17,7 +17,6 @@ template <class T> class AbstractStateFormula;
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
-
 namespace formula {
 
 /*!
@@ -63,7 +62,6 @@ public:
 };
 
 } //namespace formula
-
 } //namespace storm
 
 

src/formula/And.h

@@ -18,9 +18,21 @@ namespace formula {
 
 template <class T> class And;
 
+/*!
+ *	@brief Interface class for model checkers that support And.
+ *
+ *	All model checkers that support the formula class And must inherit
+ *	this pure virtual class.
+ */
 template <class T>
 class IAndModelChecker {
 	public:
+		/*!
+		 *	@brief Evaluates And formula within a model checker.
+		 *
+		 *	@param obj Formula object with subformulas.
+		 *	@return Result of the formula for every node.
+		 */
 		virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
 };
 
@@ -154,6 +166,12 @@ public:
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 	
+	/*!
+	 *	@brief Checks if all subtrees conform to some logic.
+	 *
+	 *	@param checker Formula checker object.
+	 *	@return true iff all subtrees conform to some logic.
+	 */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
         return checker.conforms(this->left) && checker.conforms(this->right);
     }

src/formula/Ap.h

@@ -13,14 +13,25 @@
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
-
 namespace formula {
 
 template <class T> class Ap;
 
+/*!
+ *  @brief Interface class for model checkers that support Ap.
+ *
+ *  All model checkers that support the formula class Ap must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IApModelChecker {
     public:
+		/*!
+         *  @brief Evaluates Ap formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
 };
 
@@ -91,6 +102,14 @@ public:
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *	
+     *	As atomic propositions have no subformulas, we return true here.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true
+     */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
 		return true;
 	}

src/formula/BoundOperator.h

@@ -18,12 +18,18 @@ namespace storm {
 
 namespace formula {
 
-template <class T> class BoundUntil;
+template <class T> class BoundOperator;
 
+/*!
+ *  @brief Interface class for model checkers that support BoundOperator.
+ *   
+ *  All model checkers that support the formula class BoundOperator must inherit
+ *  this pure virtual class.
+ */
 template <class T>
-class IBoundUntilModelChecker {
+class IBoundOperatorModelChecker {
     public:
-        virtual storm::storage::BitVector* checkBoundUntil(const BoundUntil<T>& obj) const = 0;
+        virtual storm::storage::BitVector* checkBoundOperator(const BoundOperator<T>& obj) const = 0;
 };
 
 /*!
@@ -156,9 +162,15 @@ 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 modelChecker.template as<IBoundUntilModelChecker>()->checkBoundOperator(*this);
+		return modelChecker.template as<IBoundOperatorModelChecker>()->checkBoundOperator(*this);
 	}
 	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
         return checker.conforms(this->pathFormula);
     }

src/formula/BoundedEventually.h

@@ -21,9 +21,21 @@ namespace formula {
 
 template <class T> class BoundedEventually;
 
+/*!
+ *  @brief Interface class for model checkers that support BoundedEventually.
+ *   
+ *  All model checkers that support the formula class BoundedEventually must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IBoundedEventuallyModelChecker {
     public:
+		/*!
+         *  @brief Evaluates BoundedEventually formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj) const = 0;
 };
 
@@ -149,6 +161,12 @@ public:
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
 		return checker.conforms(this->child);
 	}

src/formula/BoundedUntil.h

@@ -16,14 +16,25 @@
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
-
 namespace formula {
 
 template <class T> class BoundedUntil;
 
+/*!
+ *  @brief Interface class for model checkers that support BoundedUntil.
+ *   
+ *  All model checkers that support the formula class BoundedUntil must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IBoundedUntilModelChecker {
     public:
+		/*!
+         *  @brief Evaluates BoundedUntil formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj) const = 0;
 };
 
@@ -180,6 +191,12 @@ public:
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
 		return checker.conforms(this->left) && checker.conforms(this->right);
 	}

src/formula/CumulativeReward.h

@@ -20,9 +20,21 @@ namespace formula {
 
 template <class T> class CumulativeReward;
 
+/*!
+ *  @brief Interface class for model checkers that support CumulativeReward.
+ *
+ *  All model checkers that support the formula class CumulativeReward must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class ICumulativeRewardModelChecker {
     public:
+		/*!
+         *  @brief Evaluates CumulativeReward formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkCumulativeReward(const CumulativeReward<T>& obj) const = 0;
 };
 
@@ -113,6 +125,14 @@ public:
 		return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this);
 	}
 	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *  
+     *  As CumulativeReward objects have no subformulas, we return true here.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true
+     */	
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
 		return true;
 	}

src/formula/Eventually.h

@@ -18,9 +18,21 @@ namespace formula {
 
 template <class T> class Eventually;
 
+/*!
+ *  @brief Interface class for model checkers that support Eventually.
+ *
+ *  All model checkers that support the formula class Eventually must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IEventuallyModelChecker {
     public:
+		/*!
+         *  @brief Evaluates Eventually formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkEventually(const Eventually<T>& obj) const = 0;
 };
 
@@ -123,6 +135,12 @@ public:
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
 		return checker.conforms(this->child);
 	}

src/formula/Globally.h

@@ -18,9 +18,21 @@ namespace formula {
 
 template <class T> class Globally;
 
+/*!
+ *  @brief Interface class for model checkers that support Globally.
+ *   
+ *  All model checkers that support the formula class Globally must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IGloballyModelChecker {
     public:
+		/*!
+         *  @brief Evaluates Globally formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkGlobally(const Globally<T>& obj) const = 0;
 };
 
@@ -123,6 +135,12 @@ public:
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);  
 	}
 	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
 	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
 		return checker.conforms(this->child);
 	}