diff --git a/src/formula/Csl/AbstractNoBoundOperator.h b/src/formula/Csl/AbstractNoBoundOperator.h
index 860bd51cf..910efa80f 100644
--- a/src/formula/Csl/AbstractNoBoundOperator.h
+++ b/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
}
/*!
diff --git a/src/formula/Prctl/AbstractNoBoundOperator.h b/src/formula/Prctl/AbstractNoBoundOperator.h
index 7cb38319c..031c25581 100644
--- a/src/formula/Prctl/AbstractNoBoundOperator.h
+++ b/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
}
/*!
diff --git a/src/formula/abstract/AbstractFormula.h b/src/formula/abstract/AbstractFormula.h
index c0c472737..99fa7f78c 100644
--- a/src/formula/abstract/AbstractFormula.h
+++ b/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.
diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h
index 56cc33297..96bd400d9 100644
--- a/src/formula/abstract/And.h
+++ b/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> {
diff --git a/src/formula/abstract/Ap.h b/src/formula/abstract/Ap.h
index 3a8e9d16f..dc49131a4 100644
--- a/src/formula/abstract/Ap.h
+++ b/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> {
diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h
index ad9d959e5..f22a513d7 100644
--- a/src/formula/abstract/BoundedEventually.h
+++ b/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>
diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h
index f49066295..a64e8844b 100644
--- a/src/formula/abstract/BoundedNaryUntil.h
+++ b/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>
diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h
index 37118930b..a1b16f333 100644
--- a/src/formula/abstract/BoundedUntil.h
+++ b/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>
diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h
index ff1803fb7..8c116d533 100644
--- a/src/formula/abstract/Eventually.h
+++ b/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>
diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h
index 7eb0ab8fa..07ac104d6 100644
--- a/src/formula/abstract/Globally.h
+++ b/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>
diff --git a/src/formula/abstract/InstantaneousReward.h b/src/formula/abstract/InstantaneousReward.h
index a141db040..bdfc87378 100644
--- a/src/formula/abstract/InstantaneousReward.h
+++ b/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>
diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h
index c874c9408..71676bef0 100644
--- a/src/formula/abstract/Next.h
+++ b/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>
diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h
index be9933a39..ea73135cd 100644
--- a/src/formula/abstract/Not.h
+++ b/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>
diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h
index 878efc0cb..a4406117e 100644
--- a/src/formula/abstract/Or.h
+++ b/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>
diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h
index d023036dc..bdd7bba0a 100644
--- a/src/formula/abstract/PathBoundOperator.h
+++ b/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;
diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h
index 9f3951f85..cf8d23336 100644
--- a/src/formula/abstract/PathNoBoundOperator.h
+++ b/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 {
diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h
index 67b213c0e..f0d15886c 100644
--- a/src/formula/abstract/ProbabilisticBoundOperator.h
+++ b/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
diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h
index c609d035b..738b36501 100644
--- a/src/formula/abstract/ProbabilisticNoBoundOperator.h
+++ b/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> {
diff --git a/src/formula/abstract/RewardBoundOperator.h b/src/formula/abstract/RewardBoundOperator.h
index 51be81916..94b40f86b 100644
--- a/src/formula/abstract/RewardBoundOperator.h
+++ b/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
*/
diff --git a/src/formula/abstract/RewardNoBoundOperator.h b/src/formula/abstract/RewardNoBoundOperator.h
index 4e6462f67..ad8d42dfd 100644
--- a/src/formula/abstract/RewardNoBoundOperator.h
+++ b/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
*/
diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h
index 5db41d0b5..74a51d651 100644
--- a/src/formula/abstract/StateBoundOperator.h
+++ b/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;
diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h
index d21690a45..ca0038880 100644
--- a/src/formula/abstract/StateNoBoundOperator.h
+++ b/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> {
diff --git a/src/formula/abstract/SteadyStateBoundOperator.h b/src/formula/abstract/SteadyStateBoundOperator.h
index 2ce8d683f..13fee4ff2 100644
--- a/src/formula/abstract/SteadyStateBoundOperator.h
+++ b/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>
diff --git a/src/formula/abstract/SteadyStateNoBoundOperator.h b/src/formula/abstract/SteadyStateNoBoundOperator.h
index 500b53a3a..75c5fc4d4 100644
--- a/src/formula/abstract/SteadyStateNoBoundOperator.h
+++ b/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:
diff --git a/src/formula/abstract/SteadyStateReward.h b/src/formula/abstract/SteadyStateReward.h
index d8ac8589c..d5c5a7fd7 100644
--- a/src/formula/abstract/SteadyStateReward.h
+++ b/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>
diff --git a/src/formula/abstract/TimeBoundedEventually.h b/src/formula/abstract/TimeBoundedEventually.h
index 567cb1464..a47d4f76c 100644
--- a/src/formula/abstract/TimeBoundedEventually.h
+++ b/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:
diff --git a/src/formula/abstract/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h
index f0882d6ed..61cf5bf36 100644
--- a/src/formula/abstract/TimeBoundedOperator.h
+++ b/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
diff --git a/src/formula/abstract/TimeBoundedUntil.h b/src/formula/abstract/TimeBoundedUntil.h
index 61841ac57..e82339f99 100644
--- a/src/formula/abstract/TimeBoundedUntil.h
+++ b/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:
diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h
index f4db97651..496b98534 100644
--- a/src/formula/abstract/Until.h
+++ b/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>