From 9e5b69b211603b962e2c91402052569f93a6d108 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 17 Dec 2012 03:20:01 +0100 Subject: [PATCH] Further naming scheme enforcement. --- src/formula/And.h | 24 ++++++++-------- src/formula/{AP.h => Ap.h} | 28 +++++++++---------- src/formula/BoundedUntil.h | 26 ++++++++--------- src/formula/Formulas.h | 8 +++--- src/formula/Next.h | 20 ++++++------- src/formula/Not.h | 18 ++++++------ src/formula/Or.h | 24 ++++++++-------- src/formula/{PCTLformula.h => PctlFormula.h} | 8 +++--- .../{PCTLPathFormula.h => PctlPathFormula.h} | 10 +++---- ...{PCTLStateFormula.h => PctlStateFormula.h} | 10 +++---- src/formula/ProbabilisticIntervalOperator.h | 22 +++++++-------- src/formula/ProbabilisticNoBoundsOperator.h | 22 +++++++-------- src/formula/ProbabilisticOperator.h | 24 ++++++++-------- src/formula/Until.h | 26 ++++++++--------- src/modelChecker/DtmcPrctlModelChecker.h | 18 ++++++------ src/parser/PrctlParser.cpp | 2 +- src/parser/PrctlParser.h | 6 ++-- 17 files changed, 148 insertions(+), 148 deletions(-) rename src/formula/{AP.h => Ap.h} (75%) rename src/formula/{PCTLformula.h => PctlFormula.h} (87%) rename src/formula/{PCTLPathFormula.h => PctlPathFormula.h} (90%) rename src/formula/{PCTLStateFormula.h => PctlStateFormula.h} (90%) diff --git a/src/formula/And.h b/src/formula/And.h index 910e23e8f..62cc46964 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_AND_H_ #define MRMC_FORMULA_AND_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" #include namespace mrmc { @@ -27,11 +27,11 @@ namespace formula { * 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 PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class And : public PCTLStateFormula { +class And : public PctlStateFormula { public: /*! @@ -50,7 +50,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - And(PCTLStateFormula* left, PCTLStateFormula* right) { + And(PctlStateFormula* left, PctlStateFormula* right) { this->left = left; this->right = right; } @@ -75,7 +75,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -84,21 +84,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -121,7 +121,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { And* result = new And(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -146,8 +146,8 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; }; } //namespace formula diff --git a/src/formula/AP.h b/src/formula/Ap.h similarity index 75% rename from src/formula/AP.h rename to src/formula/Ap.h index 05f200c2c..1f636d7df 100644 --- a/src/formula/AP.h +++ b/src/formula/Ap.h @@ -1,5 +1,5 @@ /* - * AP.h + * Ap.h * * Created on: 19.10.2012 * Author: Thomas Heinemann @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_AP_H_ #define MRMC_FORMULA_AP_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -20,21 +20,21 @@ namespace formula { * * This class represents the leaves in the formula tree. * - * @see PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class AP : public PCTLStateFormula { +class Ap : public PctlStateFormula { public: /*! * Constructor * - * Creates a new atomic proposition leaf, with the label AP + * Creates a new atomic proposition leaf, with the label Ap * * @param ap The string representing the atomic proposition */ - AP(std::string ap) { + Ap(std::string ap) { this->ap = ap; } @@ -42,12 +42,12 @@ public: * Destructor. * At this time, empty... */ - virtual ~AP() { } + virtual ~Ap() { } /*! * @returns the name of the atomic proposition */ - const std::string& getAP() const { + const std::string& getAp() const { return ap; } @@ -56,16 +56,16 @@ public: * */ virtual std::string toString() const { - return getAP(); + return getAp(); } /*! * Clones the called object. * - * @returns a new AP-object that is identical the called object. + * @returns a new Ap-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { - return new AP(ap); + virtual PctlStateFormula* clone() const { + return new Ap(ap); } /*! @@ -78,7 +78,7 @@ public: * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkAP(*this); + return modelChecker.checkAp(*this); } private: diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index edc447375..281c112bc 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -8,8 +8,8 @@ #ifndef MRMC_FORMULA_BOUNDEDUNTIL_H_ #define MRMC_FORMULA_BOUNDEDUNTIL_H_ -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" #include "boost/integer/integer_mask.hpp" #include @@ -30,11 +30,11 @@ namespace formula { * 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 PCTLPathFormula - * @see PCTLFormula + * @see PctlPathFormula + * @see PctlFormula */ template -class BoundedUntil : public PCTLPathFormula { +class BoundedUntil : public PctlPathFormula { public: /*! @@ -53,7 +53,7 @@ public: * @param right The left formula subtree * @param bound The maximal number of steps */ - BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right, + BoundedUntil(PctlStateFormula* left, PctlStateFormula* right, uint_fast64_t bound) { this->left = left; this->right = right;; @@ -80,7 +80,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -89,21 +89,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -144,7 +144,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const { + virtual PctlPathFormula* clone() const { BoundedUntil* result = new BoundedUntil(); result->setBound(bound); if (left != NULL) { @@ -171,8 +171,8 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; uint_fast64_t bound; }; diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index cd2370a24..8db8c1f0d 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -9,14 +9,14 @@ #define MRMC_FORMULA_FORMULAS_H_ #include "And.h" -#include "AP.h" +#include "Ap.h" #include "BoundedUntil.h" #include "Next.h" #include "Not.h" #include "Or.h" -#include "PCTLformula.h" -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" #include "ProbabilisticOperator.h" #include "ProbabilisticNoBoundsOperator.h" #include "ProbabilisticIntervalOperator.h" diff --git a/src/formula/Next.h b/src/formula/Next.h index 3ffa8451d..07924846e 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -8,8 +8,8 @@ #ifndef MRMC_FORMULA_NEXT_H_ #define MRMC_FORMULA_NEXT_H_ -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -27,11 +27,11 @@ namespace formula { * 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 PCTLPathFormula - * @see PCTLFormula + * @see PctlPathFormula + * @see PctlFormula */ template -class Next : public PCTLPathFormula { +class Next : public PctlPathFormula { public: /*! @@ -46,7 +46,7 @@ public: * * @param child The child node */ - Next(PCTLStateFormula* child) { + Next(PctlStateFormula* child) { this->child = child; } @@ -65,7 +65,7 @@ public: /*! * @returns the child node */ - const PCTLStateFormula& getChild() const { + const PctlStateFormula& getChild() const { return *child; } @@ -73,7 +73,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PCTLStateFormula* child) { + void setChild(PctlStateFormula* child) { this->child = child; } @@ -95,7 +95,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const { + virtual PctlPathFormula* clone() const { Next* result = new Next(); if (child != NULL) { result->setChild(child); @@ -117,7 +117,7 @@ public: } private: - PCTLStateFormula* child; + PctlStateFormula* child; }; } //namespace formula diff --git a/src/formula/Not.h b/src/formula/Not.h index b4afb7d72..26ae6320c 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_NOT_H_ #define MRMC_FORMULA_NOT_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -23,11 +23,11 @@ namespace formula { * 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 PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class Not : public PCTLStateFormula { +class Not : public PctlStateFormula { public: /*! @@ -41,7 +41,7 @@ public: * Constructor * @param child The child node */ - Not(PCTLStateFormula* child) { + Not(PctlStateFormula* child) { this->child = child; } @@ -60,7 +60,7 @@ public: /*! * @returns The child node */ - const PCTLStateFormula& getChild() const { + const PctlStateFormula& getChild() const { return *child; } @@ -68,7 +68,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PCTLStateFormula* child) { + void setChild(PctlStateFormula* child) { this->child = child; } @@ -88,7 +88,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { Not* result = new Not(); if (child != NULL) { result->setChild(child); @@ -110,7 +110,7 @@ public: } private: - PCTLStateFormula* child; + PctlStateFormula* child; }; } //namespace formula diff --git a/src/formula/Or.h b/src/formula/Or.h index 110ee5228..bc1302185 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_OR_H_ #define MRMC_FORMULA_OR_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -26,11 +26,11 @@ namespace formula { * 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 PCTLStateFormula - * @see PCTLFormula + * @see PctlStateFormula + * @see PctlFormula */ template -class Or : public PCTLStateFormula { +class Or : public PctlStateFormula { public: /*! @@ -49,7 +49,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - Or(PCTLStateFormula* left, PCTLStateFormula* right) { + Or(PctlStateFormula* left, PctlStateFormula* right) { this->left = left; this->right = right; } @@ -74,7 +74,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -83,21 +83,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -120,7 +120,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { Or* result = new Or(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -145,8 +145,8 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; }; } //namespace formula diff --git a/src/formula/PCTLformula.h b/src/formula/PctlFormula.h similarity index 87% rename from src/formula/PCTLformula.h rename to src/formula/PctlFormula.h index 26c805b3e..a4d910483 100644 --- a/src/formula/PCTLformula.h +++ b/src/formula/PctlFormula.h @@ -1,5 +1,5 @@ /* - * PCTLformula.h + * Pctlformula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann @@ -23,16 +23,16 @@ namespace formula { * @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 - * PCTLPathFormula and PCTLStateFormula offer the method clone(). + * PctlPathFormula and PctlStateFormula offer the method clone(). */ template -class PCTLFormula { +class PctlFormula { public: /*! * virtual destructor */ - virtual ~PCTLFormula() { } + virtual ~PctlFormula() { } /*! * @note This function is not implemented in this class. diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PctlPathFormula.h similarity index 90% rename from src/formula/PCTLPathFormula.h rename to src/formula/PctlPathFormula.h index c8230f621..9b6a38b94 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PctlPathFormula.h @@ -1,5 +1,5 @@ /* - * PCTLPathFormula.h + * PctlPathFormula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_PCTLPATHFORMULA_H_ #define MRMC_FORMULA_PCTLPATHFORMULA_H_ -#include "PCTLformula.h" +#include "PctlFormula.h" #include "modelChecker/DtmcPrctlModelChecker.h" #include @@ -26,13 +26,13 @@ namespace formula { * clone(). */ template -class PCTLPathFormula : public PCTLFormula { +class PctlPathFormula : public PctlFormula { public: /*! * empty destructor */ - virtual ~PCTLPathFormula() { } + virtual ~PctlPathFormula() { } /*! * Clones the called object. @@ -42,7 +42,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const = 0; + virtual PctlPathFormula* clone() const = 0; /*! * Calls the model checker to check this formula. diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PctlStateFormula.h similarity index 90% rename from src/formula/PCTLStateFormula.h rename to src/formula/PctlStateFormula.h index c9ed0b5fe..c4eee14f2 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PctlStateFormula.h @@ -1,5 +1,5 @@ /* - * PCTLStateFormula.h + * PctlStateFormula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_PCTLSTATEFORMULA_H_ #define MRMC_FORMULA_PCTLSTATEFORMULA_H_ -#include "PCTLformula.h" +#include "PctlFormula.h" #include "storage/BitVector.h" #include "modelChecker/DtmcPrctlModelChecker.h" @@ -26,13 +26,13 @@ namespace formula { * clone(). */ template -class PCTLStateFormula : public PCTLFormula { +class PctlStateFormula : public PctlFormula { public: /*! * empty destructor */ - virtual ~PCTLStateFormula() { } + virtual ~PctlStateFormula() { } /*! * Clones the called object. @@ -42,7 +42,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const = 0; + virtual PctlStateFormula* clone() const = 0; /*! * Calls the model checker to check this formula. diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h index 6fe054366..5fd2943af 100644 --- a/src/formula/ProbabilisticIntervalOperator.h +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -8,8 +8,8 @@ #ifndef MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ #define MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ -#include "PCTLStateFormula.h" -#include "PCTLPathFormula.h" +#include "PctlStateFormula.h" +#include "PctlPathFormula.h" #include "utility/ConstTemplates.h" namespace mrmc { @@ -35,14 +35,14 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PCTLStateFormula - * @see PCTLPathFormula + * @see PctlStateFormula + * @see PctlPathFormula * @see ProbabilisticOperator * @see ProbabilisticNoBoundsOperator - * @see PCTLFormula + * @see PctlFormula */ template -class ProbabilisticIntervalOperator : public PCTLStateFormula { +class ProbabilisticIntervalOperator : public PctlStateFormula { public: /*! @@ -61,7 +61,7 @@ public: * @param upperBound The upper bound for the probability * @param pathFormula The child node */ - ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula& pathFormula) { + ProbabilisticIntervalOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) { this->lower = lowerBound; this->upper = upperBound; this->pathFormula = &pathFormula; @@ -82,7 +82,7 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - const PCTLPathFormula& getPathFormula () const { + const PctlPathFormula& getPathFormula () const { return *pathFormula; } @@ -105,7 +105,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PCTLPathFormula* pathFormula) { + void setPathFormula(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -141,7 +141,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { ProbabilisticIntervalOperator* result = new ProbabilisticIntervalOperator(); result->setInterval(lower, upper); if (pathFormula != NULL) { @@ -166,7 +166,7 @@ public: private: T lower; T upper; - PCTLPathFormula* pathFormula; + PctlPathFormula* pathFormula; }; } //namespace formula diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/ProbabilisticNoBoundsOperator.h index 0082fe33f..b89080ca7 100644 --- a/src/formula/ProbabilisticNoBoundsOperator.h +++ b/src/formula/ProbabilisticNoBoundsOperator.h @@ -8,8 +8,8 @@ #ifndef MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ #define MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ -#include "PCTLformula.h" -#include "PCTLPathFormula.h" +#include "PctlFormula.h" +#include "PctlPathFormula.h" namespace mrmc { namespace formula { @@ -26,20 +26,20 @@ namespace formula { * * @note * This class is a hybrid of a state and path formula, and may only appear as the outermost operator. - * Hence, it is seen as neither a state nor a path formula, but is directly derived from PCTLformula. + * Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula. * * 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) * * - * @see PCTLStateFormula - * @see PCTLPathFormula + * @see PctlStateFormula + * @see PctlPathFormula * @see ProbabilisticOperator * @see ProbabilisticIntervalOperator - * @see PCTLFormula + * @see PctlFormula */ template -class ProbabilisticNoBoundsOperator: public mrmc::formula::PCTLFormula { +class ProbabilisticNoBoundsOperator: public mrmc::formula::PctlFormula { public: /*! * Empty constructor @@ -54,7 +54,7 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundsOperator(PCTLPathFormula &pathFormula) { + ProbabilisticNoBoundsOperator(PctlPathFormula &pathFormula) { this->pathFormula = &pathFormula; } @@ -68,7 +68,7 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - const PCTLPathFormula& getPathFormula () const { + const PctlPathFormula& getPathFormula () const { return *pathFormula; } @@ -77,7 +77,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PCTLPathFormula* pathFormula) { + void setPathFormula(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -92,7 +92,7 @@ public: } private: - PCTLPathFormula* pathFormula; + PctlPathFormula* pathFormula; }; } /* namespace formula */ diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 8905e030d..b1131ef4b 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -8,7 +8,7 @@ #ifndef MRMC_FORMULA_PROBABILISTICOPERATOR_H_ #define MRMC_FORMULA_PROBABILISTICOPERATOR_H_ -#include "PCTLStateFormula.h" +#include "PctlStateFormula.h" namespace mrmc { namespace formula { @@ -32,14 +32,14 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PCTLStateFormula - * @see PCTLPathFormula + * @see PctlStateFormula + * @see PctlPathFormula * @see ProbabilisticIntervalOperator * @see ProbabilisticNoBoundsOperator - * @see PCTLFormula + * @see PctlFormula */ template -class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula { +class ProbabilisticOperator : public mrmc::formula::PctlStateFormula { public: /*! * Empty constructor @@ -55,7 +55,7 @@ public: * @param bound The expected value for path formulas * @param pathFormula The child node */ - ProbabilisticOperator(T bound, PCTLPathFormula& pathFormula) { + ProbabilisticOperator(T bound, PctlPathFormula& pathFormula) { this->bound = bound; this->pathFormula = &pathFormula; } @@ -73,7 +73,7 @@ public: /*! * @returns the child node (representation of a PCTL path formula) */ - const PCTLPathFormula& getPathFormula () const { + const PctlPathFormula& getPathFormula () const { return *pathFormula; } @@ -89,7 +89,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PCTLPathFormula* pathFormula) { + void setPathFormula(PctlPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -109,7 +109,7 @@ public: * * @returns a new ProbabilisticOperator-object that is identical to the called object. */ - virtual PCTLStateFormula* clone() const { + virtual PctlStateFormula* clone() const { ProbabilisticOperator* result = new ProbabilisticOperator(); result->setBound(bound); if (pathFormula != NULL) { @@ -134,9 +134,9 @@ public: } /*! - * Returns a string representation of this PCTLStateFormula + * Returns a string representation of this PctlStateFormula * - * @returns a string representation of this PCTLStateFormula + * @returns a string representation of this PctlStateFormula */ virtual std::string toString() const { std::string result = " P="; @@ -148,7 +148,7 @@ public: } private: T bound; - PCTLPathFormula* pathFormula; + PctlPathFormula* pathFormula; }; } /* namespace formula */ diff --git a/src/formula/Until.h b/src/formula/Until.h index fb0b67f47..3f094e3a3 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -8,8 +8,8 @@ #ifndef MRMC_FORMULA_UNTIL_H_ #define MRMC_FORMULA_UNTIL_H_ -#include "PCTLPathFormula.h" -#include "PCTLStateFormula.h" +#include "PctlPathFormula.h" +#include "PctlStateFormula.h" namespace mrmc { @@ -28,11 +28,11 @@ namespace formula { * 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 PCTLPathFormula - * @see PCTLFormula + * @see PctlPathFormula + * @see PctlFormula */ template -class Until : public PCTLPathFormula { +class Until : public PctlPathFormula { public: /*! @@ -49,7 +49,7 @@ public: * @param left The left formula subtree * @param right The left formula subtree */ - Until(PCTLStateFormula* left, PCTLStateFormula* right) { + Until(PctlStateFormula* left, PctlStateFormula* right) { this->left = left; this->right = right; } @@ -74,7 +74,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PCTLStateFormula* newLeft) { + void setLeft(PctlStateFormula* newLeft) { left = newLeft; } @@ -83,21 +83,21 @@ public: * * @param newRight the new right child. */ - void setRight(PCTLStateFormula* newRight) { + void setRight(PctlStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PCTLStateFormula& getLeft() const { + const PctlStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PCTLStateFormula& getRight() const { + const PctlStateFormula& getRight() const { return *right; } @@ -120,7 +120,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PCTLPathFormula* clone() const { + virtual PctlPathFormula* clone() const { Until* result = new Until(); if (left != NULL) { result->setLeft(left->clone()); @@ -145,8 +145,8 @@ public: } private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PctlStateFormula* left; + PctlStateFormula* right; }; } //namespace formula diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 984655aa9..9556fd966 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -23,8 +23,8 @@ class DtmcPrctlModelChecker; } -#include "src/formula/PCTLPathFormula.h" -#include "src/formula/PCTLStateFormula.h" +#include "src/formula/PctlPathFormula.h" +#include "src/formula/PctlStateFormula.h" #include "src/formula/Formulas.h" @@ -96,7 +96,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula& formula) const { + mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PctlStateFormula& formula) const { return formula.check(*this); } @@ -117,16 +117,16 @@ public: /*! * The check method for a formula with an AP node as root in its formula tree * - * @param formula The AP state formula to check + * @param formula The Ap state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkAP(const mrmc::formula::AP& formula) const { - if (formula.getAP().compare("true") == 0) { + mrmc::storage::BitVector* checkAp(const mrmc::formula::Ap& formula) const { + if (formula.getAp().compare("true") == 0) { return new mrmc::storage::BitVector(model->getNumberOfStates(), 1); - } else if (formula.getAP().compare("false") == 0) { + } else if (formula.getAp().compare("false") == 0) { return new mrmc::storage::BitVector(model->getNumberOfStates()); } - return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP())); + return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAp())); } /*! @@ -226,7 +226,7 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - std::vector* checkPathFormula(const mrmc::formula::PCTLPathFormula& formula) const { + std::vector* checkPathFormula(const mrmc::formula::PctlPathFormula& formula) const { return formula.check(*this); } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 695d64a78..f1a23077a 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -58,7 +58,7 @@ namespace /*! * @brief Resulting formula. */ - mrmc::formula::PCTLFormula* result; + mrmc::formula::PctlFormula* result; struct dump { diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 0cd5ee7cf..24dc746bb 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -1,7 +1,7 @@ #ifndef MRMC_PARSER_PRCTLPARSER_H_ #define MRMC_PARSER_PRCTLPARSER_H_ -#include "src/formula/PCTLformula.h" +#include "src/formula/PctlFormula.h" #include "src/parser/Parser.h" namespace mrmc { @@ -18,13 +18,13 @@ class PrctlParser : Parser /*! * @brief return formula object parsed from file. */ - mrmc::formula::PCTLFormula* getFormula() + mrmc::formula::PctlFormula* getFormula() { return this->formula; } private: - mrmc::formula::PCTLFormula* formula; + mrmc::formula::PctlFormula* formula; }; } // namespace parser