Documentation for CSL and PRCTL classes

src/formula/Csl/AbstractCslFormula.h

@@ -14,6 +14,9 @@ namespace storm {
 namespace formula {
 namespace csl {
 
+/*!
+ * Abstract base class for all CSL root formulas.
+ */
 template <class T>
 class AbstractCslFormula : public virtual storm::formula::abstract::AbstractFormula<T>{
 public:

src/formula/Csl/AbstractNoBoundOperator.h

@@ -38,6 +38,9 @@ public:
 
 };
 
+/*!
+ * Interface class for all CSL No Bound operators.
+ */
 template <class T>
 class AbstractNoBoundOperator: public AbstractCslFormula<T>/*,
 										 public virtual storm::formula::abstract::IOptimizingOperator*/ {

src/formula/Csl/AbstractPathFormula.h

@@ -35,6 +35,9 @@ namespace csl {
  * @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().
+ *
+ * @note
+ * 		This class is intentionally not derived from AbstractCslFormula, as a path formula is not a complete CSL formula.
  */
 template <class T>
 class AbstractPathFormula : public virtual storm::formula::abstract::AbstractFormula<T> {

src/formula/Csl/And.h

@@ -51,7 +51,7 @@ class IAndModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractStateFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class And : public storm::formula::abstract::And<T, AbstractStateFormula<T>>, public AbstractStateFormula<T> {

src/formula/Csl/Ap.h

@@ -43,8 +43,8 @@ class IApModelChecker {
  *
  * This class represents the leaves in the formula tree.
  *
- * @see AbstractFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
+ * @see AbstractStateFormula
  */
 template <class T>
 class Ap : public storm::formula::abstract::Ap<T>,

src/formula/Csl/Eventually.h

@@ -50,7 +50,7 @@ class IEventuallyModelChecker {
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class Eventually : public storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>,

src/formula/Csl/Globally.h

@@ -51,7 +51,7 @@ class IGloballyModelChecker {
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class Globally : public storm::formula::abstract::Globally<T, AbstractStateFormula<T>>,

src/formula/Csl/Next.h

@@ -50,7 +50,7 @@ class INextModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class Next : public storm::formula::abstract::Next<T, AbstractStateFormula<T>>,

src/formula/Csl/Not.h

@@ -47,7 +47,7 @@ class INotModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractStateFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class Not : public storm::formula::abstract::Not<T, AbstractStateFormula<T>>,

src/formula/Csl/Or.h

@@ -49,7 +49,7 @@ class IOrModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractStateFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class Or : public storm::formula::abstract::Or<T, AbstractStateFormula<T>>,

src/formula/Csl/ProbabilisticBoundOperator.h

@@ -50,7 +50,7 @@ class IProbabilisticBoundOperatorModelChecker {
  * @see AbstractPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template<class T>
 class ProbabilisticBoundOperator : public storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>,

src/formula/Csl/ProbabilisticNoBoundOperator.h

@@ -44,7 +44,7 @@ namespace csl {
  * @see AbstractPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticIntervalOperator
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class ProbabilisticNoBoundOperator: public storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>,

src/formula/Csl/SteadyStateBoundOperator.h

@@ -51,7 +51,7 @@ class ISteadyStateBoundOperatorModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class SteadyStateBoundOperator : public storm::formula::abstract::SteadyStateBoundOperator<T, AbstractStateFormula<T>>,

src/formula/Csl/Until.h

@@ -51,7 +51,7 @@ class IUntilModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractCslFormula
  */
 template <class T>
 class Until : public storm::formula::abstract::Until<T, AbstractStateFormula<T>>,

src/formula/Prctl/AbstractNoBoundOperator.h

@@ -38,6 +38,9 @@ public:
 
 };
 
+/*!
+ * Interface class for all PRCTL No bound operators
+ */
 template <class T>
 class AbstractNoBoundOperator: public AbstractPrctlFormula<T>,
 										 public virtual storm::formula::abstract::IOptimizingOperator {

src/formula/Prctl/AbstractPathFormula.h

@@ -31,6 +31,8 @@ namespace prctl {
  * @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().
+ *
+ * @note This class is intentionally not derived from AbstractPrctlFormula, as path formulas are not complete PRCTL formulas.
  */
 template <class T>
 class AbstractPathFormula : public virtual storm::formula::abstract::AbstractFormula<T> {

src/formula/Prctl/AbstractPrctlFormula.h

@@ -14,6 +14,9 @@ namespace storm {
 namespace formula {
 namespace prctl {
 
+/*!
+ * Interface class for all PRCTL root formulas.
+ */
 template<class T>
 class AbstractPrctlFormula : public virtual storm::formula::abstract::AbstractFormula<T> {
 public:

src/formula/Prctl/And.h

@@ -51,7 +51,7 @@ class IAndModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractStateFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class And : public storm::formula::abstract::And<T, AbstractStateFormula<T>>, public AbstractStateFormula<T> {

src/formula/Prctl/Ap.h

@@ -43,8 +43,8 @@ class IApModelChecker {
  *
  * This class represents the leaves in the formula tree.
  *
- * @see AbstractFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
+ * @see AbstractStateFormula
  */
 template <class T>
 class Ap : public storm::formula::abstract::Ap<T>,

src/formula/Prctl/BoundedEventually.h

@@ -53,7 +53,7 @@ class IBoundedEventuallyModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class BoundedEventually : public storm::formula::abstract::BoundedEventually<T, AbstractStateFormula<T>>,

src/formula/Prctl/BoundedNaryUntil.h

@@ -60,7 +60,7 @@ class IBoundedNaryUntilModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class BoundedNaryUntil : public storm::formula::abstract::BoundedNaryUntil<T, AbstractStateFormula<T>>,

src/formula/Prctl/BoundedUntil.h

@@ -53,7 +53,7 @@ class IBoundedUntilModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class BoundedUntil : public storm::formula::abstract::BoundedUntil<T, AbstractStateFormula<T>>,

src/formula/Prctl/CumulativeReward.h

@@ -46,7 +46,7 @@ class ICumulativeRewardModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class CumulativeReward : public storm::formula::abstract::CumulativeReward<T>,

src/formula/Prctl/Eventually.h

@@ -50,7 +50,7 @@ class IEventuallyModelChecker {
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class Eventually : public storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>,

src/formula/Prctl/Globally.h

@@ -51,7 +51,7 @@ class IGloballyModelChecker {
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class Globally : public storm::formula::abstract::Globally<T, AbstractStateFormula<T>>,

src/formula/Prctl/InstantaneousReward.h

@@ -47,7 +47,7 @@ class IInstantaneousRewardModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class InstantaneousReward : public storm::formula::abstract::InstantaneousReward<T>,

src/formula/Prctl/Next.h

@@ -50,7 +50,7 @@ class INextModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class Next : public storm::formula::abstract::Next<T, AbstractStateFormula<T>>,

src/formula/Prctl/Not.h

@@ -47,7 +47,7 @@ class INotModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractStateFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class Not : public storm::formula::abstract::Not<T, AbstractStateFormula<T>>,

src/formula/Prctl/Or.h

@@ -49,7 +49,7 @@ class IOrModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractStateFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class Or : public storm::formula::abstract::Or<T, AbstractStateFormula<T>>,

src/formula/Prctl/ProbabilisticBoundOperator.h

@@ -50,7 +50,7 @@ class IProbabilisticBoundOperatorModelChecker {
  * @see AbstractPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template<class T>
 class ProbabilisticBoundOperator : public storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>,

src/formula/Prctl/ProbabilisticNoBoundOperator.h

@@ -44,7 +44,7 @@ namespace prctl {
  * @see AbstractPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticIntervalOperator
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class ProbabilisticNoBoundOperator: public storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>,

src/formula/Prctl/ReachabilityReward.h

@@ -47,7 +47,7 @@ class IReachabilityRewardModelChecker {
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class ReachabilityReward : public storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>,

src/formula/Prctl/RewardBoundOperator.h

@@ -49,7 +49,7 @@ class IRewardBoundOperatorModelChecker {
  * @see AbstractPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template<class T>
 class RewardBoundOperator : public storm::formula::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>,

src/formula/Prctl/RewardNoBoundOperator.h

@@ -44,7 +44,7 @@ namespace prctl {
  * @see AbstractPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticIntervalOperator
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class RewardNoBoundOperator: public storm::formula::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>,

src/formula/Prctl/SteadyStateReward.h

@@ -43,7 +43,7 @@ class ISteadyStateRewardModelChecker {
  * Class for a Abstract (path) formula tree with a Steady State Reward node as root.
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class SteadyStateReward: public storm::formula::abstract::SteadyStateReward<T>,

src/formula/Prctl/Until.h

@@ -51,7 +51,7 @@ class IUntilModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  * @see AbstractPathFormula
- * @see AbstractFormula
+ * @see AbstractPrctlFormula
  */
 template <class T>
 class Until : public storm::formula::abstract::Until<T, AbstractStateFormula<T>>,

src/modelchecker/SparseDtmcPrctlModelChecker.h

@@ -66,10 +66,9 @@ public:
 	 */
 	std::vector<Type>* checkNoBoundOperator(storm::formula::prctl::AbstractNoBoundOperator<Type> const& formula) const {
 		// Check if the operator was an optimality operator and report a warning in that case.
-		//if (formula.isOptimalityOperator()) {
-		//	LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
-		//}
-		// TODO: Reimplement warning
+		if (formula.isOptimalityOperator()) {
+			LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models.");
+		}
 		return formula.check(*this, false);
 	}