From 350f1a0990bceca198af51a30ddae5ba4b5bb088 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Mon, 3 Dec 2012 11:40:54 +0100
Subject: [PATCH] Code style for formula classes
---
src/formula/AP.h | 138 +++++++-------
src/formula/And.h | 229 +++++++++++------------
src/formula/BoundedUntil.h | 275 ++++++++++++++--------------
src/formula/Next.h | 170 ++++++++---------
src/formula/Not.h | 164 +++++++++--------
src/formula/Or.h | 230 +++++++++++------------
src/formula/PCTLPathFormula.h | 53 +++---
src/formula/PCTLStateFormula.h | 53 +++---
src/formula/PCTLformula.h | 23 +--
src/formula/ProbabilisticOperator.h | 247 +++++++++++++------------
src/formula/Until.h | 225 ++++++++++++-----------
11 files changed, 914 insertions(+), 893 deletions(-)
diff --git a/src/formula/AP.h b/src/formula/AP.h
index 00a3e8734..8bda0df06 100644
--- a/src/formula/AP.h
+++ b/src/formula/AP.h
@@ -25,74 +25,76 @@ namespace formula {
*/
template <class T>
class AP : public PCTLStateFormula<T> {
- private:
- std::string ap;
- public:
- /*!
- * Constructor
- *
- * Creates a new atomic proposition leaf, with the label AP
- *
- * @param ap The string representing the atomic proposition
- */
- AP(std::string ap) {
- this->ap = ap;
- }
-
- /*!
- * Constructor
- *
- * Creates a new atomic proposition leaf, with the label AP
- *
- * @param ap The string representing the atomic proposition
- */
- AP(char* ap) {
- //TODO: Does that really work?
- this->ap = ap;
- }
-
- /*!
- * Destructor.
- * At this time, empty...
- */
- virtual ~AP() { }
-
- /*!
- * @returns the name of the atomic proposition
- */
- std::string getAP() {
- return ap;
- }
-
- /*!
- * @returns a string representation of the leaf.
- *
- */
- virtual std::string toString() {
- return getAP();
- }
-
- /*!
- * Clones the called object.
- *
- * @returns a new AP-object that is identical the called object.
- */
- virtual PCTLStateFormula<T>* clone() {
- return new AP(ap);
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
- */
- virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkAP(this);
- }
+
+public:
+ /*!
+ * Constructor
+ *
+ * Creates a new atomic proposition leaf, with the label AP
+ *
+ * @param ap The string representing the atomic proposition
+ */
+ AP(std::string ap) {
+ this->ap = ap;
+ }
+
+ /*!
+ * Constructor
+ *
+ * Creates a new atomic proposition leaf, with the label AP
+ *
+ * @param ap The string representing the atomic proposition
+ */
+ AP(char* ap) {
+ //TODO: Does that really work?
+ this->ap = ap;
+ }
+
+ /*!
+ * Destructor.
+ * At this time, empty...
+ */
+ virtual ~AP() { }
+
+ /*!
+ * @returns the name of the atomic proposition
+ */
+ std::string getAP() {
+ return ap;
+ }
+
+ /*!
+ * @returns a string representation of the leaf.
+ *
+ */
+ virtual std::string toString() {
+ return getAP();
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * @returns a new AP-object that is identical the called object.
+ */
+ virtual PCTLStateFormula<T>* clone() {
+ return new AP(ap);
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+ */
+ virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkAP(this);
+ }
+
+private:
+ std::string ap;
};
} //namespace formula
diff --git a/src/formula/And.h b/src/formula/And.h
index 8a1cd9696..16f0b6d8e 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -32,121 +32,122 @@ namespace formula {
*/
template <class T>
class And : public PCTLStateFormula<T> {
- private:
- PCTLStateFormula<T>* left;
- PCTLStateFormula<T>* right;
- public:
- /*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
- */
- And() {
- left = NULL;
- right = NULL;
- }
-
- /*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
- *
- * @param left The left sub formula
- * @param right The right sub formula
- */
- And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~And() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(PCTLStateFormula<T>* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(PCTLStateFormula<T>* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- PCTLStateFormula<T>* getLeft() {
- return left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- PCTLStateFormula<T>* getRight() {
- return right;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "(";
- result += left->toString();
- result += " && ";
- result += right->toString();
- result += ")";
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new AND-object that is identical the called object.
- */
- virtual PCTLStateFormula<T>* clone() {
- And<T>* result = new And();
- if (this->left != NULL) {
- result->setLeft(left->clone());
- }
- if (this->right != NULL) {
- result->setRight(right->clone());
- }
- return result;
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
- */
- virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkAnd(this);
- }
+public:
+ /*!
+ * Empty constructor.
+ * Will create an AND-node without subnotes. Will not represent a complete formula!
+ */
+ And() {
+ left = NULL;
+ right = NULL;
+ }
+
+ /*!
+ * Constructor.
+ * Creates an AND note with the parameters as subtrees.
+ *
+ * @param left The left sub formula
+ * @param right The right sub formula
+ */
+ And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+ this->left = left;
+ this->right = right;
+ }
+
+ /*!
+ * Destructor.
+ *
+ * The subtrees are deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ */
+ virtual ~And() {
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(PCTLStateFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(PCTLStateFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ PCTLStateFormula<T>* getLeft() {
+ return left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ PCTLStateFormula<T>* getRight() {
+ return right;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "(";
+ result += left->toString();
+ result += " && ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new AND-object that is identical the called object.
+ */
+ virtual PCTLStateFormula<T>* clone() {
+ And<T>* result = new And();
+ if (this->left != NULL) {
+ result->setLeft(left->clone());
+ }
+ if (this->right != NULL) {
+ result->setRight(right->clone());
+ }
+ return result;
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+ */
+ virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkAnd(this);
+ }
+
+private:
+ PCTLStateFormula<T>* left;
+ PCTLStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 3e48dc132..c0061691c 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -36,142 +36,145 @@ namespace formula {
*/
template <class T>
class BoundedUntil : public PCTLPathFormula<T> {
- PCTLStateFormula<T>* left;
- PCTLStateFormula<T>* right;
- uint_fast64_t bound;
- public:
- /*!
- * Empty constructor
- */
- BoundedUntil() {
- this->left = NULL;
- this->right = NULL;
- bound = 0;
- }
-
- /*!
- * Constructor
- *
- * @param left The left formula subtree
- * @param right The left formula subtree
- * @param bound The maximal number of steps
- */
- BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
- uint_fast64_t bound) {
- this->left = left;
- this->right = right;;
- this->bound = bound;
- }
-
- /*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~BoundedUntil() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(PCTLStateFormula<T>* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(PCTLStateFormula<T>* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- PCTLStateFormula<T>* getLeft() {
- return left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- PCTLStateFormula<T>* getRight() {
- return right;
- }
-
- /*!
- * @returns the maximally allowed number of steps for the bounded until operator
- */
- uint_fast64_t getBound() {
- return bound;
- }
-
- /*!
- * Sets the maximally allowed number of steps for the bounded until operator
- *
- * @param bound the new bound.
- */
- void setBound(uint_fast64_t bound) {
- this->bound = bound;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "(";
- result += left->toString();
- result += " U<=";
- result += boost::lexical_cast<std::string>(bound);
- result += " ";
- result += right->toString();
- result += ")";
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new BoundedUntil-object that is identical the called object.
- */
- virtual PCTLPathFormula<T>* clone() {
- BoundedUntil<T>* result = new BoundedUntil();
- result->setBound(bound);
- if (left != NULL) {
- result->setLeft(left->clone());
- }
- if (right != NULL) {
- result->setRight(right->clone());
- }
- return result;
- }
-
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A vector indicating the probability that the formula holds for each state.
- */
- virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkBoundedUntil(this);
- }
+
+public:
+ /*!
+ * Empty constructor
+ */
+ BoundedUntil() {
+ this->left = NULL;
+ this->right = NULL;
+ bound = 0;
+ }
+
+ /*!
+ * Constructor
+ *
+ * @param left The left formula subtree
+ * @param right The left formula subtree
+ * @param bound The maximal number of steps
+ */
+ BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
+ uint_fast64_t bound) {
+ this->left = left;
+ this->right = right;;
+ this->bound = bound;
+ }
+
+ /*!
+ * Destructor.
+ *
+ * Also deletes the subtrees.
+ * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ */
+ virtual ~BoundedUntil() {
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(PCTLStateFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(PCTLStateFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ PCTLStateFormula<T>* getLeft() {
+ return left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ PCTLStateFormula<T>* getRight() {
+ return right;
+ }
+
+ /*!
+ * @returns the maximally allowed number of steps for the bounded until operator
+ */
+ uint_fast64_t getBound() {
+ return bound;
+ }
+
+ /*!
+ * Sets the maximally allowed number of steps for the bounded until operator
+ *
+ * @param bound the new bound.
+ */
+ void setBound(uint_fast64_t bound) {
+ this->bound = bound;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "(";
+ result += left->toString();
+ result += " U<=";
+ result += boost::lexical_cast<std::string>(bound);
+ result += " ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new BoundedUntil-object that is identical the called object.
+ */
+ virtual PCTLPathFormula<T>* clone() {
+ BoundedUntil<T>* result = new BoundedUntil();
+ result->setBound(bound);
+ if (left != NULL) {
+ result->setLeft(left->clone());
+ }
+ if (right != NULL) {
+ result->setRight(right->clone());
+ }
+ return result;
+ }
+
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A vector indicating the probability that the formula holds for each state.
+ */
+ virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkBoundedUntil(this);
+ }
+
+private:
+ PCTLStateFormula<T>* left;
+ PCTLStateFormula<T>* right;
+ uint_fast64_t bound;
};
} //namespace formula
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 6000366ff..4ec120b80 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -32,90 +32,92 @@ namespace formula {
*/
template <class T>
class Next : public PCTLPathFormula<T> {
- private:
- PCTLStateFormula<T>* child;
- public:
- /*!
- * Empty constructor
- */
- Next() {
- this->child = NULL;
- }
-
- /*!
- * Constructor
- *
- * @param child The child node
- */
- Next(PCTLStateFormula<T>* child) {
- this->child = child;
- }
-
- /*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~Next() {
- if (child != NULL) {
- delete child;
- }
- }
-
- /*!
- * @returns the child node
- */
- PCTLStateFormula<T>* getChild() {
- return child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(PCTLStateFormula<T>* child) {
- this->child = child;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "(";
- result += " X ";
- result += child->toString();
- result += ")";
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new BoundedUntil-object that is identical the called object.
- */
- virtual PCTLPathFormula<T>* clone() {
- Next<T>* result = new Next<T>();
- if (child != NULL) {
- result->setChild(child);
- }
- return result;
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A vector indicating the probability that the formula holds for each state.
- */
- virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkNext(this);
- }
+
+public:
+ /*!
+ * Empty constructor
+ */
+ Next() {
+ this->child = NULL;
+ }
+
+ /*!
+ * Constructor
+ *
+ * @param child The child node
+ */
+ Next(PCTLStateFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ * Constructor.
+ *
+ * Also deletes the subtree.
+ * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ */
+ virtual ~Next() {
+ if (child != NULL) {
+ delete child;
+ }
+ }
+
+ /*!
+ * @returns the child node
+ */
+ PCTLStateFormula<T>* getChild() {
+ return child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(PCTLStateFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "(";
+ result += " X ";
+ result += child->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new BoundedUntil-object that is identical the called object.
+ */
+ virtual PCTLPathFormula<T>* clone() {
+ Next<T>* result = new Next<T>();
+ if (child != NULL) {
+ result->setChild(child);
+ }
+ return result;
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A vector indicating the probability that the formula holds for each state.
+ */
+ virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkNext(this);
+ }
+
+private:
+ PCTLStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 59f100f70..dfcb7c100 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -28,87 +28,89 @@ namespace formula {
*/
template <class T>
class Not : public PCTLStateFormula<T> {
- private:
- PCTLStateFormula<T>* child;
- public:
- /*!
- * Empty constructor
- */
- Not() {
- this->child = NULL;
- }
-
- /*!
- * Constructor
- * @param child The child node
- */
- Not(PCTLStateFormula<T>* child) {
- this->child = child;
- }
-
- /*!
- * Destructor
- *
- * Also deletes the subtree
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~Not() {
- if (child != NULL) {
- delete child;
- }
- }
-
- /*!
- * @returns The child node
- */
- PCTLStateFormula<T>* getChild() {
- return child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(PCTLStateFormula<T>* child) {
- this->child = child;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "!";
- result += child->toString();
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new AND-object that is identical the called object.
- */
- virtual PCTLStateFormula<T>* clone() {
- Not<T>* result = new Not<T>();
- if (child != NULL) {
- result->setChild(child);
- }
- return result;
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
- */
- virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkNot(this);
- }
+
+public:
+ /*!
+ * Empty constructor
+ */
+ Not() {
+ this->child = NULL;
+ }
+
+ /*!
+ * Constructor
+ * @param child The child node
+ */
+ Not(PCTLStateFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ * Destructor
+ *
+ * Also deletes the subtree
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ */
+ virtual ~Not() {
+ if (child != NULL) {
+ delete child;
+ }
+ }
+
+ /*!
+ * @returns The child node
+ */
+ PCTLStateFormula<T>* getChild() {
+ return child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(PCTLStateFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "!";
+ result += child->toString();
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new AND-object that is identical the called object.
+ */
+ virtual PCTLStateFormula<T>* clone() {
+ Not<T>* result = new Not<T>();
+ if (child != NULL) {
+ result->setChild(child);
+ }
+ return result;
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+ */
+ virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkNot(this);
+ }
+
+private:
+ PCTLStateFormula<T>* child;
};
} //namespace formula
diff --git a/src/formula/Or.h b/src/formula/Or.h
index a5cdbc659..51a2f88fd 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -31,120 +31,122 @@ namespace formula {
*/
template <class T>
class Or : public PCTLStateFormula<T> {
- private:
- PCTLStateFormula<T>* left;
- PCTLStateFormula<T>* right;
- public:
- /*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
- */
- Or() {
- left = NULL;
- right = NULL;
- }
-
- /*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
- *
- * @param left The left sub formula
- * @param right The right sub formula
- */
- Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~Or() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(PCTLStateFormula<T>* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(PCTLStateFormula<T>* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- PCTLStateFormula<T>* getLeft() {
- return left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- PCTLStateFormula<T>* getRight() {
- return right;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "(";
- result += left->toString();
- result += " || ";
- result += right->toString();
- result += ")";
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new AND-object that is identical the called object.
- */
- virtual PCTLStateFormula<T>* clone() {
- Or<T>* result = new Or();
- if (this->left != NULL) {
- result->setLeft(left->clone());
- }
- if (this->right != NULL) {
- result->setRight(right->clone());
- }
- return result;
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
- */
- virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkOr(this);
- }
+
+public:
+ /*!
+ * Empty constructor.
+ * Will create an AND-node without subnotes. Will not represent a complete formula!
+ */
+ Or() {
+ left = NULL;
+ right = NULL;
+ }
+
+ /*!
+ * Constructor.
+ * Creates an AND note with the parameters as subtrees.
+ *
+ * @param left The left sub formula
+ * @param right The right sub formula
+ */
+ Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+ this->left = left;
+ this->right = right;
+ }
+
+ /*!
+ * Destructor.
+ *
+ * The subtrees are deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ */
+ virtual ~Or() {
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(PCTLStateFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(PCTLStateFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ PCTLStateFormula<T>* getLeft() {
+ return left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ PCTLStateFormula<T>* getRight() {
+ return right;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "(";
+ result += left->toString();
+ result += " || ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new AND-object that is identical the called object.
+ */
+ virtual PCTLStateFormula<T>* clone() {
+ Or<T>* result = new Or();
+ if (this->left != NULL) {
+ result->setLeft(left->clone());
+ }
+ if (this->right != NULL) {
+ result->setRight(right->clone());
+ }
+ return result;
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+ */
+ virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkOr(this);
+ }
+
+private:
+ PCTLStateFormula<T>* left;
+ PCTLStateFormula<T>* right;
};
} //namespace formula
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h
index 70255f8b3..b795244e3 100644
--- a/src/formula/PCTLPathFormula.h
+++ b/src/formula/PCTLPathFormula.h
@@ -27,34 +27,35 @@ namespace formula {
*/
template <class T>
class PCTLPathFormula : public PCTLFormula<T> {
- public:
- /*!
- * empty destructor
- */
- virtual ~PCTLPathFormula() { }
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
- */
- virtual PCTLPathFormula<T>* clone() = 0;
+public:
+ /*!
+ * empty destructor
+ */
+ virtual ~PCTLPathFormula() { }
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @note This function is not implemented in this class.
- *
- * @returns A vector indicating the probability that the formula holds for each state.
- */
- virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @note This function is not implemented in this class.
+ * @returns a new AND-object that is identical the called object.
+ */
+ virtual PCTLPathFormula<T>* clone() = 0;
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @note This function is not implemented in this class.
+ *
+ * @returns A vector indicating the probability that the formula holds for each state.
+ */
+ virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
};
} //namespace formula
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h
index de8d0e117..daf369510 100644
--- a/src/formula/PCTLStateFormula.h
+++ b/src/formula/PCTLStateFormula.h
@@ -27,34 +27,35 @@ namespace formula {
*/
template <class T>
class PCTLStateFormula : public PCTLFormula<T> {
- public:
- /*!
- * empty destructor
- */
- virtual ~PCTLStateFormula() { }
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @note This function is not implemented in this class.
- * @returns a new AND-object that is identical the called object.
- */
- virtual PCTLStateFormula<T>* clone() = 0;
+public:
+ /*!
+ * empty destructor
+ */
+ virtual ~PCTLStateFormula() { }
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @note This function is not implemented in this class.
- *
- * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
- */
- virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @note This function is not implemented in this class.
+ * @returns a new AND-object that is identical the called object.
+ */
+ virtual PCTLStateFormula<T>* clone() = 0;
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @note This function is not implemented in this class.
+ *
+ * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+ */
+ virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
};
} //namespace formula
diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h
index 12f51a4ce..b1e7bf0b9 100644
--- a/src/formula/PCTLformula.h
+++ b/src/formula/PCTLformula.h
@@ -27,17 +27,18 @@ namespace formula {
*/
template <class T>
class PCTLFormula {
- public:
- /*!
- * virtual destructor
- */
- virtual ~PCTLFormula() { }
-
- /*!
- * @note This function is not implemented in this class.
- * @returns a string representation of the formula
- */
- virtual std::string toString() = 0;
+
+public:
+ /*!
+ * virtual destructor
+ */
+ virtual ~PCTLFormula() { }
+
+ /*!
+ * @note This function is not implemented in this class.
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() = 0;
};
} //namespace formula
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index 89978f30f..b0585fd58 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -34,128 +34,131 @@ namespace formula {
*/
template<class T>
class ProbabilisticOperator : public PCTLStateFormula<T> {
- T lower;
- T upper;
- PCTLPathFormula<T>* pathFormula;
- public:
- /*!
- * Empty constructor
- */
- ProbabilisticOperator() {
- upper = mrmc::misc::constGetZero(&upper);
- lower = mrmc::misc::constGetZero(&lower);
- pathFormula = NULL;
- }
-
- /*!
- * Constructor
- *
- * @param lowerBound The lower bound for the probability
- * @param upperBound The upper bound for the probability
- * @param pathFormula The child node (can be omitted, is then set to NULL)
- */
- ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
- this->lower = lowerBound;
- this->upper = upperBound;
- this->pathFormula = pathFormula;
- }
-
- /*!
- * Destructor
- *
- * The subtree is deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~ProbabilisticOperator() {
- if (pathFormula != NULL) {
- delete pathFormula;
- }
- }
-
- /*!
- * @returns the child node (representation of a PCTL path formula)
- */
- PCTLPathFormula<T>* getPathFormula () {
- return pathFormula;
- }
-
- /*!
- * @returns the lower bound for the probability
- */
- T getLowerBound() {
- return lower;
- }
-
- /*!
- * @returns the upper bound for the probability
- */
- T getUpperBound() {
- return upper;
- }
-
- /*!
- * Sets the child node
- *
- * @param pathFormula the path formula that becomes the new child node
- */
- void setPathFormula(PCTLPathFormula<T>* pathFormula) {
- this->pathFormula = pathFormula;
- }
-
- /*!
- * Sets the interval in which the probability that the path formula holds may lie.
- *
- * @param lowerBound The lower bound for the probability
- * @param upperBound The upper bound for the probability
- */
- void setInterval(T lowerBound, T upperBound) {
- this->lower = lowerBound;
- this->upper = upperBound;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "(";
- result += " P[";
- result += lower;
- result += ";";
- result += upper;
- result += "] ";
- result += pathFormula->toString();
- result += ")";
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new AND-object that is identical the called object.
- */
- virtual PCTLStateFormula<T>* clone() {
- ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
- result->setInterval(lower, upper);
- if (pathFormula != NULL) {
- result->setPathFormula(pathFormula->clone());
- }
- return result;
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
- */
- virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkProbabilisticOperator(this);
- }
+
+public:
+ /*!
+ * Empty constructor
+ */
+ ProbabilisticOperator() {
+ upper = mrmc::misc::constGetZero(&upper);
+ lower = mrmc::misc::constGetZero(&lower);
+ pathFormula = NULL;
+ }
+
+ /*!
+ * Constructor
+ *
+ * @param lowerBound The lower bound for the probability
+ * @param upperBound The upper bound for the probability
+ * @param pathFormula The child node (can be omitted, is then set to NULL)
+ */
+ ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
+ this->lower = lowerBound;
+ this->upper = upperBound;
+ this->pathFormula = pathFormula;
+ }
+
+ /*!
+ * Destructor
+ *
+ * The subtree is deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ */
+ virtual ~ProbabilisticOperator() {
+ if (pathFormula != NULL) {
+ delete pathFormula;
+ }
+ }
+
+ /*!
+ * @returns the child node (representation of a PCTL path formula)
+ */
+ PCTLPathFormula<T>* getPathFormula () {
+ return pathFormula;
+ }
+
+ /*!
+ * @returns the lower bound for the probability
+ */
+ T getLowerBound() {
+ return lower;
+ }
+
+ /*!
+ * @returns the upper bound for the probability
+ */
+ T getUpperBound() {
+ return upper;
+ }
+
+ /*!
+ * Sets the child node
+ *
+ * @param pathFormula the path formula that becomes the new child node
+ */
+ void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+ this->pathFormula = pathFormula;
+ }
+
+ /*!
+ * Sets the interval in which the probability that the path formula holds may lie.
+ *
+ * @param lowerBound The lower bound for the probability
+ * @param upperBound The upper bound for the probability
+ */
+ void setInterval(T lowerBound, T upperBound) {
+ this->lower = lowerBound;
+ this->upper = upperBound;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "(";
+ result += " P[";
+ result += lower;
+ result += ";";
+ result += upper;
+ result += "] ";
+ result += pathFormula->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new AND-object that is identical the called object.
+ */
+ virtual PCTLStateFormula<T>* clone() {
+ ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
+ result->setInterval(lower, upper);
+ if (pathFormula != NULL) {
+ result->setPathFormula(pathFormula->clone());
+ }
+ return result;
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+ */
+ virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkProbabilisticOperator(this);
+ }
+
+private:
+ T lower;
+ T upper;
+ PCTLPathFormula<T>* pathFormula;
};
} //namespace formula
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 39f361e11..df80ee0e0 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -33,117 +33,120 @@ namespace formula {
*/
template <class T>
class Until : public PCTLPathFormula<T> {
- PCTLStateFormula<T>* left;
- PCTLStateFormula<T>* right;
- public:
- /*!
- * Empty constructor
- */
- Until() {
- this->left = NULL;
- this->right = NULL;
- }
-
- /*!
- * Constructor
- *
- * @param left The left formula subtree
- * @param right The left formula subtree
- */
- Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~Until() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(PCTLStateFormula<T>* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(PCTLStateFormula<T>* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- PCTLStateFormula<T>* getLeft() {
- return left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- PCTLStateFormula<T>* getRight() {
- return right;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() {
- std::string result = "(";
- result += left->toString();
- result += " U ";
- result += right->toString();
- result += ")";
- return result;
- }
-
- /*!
- * Clones the called object.
- *
- * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
- *
- * @returns a new BoundedUntil-object that is identical the called object.
- */
- virtual PCTLPathFormula<T>* clone() {
- Until<T>* result = new Until();
- if (left != NULL) {
- result->setLeft(left->clone());
- }
- if (right != NULL) {
- result->setRight(right->clone());
- }
- return result;
- }
-
- /*!
- * Calls the model checker to check this formula.
- * Needed to infer the correct type of formula class.
- *
- * @note This function should only be called in a generic check function of a model checker class. For other uses,
- * the methods of the model checker should be used.
- *
- * @returns A vector indicating the probability that the formula holds for each state.
- */
- virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
- return modelChecker->checkUntil(this);
- }
+
+public:
+ /*!
+ * Empty constructor
+ */
+ Until() {
+ this->left = NULL;
+ this->right = NULL;
+ }
+
+ /*!
+ * Constructor
+ *
+ * @param left The left formula subtree
+ * @param right The left formula subtree
+ */
+ Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+ this->left = left;
+ this->right = right;
+ }
+
+ /*!
+ * Destructor.
+ *
+ * Also deletes the subtrees.
+ * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+ */
+ virtual ~Until() {
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(PCTLStateFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(PCTLStateFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ PCTLStateFormula<T>* getLeft() {
+ return left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ PCTLStateFormula<T>* getRight() {
+ return right;
+ }
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() {
+ std::string result = "(";
+ result += left->toString();
+ result += " U ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * Clones the called object.
+ *
+ * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+ *
+ * @returns a new BoundedUntil-object that is identical the called object.
+ */
+ virtual PCTLPathFormula<T>* clone() {
+ Until<T>* result = new Until();
+ if (left != NULL) {
+ result->setLeft(left->clone());
+ }
+ if (right != NULL) {
+ result->setRight(right->clone());
+ }
+ return result;
+ }
+
+ /*!
+ * Calls the model checker to check this formula.
+ * Needed to infer the correct type of formula class.
+ *
+ * @note This function should only be called in a generic check function of a model checker class. For other uses,
+ * the methods of the model checker should be used.
+ *
+ * @returns A vector indicating the probability that the formula holds for each state.
+ */
+ virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+ return modelChecker->checkUntil(this);
+ }
+
+private:
+ PCTLStateFormula<T>* left;
+ PCTLStateFormula<T>* right;
};
} //namespace formula