From fb506655642980cb316808f830ba7f9e646076c1 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 22 Apr 2013 16:53:52 +0200 Subject: [PATCH] Documentation of formula classes --- src/formula/Csl/And.h | 2 +- src/formula/Csl/Ap.h | 2 +- src/formula/Csl/Eventually.h | 2 +- src/formula/Csl/Globally.h | 2 +- src/formula/Csl/Next.h | 2 +- src/formula/Csl/Not.h | 2 +- src/formula/Csl/Or.h | 2 +- src/formula/Csl/ProbabilisticBoundOperator.h | 2 +- src/formula/Csl/ProbabilisticNoBoundOperator.h | 2 +- src/formula/Csl/Until.h | 2 +- src/formula/Ltl/AbstractLtlFormula.h | 3 +++ src/formula/Ltl/And.h | 5 ++--- src/formula/Ltl/Ap.h | 8 ++++++++ src/formula/Ltl/BoundedEventually.h | 5 ++--- src/formula/Ltl/BoundedUntil.h | 5 ++--- src/formula/Ltl/Eventually.h | 5 ++--- src/formula/Ltl/Globally.h | 5 ++--- src/formula/Ltl/Next.h | 5 ++--- src/formula/Ltl/Not.h | 5 ++--- src/formula/Ltl/Or.h | 14 ++++++++++++++ src/formula/Ltl/Until.h | 5 ++--- src/formula/Prctl/And.h | 2 +- src/formula/Prctl/Ap.h | 2 +- src/formula/Prctl/BoundedEventually.h | 2 +- src/formula/Prctl/BoundedNaryUntil.h | 2 +- src/formula/Prctl/BoundedUntil.h | 2 +- src/formula/Prctl/CumulativeReward.h | 2 +- src/formula/Prctl/Eventually.h | 2 +- src/formula/Prctl/Globally.h | 2 +- src/formula/Prctl/InstantaneousReward.h | 2 +- src/formula/Prctl/Next.h | 2 +- src/formula/Prctl/Not.h | 2 +- src/formula/Prctl/Or.h | 2 +- src/formula/Prctl/ProbabilisticBoundOperator.h | 2 +- src/formula/Prctl/ProbabilisticNoBoundOperator.h | 2 +- src/formula/Prctl/ReachabilityReward.h | 2 +- src/formula/Prctl/RewardBoundOperator.h | 2 +- src/formula/Prctl/RewardNoBoundOperator.h | 2 +- src/formula/Prctl/SteadyStateReward.h | 2 +- src/formula/Prctl/Until.h | 2 +- src/formula/abstract/And.h | 2 +- src/formula/abstract/BoundedEventually.h | 2 +- src/formula/abstract/BoundedNaryUntil.h | 2 +- src/formula/abstract/BoundedUntil.h | 2 +- src/formula/abstract/CumulativeReward.h | 2 +- src/formula/abstract/Eventually.h | 2 +- src/formula/abstract/Globally.h | 2 +- src/formula/abstract/InstantaneousReward.h | 2 +- src/formula/abstract/Next.h | 2 +- src/formula/abstract/Not.h | 2 +- src/formula/abstract/PathBoundOperator.h | 2 +- src/formula/abstract/PathNoBoundOperator.h | 4 ++-- src/formula/abstract/ProbabilisticBoundOperator.h | 2 +- .../abstract/ProbabilisticNoBoundOperator.h | 2 +- src/formula/abstract/RewardBoundOperator.h | 2 +- src/formula/abstract/RewardNoBoundOperator.h | 2 +- src/formula/abstract/StateBoundOperator.h | 2 +- src/formula/abstract/StateNoBoundOperator.h | 2 +- src/formula/abstract/SteadyStateReward.h | 2 +- src/formula/abstract/TimeBoundedOperator.h | 2 +- src/formula/abstract/TimeBoundedUntil.h | 2 +- src/formula/abstract/Until.h | 2 +- 62 files changed, 93 insertions(+), 76 deletions(-) diff --git a/src/formula/Csl/And.h b/src/formula/Csl/And.h index c68d33e65..7964e8eb3 100644 --- a/src/formula/Csl/And.h +++ b/src/formula/Csl/And.h @@ -40,7 +40,7 @@ class IAndModelChecker { /*! * @brief - * Class for a Abstract formula tree with AND node as root. + * Class for an abstract formula tree with AND node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/Csl/Ap.h b/src/formula/Csl/Ap.h index bf2771f63..70a9ad5ad 100644 --- a/src/formula/Csl/Ap.h +++ b/src/formula/Csl/Ap.h @@ -39,7 +39,7 @@ class IApModelChecker { /*! * @brief - * Class for a Abstract formula tree with atomic proposition as root. + * Class for an abstract formula tree with atomic proposition as root. * * This class represents the leaves in the formula tree. * diff --git a/src/formula/Csl/Eventually.h b/src/formula/Csl/Eventually.h index 8e393ceb3..df616d233 100644 --- a/src/formula/Csl/Eventually.h +++ b/src/formula/Csl/Eventually.h @@ -39,7 +39,7 @@ class IEventuallyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Eventually node as root. + * Class for an abstract (path) formula tree with an Eventually node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Csl/Globally.h b/src/formula/Csl/Globally.h index e81ec932d..cc6a088df 100644 --- a/src/formula/Csl/Globally.h +++ b/src/formula/Csl/Globally.h @@ -40,7 +40,7 @@ class IGloballyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Globally node as root. + * Class for an abstract (path) formula tree with a Globally node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Csl/Next.h b/src/formula/Csl/Next.h index 9a7469a57..da10aa407 100644 --- a/src/formula/Csl/Next.h +++ b/src/formula/Csl/Next.h @@ -39,7 +39,7 @@ class INextModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Next node as root. + * Class for an abstract (path) formula tree with a Next node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/Csl/Not.h b/src/formula/Csl/Not.h index ad275a1a8..648b97fcd 100644 --- a/src/formula/Csl/Not.h +++ b/src/formula/Csl/Not.h @@ -39,7 +39,7 @@ class INotModelChecker { /*! * @brief - * Class for a Abstract formula tree with NOT node as root. + * Class for an abstract formula tree with NOT node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Csl/Or.h b/src/formula/Csl/Or.h index 36b846372..3c9fe1ad5 100644 --- a/src/formula/Csl/Or.h +++ b/src/formula/Csl/Or.h @@ -38,7 +38,7 @@ class IOrModelChecker { /*! * @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. * diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h index c7103abe0..0fd4dab5e 100644 --- a/src/formula/Csl/ProbabilisticBoundOperator.h +++ b/src/formula/Csl/ProbabilisticBoundOperator.h @@ -33,7 +33,7 @@ class IProbabilisticBoundOperatorModelChecker { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * * Has one Abstract path formula as sub formula/tree. diff --git a/src/formula/Csl/ProbabilisticNoBoundOperator.h b/src/formula/Csl/ProbabilisticNoBoundOperator.h index 5c6ba7a44..7f0a21357 100644 --- a/src/formula/Csl/ProbabilisticNoBoundOperator.h +++ b/src/formula/Csl/ProbabilisticNoBoundOperator.h @@ -18,7 +18,7 @@ namespace csl { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities + * Class for an abstract formula tree with a P (probablistic) operator without declaration of probabilities * as root. * * Checking a formula with this operator as root returns the probabilities that the path formula holds diff --git a/src/formula/Csl/Until.h b/src/formula/Csl/Until.h index d716e6054..0213bd833 100644 --- a/src/formula/Csl/Until.h +++ b/src/formula/Csl/Until.h @@ -39,7 +39,7 @@ class IUntilModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Until node as root. + * Class for an abstract (path) formula tree with an Until node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h index eff27a0b6..3443c9717 100644 --- a/src/formula/Ltl/AbstractLtlFormula.h +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -16,6 +16,9 @@ namespace storm { namespace formula { namespace ltl { +/*! + * Interface class for all LTL root formulas. + */ template class AbstractLtlFormula : public virtual storm::formula::abstract::AbstractFormula { public: diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h index 7f574ba05..091a1fdb3 100644 --- a/src/formula/Ltl/And.h +++ b/src/formula/Ltl/And.h @@ -40,9 +40,9 @@ class IAndModelChecker { /*! * @brief - * Class for a Abstract formula tree with AND node as root. + * Class for an abstract formula tree with AND node as root. * - * Has two Abstract state formulas as sub formulas/trees. + * Has two Abstract LTL formulas as sub formulas/trees. * * As AND is commutative, the order is \e theoretically not important, but will influence the order in which * the model checker works. @@ -51,7 +51,6 @@ class IAndModelChecker { * (this behavior can be prevented by setting them to NULL before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class And : public storm::formula::abstract::And>, public AbstractLtlFormula { diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h index 508cc2823..226dab478 100644 --- a/src/formula/Ltl/Ap.h +++ b/src/formula/Ltl/Ap.h @@ -35,6 +35,14 @@ class IApModelChecker { virtual std::vector* checkAp(const Ap& obj) const = 0; }; +/*! + * @brief + * Class for an abstract formula tree with atomic proposition as root. + * + * This class represents the leaves in the formula tree. + * + * @see AbstractLtlFormula + */ template class Ap: public storm::formula::abstract::Ap, public storm::formula::ltl::AbstractLtlFormula { diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h index 48dfe3ecb..09c1bf25b 100644 --- a/src/formula/Ltl/BoundedEventually.h +++ b/src/formula/Ltl/BoundedEventually.h @@ -41,9 +41,9 @@ class IBoundedEventuallyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedEventually node as root. + * Class for an abstract (path) formula tree with a BoundedEventually node as root. * - * Has one Abstract state formulas as sub formula/tree. + * Has one Abstract LTL formulas as sub formula/tree. * * @par Semantics * The formula holds iff in at most \e bound steps, formula \e child holds. @@ -52,7 +52,6 @@ class IBoundedEventuallyModelChecker { * (this behavior can be prevented by setting them to NULL before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class BoundedEventually : public storm::formula::abstract::BoundedEventually>, diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h index 1247fb352..d42b92109 100644 --- a/src/formula/Ltl/BoundedUntil.h +++ b/src/formula/Ltl/BoundedUntil.h @@ -40,9 +40,9 @@ class IBoundedUntilModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedUntil node as root. + * Class for an abstract (path) formula tree with a BoundedUntil node as root. * - * Has two Abstract state formulas as sub formulas/trees. + * Has two Abstract LTL 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, @@ -52,7 +52,6 @@ class IBoundedUntilModelChecker { * (this behavior can be prevented by setting them to NULL before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class BoundedUntil : public storm::formula::abstract::BoundedUntil>, diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h index 6a29b6f9f..ea03ce8dc 100644 --- a/src/formula/Ltl/Eventually.h +++ b/src/formula/Ltl/Eventually.h @@ -38,9 +38,9 @@ class IEventuallyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Eventually node as root. + * Class for an abstract (path) formula tree with an Eventually node as root. * - * Has one Abstract state formula as sub formula/tree. + * Has one Abstract LTL formula as sub formula/tree. * * @par Semantics * The formula holds iff eventually \e child holds. @@ -49,7 +49,6 @@ class IEventuallyModelChecker { * (this behavior can be prevented by setting them to nullptr before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class Eventually : public storm::formula::abstract::Eventually>, diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h index 1982be5a1..0f54d7752 100644 --- a/src/formula/Ltl/Globally.h +++ b/src/formula/Ltl/Globally.h @@ -39,9 +39,9 @@ class IGloballyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Globally node as root. + * Class for an abstract (path) formula tree with a Globally node as root. * - * Has one Abstract state formula as sub formula/tree. + * Has one Abstract LTL formula as sub formula/tree. * * @par Semantics * The formula holds iff globally \e child holds. @@ -50,7 +50,6 @@ class IGloballyModelChecker { * (this behavior can be prevented by setting them to nullptr before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class Globally : public storm::formula::abstract::Globally>, diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h index a6df0c93d..94b313fdd 100644 --- a/src/formula/Ltl/Next.h +++ b/src/formula/Ltl/Next.h @@ -38,9 +38,9 @@ class INextModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Next node as root. + * Class for an abstract (path) formula tree with a Next node as root. * - * Has two Abstract state formulas as sub formulas/trees. + * Has two Abstract LTL formulas as sub formulas/trees. * * @par Semantics * The formula holds iff in the next step, \e child holds @@ -49,7 +49,6 @@ class INextModelChecker { * (this behavior can be prevented by setting them to NULL before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class Next : public storm::formula::abstract::Next>, diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h index 42965c907..5a9746ec3 100644 --- a/src/formula/Ltl/Not.h +++ b/src/formula/Ltl/Not.h @@ -38,15 +38,14 @@ class INotModelChecker { /*! * @brief - * Class for a Abstract formula tree with NOT node as root. + * Class for an abstract formula tree with NOT node as root. * - * Has one Abstract state formula as sub formula/tree. + * Has one Abstract LTL 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 AbstractLtlFormula - * @see AbstractFormula */ template class Not : public storm::formula::abstract::Not>, diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h index d8f1b965c..f8c666e73 100644 --- a/src/formula/Ltl/Or.h +++ b/src/formula/Ltl/Or.h @@ -35,6 +35,20 @@ class IOrModelChecker { virtual std::vector* checkOr(const Or& obj) const = 0; }; +/*! + * @brief + * Class for an abstract formula tree with OR node as root. + * + * Has two LTL 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. + * + * 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 AbstractLtlFormula + */ template class Or: public storm::formula::abstract::Or>, public storm::formula::ltl::AbstractLtlFormula { diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h index 502401f25..1689f7d00 100644 --- a/src/formula/Ltl/Until.h +++ b/src/formula/Ltl/Until.h @@ -38,9 +38,9 @@ class IUntilModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Until node as root. + * Class for an abstract (path) formula tree with an Until node as root. * - * Has two Abstract state formulas as sub formulas/trees. + * Has two Abstract LTL formulas as sub formulas/trees. * * @par Semantics * The formula holds iff eventually, formula \e right (the right subtree) holds, and before, @@ -50,7 +50,6 @@ class IUntilModelChecker { * (this behavior can be prevented by setting them to NULL before deletion) * * @see AbstractLtlFormula - * @see AbstractFormula */ template class Until : public storm::formula::abstract::Until>, diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h index c70feb8d6..f75d4d16a 100644 --- a/src/formula/Prctl/And.h +++ b/src/formula/Prctl/And.h @@ -40,7 +40,7 @@ class IAndModelChecker { /*! * @brief - * Class for a Abstract formula tree with AND node as root. + * Class for an abstract formula tree with AND node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/Prctl/Ap.h b/src/formula/Prctl/Ap.h index 9b47f4960..08766839b 100644 --- a/src/formula/Prctl/Ap.h +++ b/src/formula/Prctl/Ap.h @@ -39,7 +39,7 @@ class IApModelChecker { /*! * @brief - * Class for a Abstract formula tree with atomic proposition as root. + * Class for an abstract formula tree with atomic proposition as root. * * This class represents the leaves in the formula tree. * diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h index e47c6cb59..b288400bd 100644 --- a/src/formula/Prctl/BoundedEventually.h +++ b/src/formula/Prctl/BoundedEventually.h @@ -42,7 +42,7 @@ class IBoundedEventuallyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedEventually node as root. + * Class for an abstract (path) formula tree with a BoundedEventually node as root. * * Has one Abstract state formulas as sub formula/tree. * diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h index 4d61a602b..fb1e0e6aa 100644 --- a/src/formula/Prctl/BoundedNaryUntil.h +++ b/src/formula/Prctl/BoundedNaryUntil.h @@ -45,7 +45,7 @@ class IBoundedNaryUntilModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root. + * Class for an abstract (path) formula tree with a BoundedNaryUntil node as root. * * Has at least two Abstract state formulas as sub formulas and an interval * associated with all but the first sub formula. We'll call the first one diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h index 6ca361a1e..9b085031b 100644 --- a/src/formula/Prctl/BoundedUntil.h +++ b/src/formula/Prctl/BoundedUntil.h @@ -41,7 +41,7 @@ class IBoundedUntilModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedUntil node as root. + * Class for an abstract (path) formula tree with a BoundedUntil node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h index 563aa0de7..320c00538 100644 --- a/src/formula/Prctl/CumulativeReward.h +++ b/src/formula/Prctl/CumulativeReward.h @@ -40,7 +40,7 @@ class ICumulativeRewardModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Cumulative Reward node as root. + * Class for an abstract (path) formula tree with a Cumulative Reward node as root. * * 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) diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h index 61514a511..289a2e7e8 100644 --- a/src/formula/Prctl/Eventually.h +++ b/src/formula/Prctl/Eventually.h @@ -39,7 +39,7 @@ class IEventuallyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Eventually node as root. + * Class for an abstract (path) formula tree with an Eventually node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h index 031bd7841..b7d75408b 100644 --- a/src/formula/Prctl/Globally.h +++ b/src/formula/Prctl/Globally.h @@ -40,7 +40,7 @@ class IGloballyModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Globally node as root. + * Class for an abstract (path) formula tree with a Globally node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h index d8d140b40..e44d5f7c3 100644 --- a/src/formula/Prctl/InstantaneousReward.h +++ b/src/formula/Prctl/InstantaneousReward.h @@ -41,7 +41,7 @@ class IInstantaneousRewardModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Instantaneous Reward node as root. + * Class for an abstract (path) formula tree with a Instantaneous Reward node as root. * * 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) diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h index 4e1e096b9..beae4ea6f 100644 --- a/src/formula/Prctl/Next.h +++ b/src/formula/Prctl/Next.h @@ -39,7 +39,7 @@ class INextModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Next node as root. + * Class for an abstract (path) formula tree with a Next node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h index 6672ba0cd..65aa388b1 100644 --- a/src/formula/Prctl/Not.h +++ b/src/formula/Prctl/Not.h @@ -39,7 +39,7 @@ class INotModelChecker { /*! * @brief - * Class for a Abstract formula tree with NOT node as root. + * Class for an abstract formula tree with NOT node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h index 390b206f1..2d218f8b9 100644 --- a/src/formula/Prctl/Or.h +++ b/src/formula/Prctl/Or.h @@ -38,7 +38,7 @@ class IOrModelChecker { /*! * @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. * diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h index 741edc1d0..7b8838c0b 100644 --- a/src/formula/Prctl/ProbabilisticBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticBoundOperator.h @@ -33,7 +33,7 @@ class IProbabilisticBoundOperatorModelChecker { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * * Has one Abstract path formula as sub formula/tree. diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h index 9b5ea7350..7d146389a 100644 --- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h @@ -18,7 +18,7 @@ namespace prctl { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities + * Class for an abstract formula tree with a P (probablistic) operator without declaration of probabilities * as root. * * Checking a formula with this operator as root returns the probabilities that the path formula holds diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h index a8b283aa8..b0a9945c3 100644 --- a/src/formula/Prctl/ReachabilityReward.h +++ b/src/formula/Prctl/ReachabilityReward.h @@ -39,7 +39,7 @@ class IReachabilityRewardModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Reachability Reward node as root. + * Class for an abstract (path) formula tree with an Reachability Reward node as root. * * Has one Abstract state formula as sub formula/tree. * diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h index e3bbbd524..bd3ce8eb4 100644 --- a/src/formula/Prctl/RewardBoundOperator.h +++ b/src/formula/Prctl/RewardBoundOperator.h @@ -33,7 +33,7 @@ class IRewardBoundOperatorModelChecker { /*! * @brief - * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root. + * Class for an abstract formula tree with a R (reward) operator node over a reward interval as root. * * Has a reward path formula as sub formula/tree. * diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h index 1cf4d8f74..e00f357c6 100644 --- a/src/formula/Prctl/RewardNoBoundOperator.h +++ b/src/formula/Prctl/RewardNoBoundOperator.h @@ -18,7 +18,7 @@ namespace prctl { /*! * @brief - * Class for a Abstract formula tree with a R (reward) operator without declaration of reward values + * Class for an abstract formula tree with a R (reward) operator without declaration of reward values * as root. * * Checking a formula with this operator as root returns the reward for the reward path formula for diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h index 2593d41f1..a480936f1 100644 --- a/src/formula/Prctl/SteadyStateReward.h +++ b/src/formula/Prctl/SteadyStateReward.h @@ -40,7 +40,7 @@ class ISteadyStateRewardModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with a Steady State Reward node as root. + * Class for an abstract (path) formula tree with a Steady State Reward node as root. * * @see AbstractPathFormula * @see AbstractPrctlFormula diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h index c514b17f3..d897eeb97 100644 --- a/src/formula/Prctl/Until.h +++ b/src/formula/Prctl/Until.h @@ -39,7 +39,7 @@ class IUntilModelChecker { /*! * @brief - * Class for a Abstract (path) formula tree with an Until node as root. + * Class for an abstract (path) formula tree with an Until node as root. * * Has two Abstract state formulas as sub formulas/trees. * diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h index 96bd400d9..4e5a4a412 100644 --- a/src/formula/abstract/And.h +++ b/src/formula/abstract/And.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Logic-abstract Class for a Abstract formula tree with AND node as root. + * Logic-abstract Class for an abstract formula tree with AND node as root. * * Has two formulas as sub formulas/trees; the type is the template parameter FormulaType * diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h index f22a513d7..7a97bc67b 100644 --- a/src/formula/abstract/BoundedEventually.h +++ b/src/formula/abstract/BoundedEventually.h @@ -22,7 +22,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedEventually node as root. + * Class for an abstract (path) formula tree with a BoundedEventually node as root. * * Has one formula as sub formula/tree. * diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h index a64e8844b..eb91037f2 100644 --- a/src/formula/abstract/BoundedNaryUntil.h +++ b/src/formula/abstract/BoundedNaryUntil.h @@ -22,7 +22,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root. + * Class for an abstract (path) formula tree with a BoundedNaryUntil node as root. * * 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 diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h index a1b16f333..b0e6c193a 100644 --- a/src/formula/abstract/BoundedUntil.h +++ b/src/formula/abstract/BoundedUntil.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a BoundedUntil node as root. + * Class for an abstract (path) formula tree with a BoundedUntil node as root. * * Has two formulas as sub formulas/trees. * diff --git a/src/formula/abstract/CumulativeReward.h b/src/formula/abstract/CumulativeReward.h index 0ed21e1c6..6340748e2 100644 --- a/src/formula/abstract/CumulativeReward.h +++ b/src/formula/abstract/CumulativeReward.h @@ -18,7 +18,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a Cumulative Reward node as root. + * Class for an abstract (path) formula tree with a Cumulative Reward node as root. * * 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) diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h index 8c116d533..2c498cfdd 100644 --- a/src/formula/abstract/Eventually.h +++ b/src/formula/abstract/Eventually.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with an Eventually node as root. + * Class for an abstract (path) formula tree with an Eventually node as root. * * Has one formula as sub formula/tree. * diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h index 07ac104d6..8ae4751bc 100644 --- a/src/formula/abstract/Globally.h +++ b/src/formula/abstract/Globally.h @@ -20,7 +20,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a Globally node as root. + * Class for an abstract formula tree with a Globally node as root. * * Has one formula as sub formula/tree. * diff --git a/src/formula/abstract/InstantaneousReward.h b/src/formula/abstract/InstantaneousReward.h index bdfc87378..9727ce2e1 100644 --- a/src/formula/abstract/InstantaneousReward.h +++ b/src/formula/abstract/InstantaneousReward.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a Instantaneous Reward node as root. + * Class for an abstract (path) formula tree with a Instantaneous Reward node as root. * * 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) diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h index 71676bef0..8a81cbc6f 100644 --- a/src/formula/abstract/Next.h +++ b/src/formula/abstract/Next.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a Next node as root. + * Class for an abstract (path) formula tree with a Next node as root. * * Has two formulas as sub formulas/trees. * diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h index ea73135cd..f40811309 100644 --- a/src/formula/abstract/Not.h +++ b/src/formula/abstract/Not.h @@ -20,7 +20,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with NOT node as root. + * Class for an abstract formula tree with NOT node as root. * * Has one formula as sub formula/tree. * diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h index bdd7bba0a..291e26e7d 100644 --- a/src/formula/abstract/PathBoundOperator.h +++ b/src/formula/abstract/PathBoundOperator.h @@ -26,7 +26,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * * Has one formula as sub formula/tree. diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h index cf8d23336..392f1a19f 100644 --- a/src/formula/abstract/PathNoBoundOperator.h +++ b/src/formula/abstract/PathNoBoundOperator.h @@ -21,7 +21,7 @@ namespace formula { namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities + * Class for an abstract formula tree with a P (probablistic) operator without declaration of probabilities * as root. * * Checking a formula with this operator as root returns the probabilities that the path formula holds @@ -91,7 +91,7 @@ public: } /*! - * @returns the child node (representation of a Abstract path formula) + * @returns the child node (representation of an abstract path formula) */ const FormulaType& getPathFormula () const { return *pathFormula; diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h index f0d15886c..01bc0a114 100644 --- a/src/formula/abstract/ProbabilisticBoundOperator.h +++ b/src/formula/abstract/ProbabilisticBoundOperator.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * * Has one Abstract path formula as sub formula/tree. diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h index 738b36501..530224630 100644 --- a/src/formula/abstract/ProbabilisticNoBoundOperator.h +++ b/src/formula/abstract/ProbabilisticNoBoundOperator.h @@ -18,7 +18,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities + * Class for an abstract formula tree with a P (probablistic) operator without declaration of probabilities * as root. * * Checking a formula with this operator as root returns the probabilities that the path formula holds diff --git a/src/formula/abstract/RewardBoundOperator.h b/src/formula/abstract/RewardBoundOperator.h index 94b40f86b..cba8ae373 100644 --- a/src/formula/abstract/RewardBoundOperator.h +++ b/src/formula/abstract/RewardBoundOperator.h @@ -17,7 +17,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root. + * Class for an abstract formula tree with a R (reward) operator node over a reward interval as root. * * Has a reward path formula as sub formula/tree. * diff --git a/src/formula/abstract/RewardNoBoundOperator.h b/src/formula/abstract/RewardNoBoundOperator.h index ad8d42dfd..fdcc2c3ef 100644 --- a/src/formula/abstract/RewardNoBoundOperator.h +++ b/src/formula/abstract/RewardNoBoundOperator.h @@ -17,7 +17,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a R (reward) operator without declaration of reward values + * Class for an abstract formula tree with a R (reward) operator without declaration of reward values * as root. * * Checking a formula with this operator as root returns the reward for the reward path formula for diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h index 74a51d651..8ccf69fa0 100644 --- a/src/formula/abstract/StateBoundOperator.h +++ b/src/formula/abstract/StateBoundOperator.h @@ -21,7 +21,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * * Has one formula as sub formula/tree. diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h index ca0038880..23b172cf8 100644 --- a/src/formula/abstract/StateNoBoundOperator.h +++ b/src/formula/abstract/StateNoBoundOperator.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with an operator without declaration of bounds. + * Class for an 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 diff --git a/src/formula/abstract/SteadyStateReward.h b/src/formula/abstract/SteadyStateReward.h index d5c5a7fd7..07419c83c 100644 --- a/src/formula/abstract/SteadyStateReward.h +++ b/src/formula/abstract/SteadyStateReward.h @@ -18,7 +18,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with a Steady State Reward node as root. + * Class for an abstract (path) formula tree with a Steady State Reward node as root. * * @see AbstractFormula */ diff --git a/src/formula/abstract/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h index 61cf5bf36..fdb454503 100644 --- a/src/formula/abstract/TimeBoundedOperator.h +++ b/src/formula/abstract/TimeBoundedOperator.h @@ -19,7 +19,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract formula tree with a operator node as root that uses a time interval + * Class for an 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 concrete subclasses of this abstract class. diff --git a/src/formula/abstract/TimeBoundedUntil.h b/src/formula/abstract/TimeBoundedUntil.h index e82339f99..3574401a1 100644 --- a/src/formula/abstract/TimeBoundedUntil.h +++ b/src/formula/abstract/TimeBoundedUntil.h @@ -17,7 +17,7 @@ namespace abstract { /** * @brief - * Class for a Abstract formula tree with an time bounded until operator as root. + * Class for an 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 diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h index 496b98534..3e2031b96 100644 --- a/src/formula/abstract/Until.h +++ b/src/formula/abstract/Until.h @@ -18,7 +18,7 @@ namespace abstract { /*! * @brief - * Class for a Abstract (path) formula tree with an Until node as root. + * Class for an abstract (path) formula tree with an Until node as root. * * Has two formulas as sub formulas/trees. *