diff --git a/src/formula/Csl.h b/src/formula/Csl.h index a6a6c4e67..8e856f459 100644 --- a/src/formula/Csl.h +++ b/src/formula/Csl.h @@ -15,9 +15,7 @@ #include "Csl/Next.h" #include "Csl/Not.h" #include "Csl/Or.h" -#include "Csl/ProbabilisticNoBoundOperator.h" #include "Csl/ProbabilisticBoundOperator.h" -#include "Csl/SteadyStateNoBoundOperator.h" #include "Csl/SteadyStateBoundOperator.h" #include "Csl/Until.h" diff --git a/src/formula/Csl/AbstractCslFormula.h b/src/formula/Csl/AbstractCslFormula.h index 1c8503180..7de783d96 100644 --- a/src/formula/Csl/AbstractCslFormula.h +++ b/src/formula/Csl/AbstractCslFormula.h @@ -8,7 +8,7 @@ #ifndef ABSTRACTCSLFORMULA_H_ #define ABSTRACTCSLFORMULA_H_ -#include "src/formula/abstract/AbstractFormula.h" +#include "src/formula/AbstractFormula.h" namespace storm { namespace property { @@ -18,7 +18,7 @@ namespace csl { * Abstract base class for all CSL root formulas. */ template -class AbstractCslFormula : public virtual storm::property::abstract::AbstractFormula{ +class AbstractCslFormula : public virtual storm::property::AbstractFormula{ public: virtual ~AbstractCslFormula() { // Intentionally left empty diff --git a/src/formula/Csl/AbstractNoBoundOperator.h b/src/formula/Csl/AbstractNoBoundOperator.h deleted file mode 100644 index 9960e8de2..000000000 --- a/src/formula/Csl/AbstractNoBoundOperator.h +++ /dev/null @@ -1,83 +0,0 @@ -/* - * AbstractNoBoundOperator.h - * - * Created on: 16.04.2013 - * Author: thomas - */ - -#ifndef STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ -#define STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ - -#include "AbstractCslFormula.h" -#include "src/formula/abstract/IOptimizingOperator.h" - -namespace storm { -namespace property { -namespace csl { - -template -class AbstractNoBoundOperator; - -/*! - * @brief Interface class for model checkers that support PathNoBoundOperator. - * - * All model checkers that support the formula class NoBoundOperator must inherit - * this pure virtual class. - */ -template -class INoBoundOperatorModelChecker { -public: - /*! - * @brief Evaluates NoBoundOperator formula within a model checker. - * - * @param obj Formula object with subformulas. - * @return Result of the formula for every node. - */ - virtual std::vector checkNoBoundOperator(const AbstractNoBoundOperator& obj) const = 0; - - -}; - -/*! - * Interface class for all CSL No Bound operators. - */ -template -class AbstractNoBoundOperator: public AbstractCslFormula, - public virtual storm::property::abstract::IOptimizingOperator { -public: - AbstractNoBoundOperator() { - // Intentionally left empty - - } - virtual ~AbstractNoBoundOperator() { - // Intentionally left empty - } - - /*! - * 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 AbstractNoBoundOperator* clone() const = 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 check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const = 0; -}; - -} /* namespace csl */ -} /* namespace property */ -} /* namespace storm */ -#endif /* STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/AbstractPathFormula.h b/src/formula/Csl/AbstractPathFormula.h index a61cab96f..951bc6f41 100644 --- a/src/formula/Csl/AbstractPathFormula.h +++ b/src/formula/Csl/AbstractPathFormula.h @@ -16,7 +16,7 @@ template class AbstractPathFormula; } //namespace property } //namespace storm -#include "src/formula/abstract/AbstractFormula.h" +#include "src/formula/Csl/AbstractCslFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" #include @@ -40,7 +40,7 @@ namespace csl { * This class is intentionally not derived from AbstractCslFormula, as a path formula is not a complete CSL formula. */ template -class AbstractPathFormula : public virtual storm::property::abstract::AbstractFormula { +class AbstractPathFormula : public virtual storm::property::csl::AbstractCslFormula { public: /*! diff --git a/src/formula/Csl/AbstractStateFormula.h b/src/formula/Csl/AbstractStateFormula.h index c54d318d5..2bd16471b 100644 --- a/src/formula/Csl/AbstractStateFormula.h +++ b/src/formula/Csl/AbstractStateFormula.h @@ -8,15 +8,7 @@ #ifndef STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_ #define STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_ -namespace storm { -namespace property { -namespace csl { -template class AbstractStateFormula; -} -} -} - -#include "AbstractCslFormula.h" +#include "src/formula/Csl/AbstractCslFormula.h" #include "src/storage/BitVector.h" #include "src/modelchecker/csl/ForwardDeclarations.h" @@ -34,7 +26,7 @@ namespace csl { * clone(). */ template -class AbstractStateFormula : public AbstractCslFormula { +class AbstractStateFormula : public storm::property::csl::AbstractCslFormula { public: /*! diff --git a/src/formula/Csl/And.h b/src/formula/Csl/And.h index efed92f17..1453cc30b 100644 --- a/src/formula/Csl/And.h +++ b/src/formula/Csl/And.h @@ -8,8 +8,7 @@ #ifndef STORM_FORMULA_CSL_AND_H_ #define STORM_FORMULA_CSL_AND_H_ -#include "AbstractStateFormula.h" -#include "src/formula/abstract/And.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" #include @@ -54,15 +53,17 @@ class IAndModelChecker { * @see AbstractCslFormula */ template -class And : public storm::property::abstract::And>, public AbstractStateFormula { +class And : public AbstractStateFormula { public: + /*! * Empty constructor. * Will create an AND-node without subnotes. Will not represent a complete formula! */ And() { - //intentionally left empty + left = NULL; + right = NULL; } /*! @@ -72,9 +73,9 @@ public: * @param left The left sub formula * @param right The right sub formula */ - And(AbstractStateFormula* left, AbstractStateFormula* right) - : storm::property::abstract::And>(left, right) { - //intentionally left empty + And(AbstractStateFormula* left, AbstractStateFormula* right) { + this->left = left; + this->right = right; } /*! @@ -84,7 +85,12 @@ public: * (this behavior can be prevented by setting them to NULL before deletion) */ virtual ~And() { - //intentionally left empty + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } } /*! @@ -118,6 +124,80 @@ public: return modelChecker.template as()->checkAnd(*this); } + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "("; + result += left->toString(); + result += " & "; + result += right->toString(); + result += ")"; + return result; + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * @param checker Formula checker object. + * @return true iff all subtrees conform to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->left) && checker.validate(this->right); + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(AbstractStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(AbstractStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + const AbstractStateFormula& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child node + */ + const AbstractStateFormula& getRight() const { + 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; + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; + }; } //namespace csl diff --git a/src/formula/Csl/Ap.h b/src/formula/Csl/Ap.h index cebd9aa49..66f49c503 100644 --- a/src/formula/Csl/Ap.h +++ b/src/formula/Csl/Ap.h @@ -8,8 +8,7 @@ #ifndef STORM_FORMULA_CSL_AP_H_ #define STORM_FORMULA_CSL_AP_H_ -#include "AbstractStateFormula.h" -#include "src/formula/abstract/Ap.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" @@ -47,10 +46,10 @@ class IApModelChecker { * @see AbstractStateFormula */ template -class Ap : public storm::property::abstract::Ap, - public AbstractStateFormula { +class Ap : public AbstractStateFormula { public: + /*! * Constructor * @@ -58,9 +57,8 @@ public: * * @param ap The string representing the atomic proposition */ - Ap(std::string ap) - : storm::property::abstract::Ap(ap) { - // Intentionally left empty + Ap(std::string ap) { + this->ap = ap; } /*! @@ -95,6 +93,36 @@ public: return modelChecker.template as()->checkAp(*this); } + /*! + * @brief Checks if all subtrees conform to some logic. + * + * As atomic propositions have no subformulas, we return true here. + * + * @param checker Formula checker object. + * @return true + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return true; + } + + /*! + * @returns the name of the atomic proposition + */ + const std::string& getAp() const { + return ap; + } + + /*! + * @returns a string representation of the leaf. + * + */ + virtual std::string toString() const override { + return getAp(); + } + +private: + std::string ap; + }; } //namespace abstract diff --git a/src/formula/Csl/Eventually.h b/src/formula/Csl/Eventually.h index 5553d16c7..1d1f1a358 100644 --- a/src/formula/Csl/Eventually.h +++ b/src/formula/Csl/Eventually.h @@ -8,7 +8,6 @@ #ifndef STORM_FORMULA_CSL_EVENTUALLY_H_ #define STORM_FORMULA_CSL_EVENTUALLY_H_ -#include "src/formula/abstract/Eventually.h" #include "src/formula/Csl/AbstractPathFormula.h" #include "src/formula/Csl/AbstractStateFormula.h" #include "src/modelchecker/csl/ForwardDeclarations.h" @@ -53,15 +52,15 @@ class IEventuallyModelChecker { * @see AbstractCslFormula */ template -class Eventually : public storm::property::abstract::Eventually>, - public AbstractPathFormula { +class Eventually : public AbstractPathFormula { public: + /*! * Empty constructor */ - Eventually() { - // Intentionally left empty + Eventually() : child(nullptr) { + // Intentionally left empty. } /*! @@ -69,9 +68,8 @@ public: * * @param child The child node */ - Eventually(AbstractStateFormula* child) - : storm::property::abstract::Eventually>(child) { - + Eventually(AbstractStateFormula* child) : child(child){ + // Intentionally left empty. } /*! @@ -81,7 +79,9 @@ public: * (this behaviour can be prevented by setting the subtrees to nullptr before deletion) */ virtual ~Eventually() { - //intentionally left empty + if (child != nullptr) { + delete child; + } } /*! @@ -111,6 +111,51 @@ public: virtual std::vector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkEventually(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "F "; + result += child->toString(); + return result; + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->child); + } + + /*! + * @returns the child node + */ + const AbstractStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(AbstractStateFormula* child) { + 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; + } + +private: + AbstractStateFormula* child; }; } //namespace csl diff --git a/src/formula/Csl/Globally.h b/src/formula/Csl/Globally.h index 954b59fd4..85cd32396 100644 --- a/src/formula/Csl/Globally.h +++ b/src/formula/Csl/Globally.h @@ -8,9 +8,8 @@ #ifndef STORM_FORMULA_CSL_GLOBALLY_H_ #define STORM_FORMULA_CSL_GLOBALLY_H_ -#include "src/formula/abstract/Globally.h" -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" @@ -54,15 +53,15 @@ class IGloballyModelChecker { * @see AbstractCslFormula */ template -class Globally : public storm::property::abstract::Globally>, - public AbstractPathFormula { +class Globally : public AbstractPathFormula { public: + /*! * Empty constructor */ - Globally() { - //intentionally left empty + Globally() : child(nullptr){ + // Intentionally left empty. } /*! @@ -70,9 +69,8 @@ public: * * @param child The child node */ - Globally(AbstractStateFormula* child) - : storm::property::abstract::Globally>(child) { - //intentionally left empty + Globally(AbstractStateFormula* child) : child(child){ + // Intentionally left empty. } /*! @@ -82,10 +80,11 @@ public: * (this behaviour can be prevented by setting the subtrees to nullptr before deletion) */ virtual ~Globally() { - //intentionally left empty + if (child != nullptr) { + delete child; + } } - /*! * Clones the called object. * @@ -113,6 +112,51 @@ public: virtual std::vector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkGlobally(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "G "; + result += child->toString(); + return result; + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->child); + } + + /*! + * @returns the child node + */ + const AbstractStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(AbstractStateFormula* child) { + 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; + } + +private: + AbstractStateFormula* child; }; } //namespace csl diff --git a/src/formula/Csl/Next.h b/src/formula/Csl/Next.h index 338d119e5..f014190aa 100644 --- a/src/formula/Csl/Next.h +++ b/src/formula/Csl/Next.h @@ -8,9 +8,8 @@ #ifndef STORM_FORMULA_CSL_NEXT_H_ #define STORM_FORMULA_CSL_NEXT_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" -#include "src/formula/abstract/Next.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -53,15 +52,15 @@ class INextModelChecker { * @see AbstractCslFormula */ template -class Next : public storm::property::abstract::Next>, - public AbstractPathFormula { +class Next : public AbstractPathFormula { public: + /*! * Empty constructor */ - Next() { - //intentionally left empty + Next() : child(nullptr){ + // Intentionally left empty. } /*! @@ -69,19 +68,20 @@ public: * * @param child The child node */ - Next(AbstractStateFormula* child) - : storm::property::abstract::Next>(child) { - //intentionally left empty + Next(AbstractStateFormula* child) : child(child){ + // Intentionally left empty. } /*! * Constructor. * * Also deletes the subtree. - * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + * (this behavior can be prevented by setting the subtrees to NULL before deletion) */ virtual ~Next() { - //intentionally left empty + if (child != NULL) { + delete child; + } } /*! @@ -111,6 +111,53 @@ public: virtual std::vector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkNext(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "("; + result += " X "; + result += child->toString(); + result += ")"; + return result; + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->child); + } + + /*! + * @returns the child node + */ + const AbstractStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(AbstractStateFormula* child) { + 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; + } + +private: + AbstractStateFormula* child; }; } //namespace csl diff --git a/src/formula/Csl/Not.h b/src/formula/Csl/Not.h index dd0c2a705..58ca37299 100644 --- a/src/formula/Csl/Not.h +++ b/src/formula/Csl/Not.h @@ -8,8 +8,7 @@ #ifndef STORM_FORMULA_CSL_NOT_H_ #define STORM_FORMULA_CSL_NOT_H_ -#include "AbstractStateFormula.h" -#include "src/formula/abstract/Not.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" @@ -50,24 +49,23 @@ class INotModelChecker { * @see AbstractCslFormula */ template -class Not : public storm::property::abstract::Not>, - public AbstractStateFormula { +class Not : public AbstractStateFormula { public: + /*! * Empty constructor */ Not() { - //intentionally left empty + this->child = NULL; } /*! * Constructor * @param child The child node */ - Not(AbstractStateFormula* child) : - storm::property::abstract::Not>(child){ - //intentionally left empty + Not(AbstractStateFormula* child) { + this->child = child; } /*! @@ -77,7 +75,9 @@ public: * (this behavior can be prevented by setting them to NULL before deletion) */ virtual ~Not() { - //intentionally left empty + if (child != NULL) { + delete child; + } } /*! @@ -107,6 +107,51 @@ public: virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkNot(*this); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "!"; + result += child->toString(); + return result; + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->child); + } + + /*! + * @returns The child node + */ + const AbstractStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(AbstractStateFormula* child) { + 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; + } + +private: + AbstractStateFormula* child; }; } //namespace csl diff --git a/src/formula/Csl/Or.h b/src/formula/Csl/Or.h index 29add98cc..9533b873a 100644 --- a/src/formula/Csl/Or.h +++ b/src/formula/Csl/Or.h @@ -8,8 +8,7 @@ #ifndef STORM_FORMULA_CSL_OR_H_ #define STORM_FORMULA_CSL_OR_H_ -#include "AbstractStateFormula.h" -#include "src/formula/abstract/Or.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -52,39 +51,45 @@ class IOrModelChecker { * @see AbstractCslFormula */ template -class Or : public storm::property::abstract::Or>, - public AbstractStateFormula { +class Or : public AbstractStateFormula { public: - /*! - * Empty constructor. - * Will create an OR-node without subnotes. The result does not represent a complete formula! - */ - Or() { - //intentionally left empty - } /*! - * Constructor. - * Creates an OR note with the parameters as subtrees. - * - * @param left The left sub formula - * @param right The right sub formula - */ - Or(AbstractStateFormula* left, AbstractStateFormula* right) : - storm::property::abstract::Or>(left, right) { - //intentionally left empty - } + * Empty constructor. + * Will create an OR-node without subnotes. Will not represent a complete formula! + */ + Or() { + left = NULL; + right = NULL; + } - /*! - * Destructor. - * - * The subtrees are deleted with the object - * (this behavior can be prevented by setting them to NULL before deletion) - */ - virtual ~Or() { - //intentionally left empty - } + /*! + * Constructor. + * Creates an OR note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + Or(AbstractStateFormula* left, AbstractStateFormula* 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; + } + } /*! * Clones the called object. @@ -116,6 +121,81 @@ public: virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkOr(*this); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "("; + result += left->toString(); + result += " | "; + result += right->toString(); + result += ")"; + return result; + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * @param checker Formula checker object. + * @return true iff all subtrees conform to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->left) && checker.validate(this->right); + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(AbstractStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(AbstractStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + const AbstractStateFormula& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child node + */ + const AbstractStateFormula& getRight() const { + 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; + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; + }; } //namespace csl diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h index 28937fab4..4b4e5d937 100644 --- a/src/formula/Csl/ProbabilisticBoundOperator.h +++ b/src/formula/Csl/ProbabilisticBoundOperator.h @@ -8,9 +8,9 @@ #ifndef STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ #define STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ -#include "AbstractStateFormula.h" -#include "AbstractPathFormula.h" -#include "src/formula/abstract/ProbabilisticBoundOperator.h" +#include "src/formula/Csl/AbstractStateFormula.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/ComparisonType.h" #include "utility/constants.h" namespace storm { @@ -53,36 +53,39 @@ class IProbabilisticBoundOperatorModelChecker { * @see AbstractCslFormula */ template -class ProbabilisticBoundOperator : public storm::property::abstract::ProbabilisticBoundOperator>, - public AbstractStateFormula { +class ProbabilisticBoundOperator : public AbstractStateFormula { public: + /*! * Empty constructor */ - ProbabilisticBoundOperator() : storm::property::abstract::ProbabilisticBoundOperator> - (LESS_EQUAL, storm::utility::constantZero(), nullptr) { - // Intentionally left empty + ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr) { + // Intentionally left empty. } - /*! - * Constructor + * Constructor for non-optimizing operator. * - * @param comparisonRelation The relation to compare the actual value and the bound + * @param comparisonOperator The relation for the bound. * @param bound The bound for the probability * @param pathFormula The child node */ - ProbabilisticBoundOperator( - storm::property::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) - : storm::property::abstract::ProbabilisticBoundOperator>(comparisonRelation, bound, pathFormula) { - // Intentionally left empty + ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) + : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { + // Intentionally left empty. } - ProbabilisticBoundOperator( - storm::property::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) - : storm::property::abstract::ProbabilisticBoundOperator>(comparisonRelation, bound, pathFormula, minimumOperator){ - // Intentionally left empty + /*! + * Destructor + * + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~ProbabilisticBoundOperator() { + if (pathFormula != nullptr) { + delete pathFormula; + } } /*! @@ -112,6 +115,101 @@ public: virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkProbabilisticBoundOperator(*this); } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->pathFormula); + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "P "; + switch (comparisonOperator) { + case LESS: result += "<"; break; + case LESS_EQUAL: result += "<="; break; + case GREATER: result += ">"; break; + case GREATER_EQUAL: result += ">="; break; + } + result += " "; + result += std::to_string(bound); + result += " ["; + result += pathFormula->toString(); + result += "]"; + return result; + } + + /*! + * @returns the child node (representation of a formula) + */ + const AbstractPathFormula& getPathFormula () const { + return *pathFormula; + } + + /*! + * Sets the child node + * + * @param pathFormula the path formula that becomes the new child node + */ + void setPathFormula(AbstractPathFormula* pathFormula) { + 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 + */ + const storm::property::ComparisonType getComparisonOperator() const { + return comparisonOperator; + } + + void setComparisonOperator(storm::property::ComparisonType comparisonOperator) { + this->comparisonOperator = comparisonOperator; + } + + /*! + * @returns the bound for the measure + */ + const T& getBound() const { + return bound; + } + + /*! + * Sets the interval in which the probability that the path formula holds may lie in. + * + * @param bound The bound for the measure + */ + void setBound(T bound) { + this->bound = bound; + } + + bool meetsBound(T value) const { + switch (comparisonOperator) { + case LESS: return value < bound; break; + case LESS_EQUAL: return value <= bound; break; + case GREATER: return value > bound; break; + case GREATER_EQUAL: return value >= bound; break; + default: return false; + } + } + +private: + storm::property::ComparisonType comparisonOperator; + T bound; + AbstractPathFormula* pathFormula; }; } //namespace csl diff --git a/src/formula/Csl/ProbabilisticNoBoundOperator.h b/src/formula/Csl/ProbabilisticNoBoundOperator.h deleted file mode 100644 index 63c9a501e..000000000 --- a/src/formula/Csl/ProbabilisticNoBoundOperator.h +++ /dev/null @@ -1,115 +0,0 @@ -/* - * ProbabilisticNoBoundOperator.h - * - * Created on: 12.12.2012 - * Author: thomas - */ - -#ifndef STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ -#define STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ - -#include "AbstractPathFormula.h" -#include "AbstractNoBoundOperator.h" -#include "src/formula/abstract/ProbabilisticNoBoundOperator.h" - -namespace storm { -namespace property { -namespace csl { - -/*! - * @brief - * 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 - * (for each state) - * - * Has one Abstract path formula as sub formula/tree. - * - * @note - * This class is a hybrid of a state and path formula, and may only appear as the outermost operator. - * Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula. - * - * @note - * This class does not contain a check() method like the other formula classes. - * The check method should only be called by the model checker to infer the correct check function for sub - * formulas. As this operator can only appear at the root, the method is not useful here. - * Use the checkProbabilisticNoBoundOperator method from the DtmccslModelChecker class instead. - * - * 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 AbstractStateFormula - * @see AbstractPathFormula - * @see ProbabilisticOperator - * @see ProbabilisticIntervalOperator - * @see AbstractCslFormula - */ -template -class ProbabilisticNoBoundOperator: public storm::property::abstract::ProbabilisticNoBoundOperator>, - public AbstractNoBoundOperator { -public: - /*! - * Empty constructor - */ - ProbabilisticNoBoundOperator() { - // Intentionally left empty - } - - /*! - * Constructor - * - * @param pathFormula The child node. - */ - ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) - : storm::property::abstract::ProbabilisticNoBoundOperator>(pathFormula) { - // Intentionally left empty - } - - /*! - * Constructor - * - * @param pathFormula The child node. - */ - ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) - : storm::property::abstract::ProbabilisticNoBoundOperator>(pathFormula, minimumOperator) { - // Intentionally left empty - } - - /*! - * Destructor - */ - virtual ~ProbabilisticNoBoundOperator() { - // Intentionally left empty - } - - virtual AbstractNoBoundOperator* clone() const override { - ProbabilisticNoBoundOperator* result = new ProbabilisticNoBoundOperator(); - if (this->pathFormulaIsSet()) { - result->setPathFormula(this->getPathFormula().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. - * - * @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 check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { - return this->getPathFormula().check(modelChecker, qualitative); - } -}; - -} //namespace csl -} //namespace property -} //namespace storm - -#endif /* STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h index ddd9be3b2..c8d9e8de4 100644 --- a/src/formula/Csl/SteadyStateBoundOperator.h +++ b/src/formula/Csl/SteadyStateBoundOperator.h @@ -9,13 +9,11 @@ #define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ #include "AbstractStateFormula.h" -#include "src/formula/abstract/SteadyStateBoundOperator.h" #include "src/formula/AbstractFormulaChecker.h" +#include "src/formula/ComparisonType.h" namespace storm { - namespace property { - namespace csl { template class SteadyStateBoundOperator; @@ -54,33 +52,39 @@ class ISteadyStateBoundOperatorModelChecker { * @see AbstractCslFormula */ template -class SteadyStateBoundOperator : public storm::property::abstract::SteadyStateBoundOperator>, - public AbstractStateFormula { +class SteadyStateBoundOperator : public AbstractStateFormula { public: + /*! * Empty constructor */ - SteadyStateBoundOperator() : storm::property::abstract::SteadyStateBoundOperator> - (LESS_EQUAL, storm::utility::constantZero(), nullptr) { + SteadyStateBoundOperator() : comparisonOperator(LESS), bound(storm::utility::constantZero()), stateFormula(nullptr) { // Intentionally left empty } /*! * Constructor * + * @param comparisonOperator The relation for the bound. + * @param bound The bound for the probability * @param stateFormula The child node */ - SteadyStateBoundOperator( - storm::property::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : - storm::property::abstract::SteadyStateBoundOperator>(comparisonRelation, bound, stateFormula) { + SteadyStateBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractStateFormula* stateFormula) + : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { + // Intentionally left empty } /*! * Destructor + * + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) */ virtual ~SteadyStateBoundOperator() { - // Intentionally left empty + if (stateFormula != nullptr) { + delete stateFormula; + } } /*! @@ -108,7 +112,100 @@ public: virtual storm::storage::BitVector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkSteadyStateBoundOperator(*this); } - + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->stateFormula); + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "S "; + switch (comparisonOperator) { + case LESS: result += "< "; break; + case LESS_EQUAL: result += "<= "; break; + case GREATER: result += "> "; break; + case GREATER_EQUAL: result += ">= "; break; + } + result += std::to_string(bound); + result += " ["; + result += stateFormula->toString(); + result += "]"; + return result; + } + + /*! + * @returns the child node (representation of a formula) + */ + const AbstractStateFormula& getStateFormula () const { + return *stateFormula; + } + + /*! + * Sets the child node + * + * @param stateFormula the state formula that becomes the new child node + */ + void setStateFormula(AbstractStateFormula* stateFormula) { + 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 + */ + const ComparisonType getComparisonOperator() const { + return comparisonOperator; + } + + void setComparisonOperator(ComparisonType comparisonOperator) { + this->comparisonOperator = comparisonOperator; + } + + /*! + * @returns the bound for the measure + */ + const T& getBound() const { + return bound; + } + + /*! + * Sets the interval in which the probability that the path formula holds may lie in. + * + * @param bound The bound for the measure + */ + void setBound(T bound) { + this->bound = bound; + } + + bool meetsBound(T value) const { + switch (comparisonOperator) { + case LESS: return value < bound; break; + case LESS_EQUAL: return value <= bound; break; + case GREATER: return value > bound; break; + case GREATER_EQUAL: return value >= bound; break; + default: return false; + } + } + +private: + ComparisonType comparisonOperator; + T bound; + AbstractStateFormula* stateFormula; }; } //namespace csl diff --git a/src/formula/Csl/SteadyStateNoBoundOperator.h b/src/formula/Csl/SteadyStateNoBoundOperator.h deleted file mode 100644 index b92526d47..000000000 --- a/src/formula/Csl/SteadyStateNoBoundOperator.h +++ /dev/null @@ -1,100 +0,0 @@ -/* - * SteadyStateNoBoundOperator.h - * - * Created on: 09.04.2013 - * Author: thomas - */ - -#ifndef STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ -#define STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ - -#include "AbstractStateFormula.h" -#include "AbstractNoBoundOperator.h" -#include "src/formula/abstract/SteadyStateNoBoundOperator.h" - -namespace storm { -namespace property { -namespace csl { - -template class SteadyStateNoBoundOperator; - -/*! - * @brief Interface class for model checkers that support SteadyStateOperator. - * - * All model checkers that support the formula class SteadyStateOperator must inherit - * this pure virtual class. - */ -template -class ISteadyStateNoBoundOperatorModelChecker { - public: - /*! - * @brief Evaluates SteadyStateOperator formula within a model checker. - * - * @param obj Formula object with subformulas. - * @return Result of the formula for every node. - */ - virtual std::vector checkSteadyStateNoBoundOperator(const SteadyStateNoBoundOperator& obj) const = 0; -}; - -template -class SteadyStateNoBoundOperator: public storm::property::abstract::SteadyStateNoBoundOperator>, - public AbstractNoBoundOperator { -public: - /*! - * Empty constructor - */ - SteadyStateNoBoundOperator() : storm::property::abstract::SteadyStateNoBoundOperator>() { - // Intentionally left empty - - } - - /*! - * Constructor - * - * @param stateFormula The state formula that forms the subtree - */ - SteadyStateNoBoundOperator(AbstractStateFormula* stateFormula) - : storm::property::abstract::SteadyStateNoBoundOperator>(stateFormula) { - // Intentionally left empty - } - - /*! - * Destructor - */ - ~SteadyStateNoBoundOperator() { - // Intentionally left empty - } - - /*! - * 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 AbstractNoBoundOperator * clone() const override { - SteadyStateNoBoundOperator* result = new SteadyStateNoBoundOperator(); - result->setStateFormula(this->getStateFormula().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 check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { - return modelChecker.template as()->checkSteadyStateNoBoundOperator(*this); - } - -}; - -} /* namespace csl */ -} /* namespace property */ -} /* namespace storm */ - -#endif /* STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/TimeBoundedEventually.h b/src/formula/Csl/TimeBoundedEventually.h index 3b443938a..ac601b7d8 100644 --- a/src/formula/Csl/TimeBoundedEventually.h +++ b/src/formula/Csl/TimeBoundedEventually.h @@ -8,9 +8,8 @@ #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ #define STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ -#include "src/formula/abstract/TimeBoundedEventually.h" -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" namespace storm { namespace property { @@ -38,27 +37,27 @@ class ITimeBoundedEventuallyModelChecker { template -class TimeBoundedEventually: public storm::property::abstract::TimeBoundedEventually>, - public AbstractPathFormula { +class TimeBoundedEventually: public AbstractPathFormula { public: + /** * Simple constructor: Only sets the bounds * * @param lowerBound * @param upperBound */ - TimeBoundedEventually(T lowerBound, T upperBound) - : storm::property::abstract::TimeBoundedEventually>(lowerBound, upperBound) { - // Intentionally left empty + TimeBoundedEventually(T lowerBound, T upperBound) : child(nullptr) { + setInterval(lowerBound, upperBound); } - TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula* child) - : storm::property::abstract::TimeBoundedEventually>(lowerBound, upperBound, child) { - // Intentionally left empty + TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula* child) : child(nullptr) { + setInterval(lowerBound, upperBound); } virtual ~TimeBoundedEventually() { - // Intentionally left empty + if (child != nullptr) { + delete child; + } } /*! @@ -88,6 +87,94 @@ public: virtual std::vector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkTimeBoundedEventually(*this, qualitative); } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->child); + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "F"; + if (upperBound == std::numeric_limits::infinity()) { + result = ">=" + std::to_string(lowerBound); + } else { + result = "["; + result += std::to_string(lowerBound); + result += ","; + result += std::to_string(upperBound); + result += "]"; + } + result += " "; + result += child->toString(); + return result; + } + + /*! + * @returns the child node + */ + const AbstractStateFormula& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(AbstractStateFormula* child) { + 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; + } + + /** + * Getter for lowerBound attribute + * + * @return lower bound of the operator. + */ + T getLowerBound() const { + return lowerBound; + } + + /** + * Getter for upperBound attribute + * @return upper bound of the operator. + */ + T getUpperBound() const { + return upperBound; + } + + /** + * Set the time interval for the time bounded operator + * + * @param lowerBound + * @param upperBound + * @throw InvalidArgumentException if the lower bound is larger than the upper bound. + */ + void setInterval(T lowerBound, T upperBound) { + if (lowerBound > upperBound) { + throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound"); + } + this->lowerBound = lowerBound; + this->upperBound = upperBound; + } + +private: + AbstractStateFormula* child; + T lowerBound, upperBound; }; } /* namespace csl */ diff --git a/src/formula/Csl/TimeBoundedUntil.h b/src/formula/Csl/TimeBoundedUntil.h index 7b2044daa..560bb8df8 100644 --- a/src/formula/Csl/TimeBoundedUntil.h +++ b/src/formula/Csl/TimeBoundedUntil.h @@ -8,9 +8,8 @@ #ifndef STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ #define STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" -#include "src/formula/abstract/TimeBoundedUntil.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" namespace storm { namespace property { @@ -37,9 +36,9 @@ class ITimeBoundedUntilModelChecker { }; template -class TimeBoundedUntil: public storm::property::abstract::TimeBoundedUntil>, - public AbstractPathFormula { +class TimeBoundedUntil: public AbstractPathFormula { public: + /** * Constructor providing bounds only; * Sub formulas are set to null. @@ -47,11 +46,11 @@ public: * @param lowerBound * @param upperBound */ - TimeBoundedUntil(T lowerBound, T upperBound) : - storm::property::abstract::TimeBoundedUntil>(lowerBound, upperBound) { - // Intentionally left empty + TimeBoundedUntil(T lowerBound, T upperBound) : left(nullptr), right(nullptr) { + setInterval(lowerBound, upperBound); } + /** * Full constructor * @param lowerBound @@ -59,16 +58,20 @@ public: * @param left * @param right */ - TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula* left, AbstractStateFormula* right) : - storm::property::abstract::TimeBoundedUntil>(lowerBound, upperBound, left, right) { - + TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula* left, AbstractStateFormula* right) : left(left), right(right) { + setInterval(lowerBound, upperBound); } /*! * Destructor */ virtual ~TimeBoundedUntil() { - // Intentionally left empty + if (left != nullptr) { + delete left; + } + if (right != nullptr) { + delete right; + } } /*! @@ -102,6 +105,121 @@ public: virtual std::vector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkTimeBoundedUntil(*this, qualitative); } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->left) && checker.validate(this->right); + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = left->toString(); + result += " U"; + if (upperBound == std::numeric_limits::infinity()) { + result = ">=" + std::to_string(lowerBound); + } else { + result = "["; + result += std::to_string(lowerBound); + result += ","; + result += std::to_string(upperBound); + result += "]"; + } + result += " "; + result += right->toString(); + return result; + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(AbstractStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(AbstractStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + const AbstractStateFormula& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child node + */ + const AbstractStateFormula& getRight() const { + 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; + } + + /** + * Getter for lowerBound attribute + * + * @return lower bound of the operator. + */ + T getLowerBound() const { + return lowerBound; + } + + /** + * Getter for upperBound attribute + * @return upper bound of the operator. + */ + T getUpperBound() const { + return upperBound; + } + + /** + * Set the time interval for the time bounded operator + * + * @param lowerBound + * @param upperBound + * @throw InvalidArgumentException if the lower bound is larger than the upper bound. + */ + void setInterval(T lowerBound, T upperBound) { + if (lowerBound > upperBound) { + throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound"); + } + this->lowerBound = lowerBound; + this->upperBound = upperBound; + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; + T lowerBound, upperBound; }; } /* namespace csl */ diff --git a/src/formula/Csl/Until.h b/src/formula/Csl/Until.h index 6f6d68086..34b44b780 100644 --- a/src/formula/Csl/Until.h +++ b/src/formula/Csl/Until.h @@ -8,9 +8,8 @@ #ifndef STORM_FORMULA_CSL_UNTIL_H_ #define STORM_FORMULA_CSL_UNTIL_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" -#include "src/formula/abstract/Until.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -54,15 +53,14 @@ class IUntilModelChecker { * @see AbstractCslFormula */ template -class Until : public storm::property::abstract::Until>, - public AbstractPathFormula { +class Until : public AbstractPathFormula { public: /*! * Empty constructor */ - Until() { - // Intentionally left empty + Until() : left(nullptr), right(nullptr){ + // Intentionally left empty. } /*! @@ -71,9 +69,8 @@ public: * @param left The left formula subtree * @param right The left formula subtree */ - Until(AbstractStateFormula* left, AbstractStateFormula* right) - : storm::property::abstract::Until>(left, right) { - // Intentionally left empty + Until(AbstractStateFormula* left, AbstractStateFormula* right) : left(left), right(right){ + // Intentionally left empty. } /*! @@ -83,7 +80,12 @@ public: * (this behaviour can be prevented by setting the subtrees to NULL before deletion) */ virtual ~Until() { - // Intentionally left empty + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } } /*! @@ -116,6 +118,78 @@ public: virtual std::vector check(const storm::modelchecker::csl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkUntil(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = left->toString(); + result += " U "; + result += right->toString(); + return result; + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * @param checker Formula checker object. + * @return true iff all subtrees conform to some logic. + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return checker.validate(this->left) && checker.validate(this->right); + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(AbstractStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(AbstractStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + const AbstractStateFormula& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child node + */ + const AbstractStateFormula& getRight() const { + 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; + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; }; } //namespace csl diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h index b10a9e92a..7eed7fb6a 100644 --- a/src/formula/Prctl/AbstractStateFormula.h +++ b/src/formula/Prctl/AbstractStateFormula.h @@ -26,7 +26,7 @@ namespace prctl { * clone(). */ template -class AbstractStateFormula : public virtual storm::property::prctl::AbstractPrctlFormula { +class AbstractStateFormula : public storm::property::prctl::AbstractPrctlFormula { public: /*! diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h index eeb52e37f..67a824254 100644 --- a/src/formula/Prctl/Globally.h +++ b/src/formula/Prctl/Globally.h @@ -8,8 +8,8 @@ #ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_ #define STORM_FORMULA_PRCTL_GLOBALLY_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" +#include "src/formula/Prctl/AbstractPathFormula.h" +#include "src/formula/Prctl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" @@ -85,7 +85,6 @@ public: } } - /*! * Clones the called object. * diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h index a50cfd005..776195903 100644 --- a/src/formula/Prctl/Next.h +++ b/src/formula/Prctl/Next.h @@ -8,8 +8,8 @@ #ifndef STORM_FORMULA_PRCTL_NEXT_H_ #define STORM_FORMULA_PRCTL_NEXT_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" +#include "src/formula/Prctl/AbstractPathFormula.h" +#include "src/formula/Prctl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h index 231ced8d9..65a06be3a 100644 --- a/src/formula/Prctl/Not.h +++ b/src/formula/Prctl/Not.h @@ -52,6 +52,7 @@ template class Not : public AbstractStateFormula { public: + /*! * Empty constructor */ diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h index 3f1b83f36..dc92ee10a 100644 --- a/src/formula/Prctl/Or.h +++ b/src/formula/Prctl/Or.h @@ -54,9 +54,10 @@ template class Or : public AbstractStateFormula { public: + /*! * Empty constructor. - * Will create an AND-node without subnotes. Will not represent a complete formula! + * Will create an OR-node without subnotes. Will not represent a complete formula! */ Or() { left = NULL; @@ -65,7 +66,7 @@ public: /*! * Constructor. - * Creates an AND note with the parameters as subtrees. + * Creates an OR note with the parameters as subtrees. * * @param left The left sub formula * @param right The right sub formula diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h index d1d3bc1dc..36499884a 100644 --- a/src/modelchecker/csl/AbstractModelChecker.h +++ b/src/modelchecker/csl/AbstractModelChecker.h @@ -46,7 +46,6 @@ class AbstractModelChecker : public virtual storm::property::csl::INextModelChecker, public virtual storm::property::csl::ITimeBoundedUntilModelChecker, public virtual storm::property::csl::ITimeBoundedEventuallyModelChecker, - public virtual storm::property::csl::INoBoundOperatorModelChecker, public virtual storm::property::csl::IProbabilisticBoundOperatorModelChecker { public: