From 0e0b5ff6881ae02b370c7271feebbe80fbfe49e1 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 16 Apr 2013 14:16:15 +0200 Subject: [PATCH] Added methods to check whether child nodes are set (necessary, as sub classes have no direct access to the pointer) --- src/formula/abstract/And.h | 16 ++++++++++++++++ src/formula/abstract/BoundedEventually.h | 8 ++++++++ src/formula/abstract/BoundedNaryUntil.h | 15 +++++++++++++++ src/formula/abstract/BoundedUntil.h | 16 ++++++++++++++++ src/formula/abstract/Eventually.h | 8 ++++++++ src/formula/abstract/Globally.h | 8 ++++++++ src/formula/abstract/Next.h | 8 ++++++++ src/formula/abstract/Not.h | 8 ++++++++ src/formula/abstract/Or.h | 16 ++++++++++++++++ src/formula/abstract/PathBoundOperator.h | 8 ++++++++ src/formula/abstract/PathNoBoundOperator.h | 8 ++++++++ .../abstract/ProbabilisticBoundOperator.h | 2 +- .../abstract/ProbabilisticNoBoundOperator.h | 2 +- src/formula/abstract/StateBoundOperator.h | 8 ++++++++ src/formula/abstract/StateNoBoundOperator.h | 8 ++++++++ src/formula/abstract/Until.h | 16 ++++++++++++++++ 16 files changed, 153 insertions(+), 2 deletions(-) diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h index 74e6c2e24..672453a48 100644 --- a/src/formula/abstract/And.h +++ b/src/formula/abstract/And.h @@ -104,6 +104,22 @@ public: return *right; } + /*! + * + * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise + */ + bool leftIsSet() const { + return left != nullptr; + } + + /*! + * + * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise + */ + bool rightIsSet() const { + return right != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h index 250804b8a..ac88b69e4 100644 --- a/src/formula/abstract/BoundedEventually.h +++ b/src/formula/abstract/BoundedEventually.h @@ -85,6 +85,14 @@ public: this->child = child; } + /*! + * + * @return True if the child is set, i.e. it does not point to nullptr; false otherwise + */ + bool childIsSet() const { + return child != nullptr; + } + /*! * @returns the maximally allowed number of steps for the bounded until operator */ diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h index e8a65cb9a..014ad1674 100644 --- a/src/formula/abstract/BoundedNaryUntil.h +++ b/src/formula/abstract/BoundedNaryUntil.h @@ -90,6 +90,21 @@ public: right = newRight; } + /*! + * + * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise + */ + bool leftIsSet() const { + return left != nullptr; + } + + /*! + * + * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise + */ + bool rightIsSet() const { + return right != nullptr; + } /*! * Sets the right child node. diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h index 83838b0da..132bb28bf 100644 --- a/src/formula/abstract/BoundedUntil.h +++ b/src/formula/abstract/BoundedUntil.h @@ -107,6 +107,22 @@ public: return *right; } + /*! + * + * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise + */ + bool leftIsSet() const { + return left != nullptr; + } + + /*! + * + * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise + */ + bool rightIsSet() const { + return right != nullptr; + } + /*! * @returns the maximally allowed number of steps for the bounded until operator */ diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h index 508401390..429466ce0 100644 --- a/src/formula/abstract/Eventually.h +++ b/src/formula/abstract/Eventually.h @@ -79,6 +79,14 @@ public: this->child = child; } + /*! + * + * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise + */ + bool childIsSet() const { + return child != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h index 1e46ab2b3..3006b9289 100644 --- a/src/formula/abstract/Globally.h +++ b/src/formula/abstract/Globally.h @@ -80,6 +80,14 @@ public: this->child = child; } + /*! + * + * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise + */ + bool childIsSet() const { + return child != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h index 1f94afd4d..bbf212305 100644 --- a/src/formula/abstract/Next.h +++ b/src/formula/abstract/Next.h @@ -79,6 +79,14 @@ public: this->child = child; } + /*! + * + * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise + */ + bool childIsSet() const { + return child != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h index 3d4ca6216..2e8cdec4e 100644 --- a/src/formula/abstract/Not.h +++ b/src/formula/abstract/Not.h @@ -76,6 +76,14 @@ public: this->child = child; } + /*! + * + * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise + */ + bool childIsSet() const { + return child != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h index 689fa4d7a..73039673d 100644 --- a/src/formula/abstract/Or.h +++ b/src/formula/abstract/Or.h @@ -102,6 +102,22 @@ public: return *right; } + /*! + * + * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise + */ + bool leftIsSet() const { + return left != nullptr; + } + + /*! + * + * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise + */ + bool rightIsSet() const { + return right != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h index f1a2c196b..3b240d774 100644 --- a/src/formula/abstract/PathBoundOperator.h +++ b/src/formula/abstract/PathBoundOperator.h @@ -103,6 +103,14 @@ public: this->pathFormula = pathFormula; } + /*! + * + * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise + */ + bool pathFormulaIsSet() const { + return pathFormula != nullptr; + } + /*! * @returns the comparison relation */ diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h index 428ba99ca..8cd89c3bc 100644 --- a/src/formula/abstract/PathNoBoundOperator.h +++ b/src/formula/abstract/PathNoBoundOperator.h @@ -106,6 +106,14 @@ public: this->pathFormula = pathFormula; } + /*! + * + * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise + */ + bool pathFormulaIsSet() const { + return pathFormula != nullptr; + } + /*! * @returns a string representation of the formula */ diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h index 18be5a834..c22e99207 100644 --- a/src/formula/abstract/ProbabilisticBoundOperator.h +++ b/src/formula/abstract/ProbabilisticBoundOperator.h @@ -39,7 +39,7 @@ namespace abstract { * @see AbstractFormula */ template -class ProbabilisticBoundOperator : public PathBoundOperator { +class ProbabilisticBoundOperator : public PathBoundOperator { public: /*! diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h index 7f565e1b7..4e2553caa 100644 --- a/src/formula/abstract/ProbabilisticNoBoundOperator.h +++ b/src/formula/abstract/ProbabilisticNoBoundOperator.h @@ -2,7 +2,7 @@ * ProbabilisticNoBoundOperator.h * * Created on: 12.12.2012 - * Author: thomas + * Author: Thomas Heinemann */ #ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_ diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h index 117ab3c8f..08cd5822a 100644 --- a/src/formula/abstract/StateBoundOperator.h +++ b/src/formula/abstract/StateBoundOperator.h @@ -85,6 +85,14 @@ public: this->stateFormula = stateFormula; } + /*! + * + * @return True if the state formula is set, i.e. it does not point to nullptr; false otherwise + */ + bool stateFormulaIsSet() const { + return stateFormula != nullptr; + } + /*! * @returns the comparison relation */ diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h index 58f2343d4..794bb448f 100644 --- a/src/formula/abstract/StateNoBoundOperator.h +++ b/src/formula/abstract/StateNoBoundOperator.h @@ -82,6 +82,14 @@ public: this->stateFormula = stateFormula; } + /*! + * + * @return True if the state formula is set, i.e. it does not point to nullptr; false otherwise + */ + bool stateFormulaIsSet() const { + return stateFormula != nullptr; + } + /*! * Calls the model checker to check this formula. * Needed to infer the correct type of formula class. diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h index a172c64ee..cadf0b408 100644 --- a/src/formula/abstract/Until.h +++ b/src/formula/abstract/Until.h @@ -102,6 +102,22 @@ public: return *right; } + /*! + * + * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise + */ + bool leftIsSet() const { + return left != nullptr; + } + + /*! + * + * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise + */ + bool rightIsSet() const { + return right != nullptr; + } + /*! * @returns a string representation of the formula */