second hald of documentation. I guess that's it :-)

src/formula/InstantaneousReward.h

@@ -20,9 +20,21 @@ namespace formula {
 
 template <class T> class InstantaneousReward;
 
+/*!
+ *  @brief Interface class for model checkers that support InstantaneousReward.
+ *
+ *  All model checkers that support the formula class InstantaneousReward must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IInstantaneousRewardModelChecker {
     public:
+		/*!
+         *  @brief Evaluates InstantaneousReward formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkInstantaneousReward(const InstantaneousReward<T>& obj) const = 0;
 };
 
@@ -113,6 +125,14 @@ public:
 		return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this);
 	}
 	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *  
+     *  As InstantaneousReward formulas 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/Next.h

@@ -18,9 +18,21 @@ namespace formula {
 
 template <class T> class Next;
 
+/*!
+ *  @brief Interface class for model checkers that support Next.
+ *   
+ *  All model checkers that support the formula class Next must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class INextModelChecker {
     public:
+		/*!
+         *  @brief Evaluates Next formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkNext(const Next<T>& obj) const = 0;
 };
 
@@ -125,6 +137,12 @@ public:
 		return modelChecker.template as<INextModelChecker>()->checkNext(*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/NoBoundOperator.h

@@ -18,9 +18,21 @@ namespace formula {
 
 template <class T> class NoBoundOperator;
 
+/*!
+ *  @brief Interface class for model checkers that support NoBoundOperator.
+ *   
+ *  All model checkers that support the formula class NoBoundOperator must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class INoBoundOperatorModelChecker {
     public:
+		/*!
+         *  @brief Evaluates NoBoundOperator formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkNoBoundOperator(const NoBoundOperator<T>& obj) const = 0;
 };
 
@@ -118,6 +130,12 @@ public:
 	 */
 	virtual std::string toString() const = 0;
 	
+	/*!
+     *  @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/Not.h

@@ -18,9 +18,21 @@ namespace formula {
 
 template <class T> class Not;
 
+/*!
+ *  @brief Interface class for model checkers that support Not.
+ *   
+ *  All model checkers that support the formula class Not must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class INotModelChecker {
     public:
+		/*!
+         *  @brief Evaluates Not formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
 };
 
@@ -119,6 +131,12 @@ public:
 		return modelChecker.template as<INotModelChecker>()->checkNot(*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/Or.h

@@ -16,9 +16,21 @@ namespace formula {
 
 template <class T> class Or;
 
+/*!
+ *  @brief Interface class for model checkers that support Or.
+ *   
+ *  All model checkers that support the formula class Or must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IOrModelChecker {
 	public:
+		/*!
+         *  @brief Evaluates Or formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
 		virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
 };
 
@@ -152,6 +164,12 @@ public:
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*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/PrctlFormulaChecker.h

@@ -9,9 +9,22 @@
 namespace storm {
 namespace formula {
 
+/*!
+ *	@brief Checks formulas if they are within PRCTL.
+ *
+ *	This class implements AbstractFormulaChecker to check if a given formula
+ *	is part of PRCTL logic.
+ */
 template <class T>
 class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 	public:
+		/*!
+		 *	Implementation of AbstractFormulaChecker::conforms() using code
+		 *	looking exactly like the sample code given there.
+		 *
+		 *	We currently allow And, Ap, Eventually, Not, Or,
+		 *	ProbabilisticNoBoundOperator.
+		 */
 		virtual bool conforms(const AbstractFormula<T>* formula) const {
 			if (
 					dynamic_cast<const And<T>*>(formula) ||
@@ -25,11 +38,9 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 			}
 			return false;
 		}
-	
-	private:
 };
 
-}
-}
+} // namespace formula
+} // namespace storm
 
 #endif

src/formula/ProbabilisticBoundOperator.h

@@ -14,7 +14,6 @@
 #include "utility/ConstTemplates.h"
 
 namespace storm {
-
 namespace formula {
 
 /*!
@@ -92,7 +91,6 @@ public:
 };
 
 } //namespace formula
-
 } //namespace storm
 
 #endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */

src/formula/ProbabilisticNoBoundOperator.h

@@ -13,7 +13,6 @@
 #include "NoBoundOperator.h"
 
 namespace storm {
-
 namespace formula {
 
 /*!
@@ -77,7 +76,6 @@ public:
 };
 
 } /* namespace formula */
-
 } /* namespace storm */
 
 #endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */

src/formula/ReachabilityReward.h

@@ -14,14 +14,25 @@
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
-
 namespace formula {
 
 template <class T> class ReachabilityReward;
 
+/*!
+ *  @brief Interface class for model checkers that support ReachabilityReward.
+ *   
+ *  All model checkers that support the formula class ReachabilityReward must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IReachabilityRewardModelChecker {
     public:
+		/*!
+         *  @brief Evaluates ReachabilityReward formula within a model checker.  
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkReachabilityReward(const ReachabilityReward<T>& obj) const = 0;
 };
 
@@ -121,6 +132,12 @@ public:
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*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);
 	}
@@ -130,7 +147,6 @@ private:
 };
 
 } //namespace formula
-
 } //namespace storm
 
 #endif /* STORM_FORMULA_REACHABILITYREWARD_H_ */

src/formula/RewardBoundOperator.h

@@ -14,7 +14,6 @@
 #include "utility/ConstTemplates.h"
 
 namespace storm {
-
 namespace formula {
 
 /*!
@@ -90,7 +89,6 @@ public:
 };
 
 } //namespace formula
-
 } //namespace storm
 
 #endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */

src/formula/RewardNoBoundOperator.h

@@ -13,7 +13,6 @@
 #include "NoBoundOperator.h"
 
 namespace storm {
-
 namespace formula {
 
 /*!
@@ -77,7 +76,6 @@ public:
 };
 
 } /* namespace formula */
-
 } /* namespace storm */
 
 #endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */

src/formula/Until.h

@@ -13,14 +13,25 @@
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
-
 namespace formula {
 
 template <class T> class Until;
 
+/*!
+ *  @brief Interface class for model checkers that support Until.
+ *
+ *  All model checkers that support the formula class Until must inherit
+ *  this pure virtual class.
+ */
 template <class T>
 class IUntilModelChecker {
     public:
+		/*!
+         *  @brief Evaluates Until formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
         virtual std::vector<T>* checkUntil(const Until<T>& obj) const = 0;
 };
 
@@ -153,6 +164,12 @@ public:
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*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);
     }