diff --git a/src/formula/Prctl.h b/src/formula/Prctl.h index 87466f55f..5f12911ea 100644 --- a/src/formula/Prctl.h +++ b/src/formula/Prctl.h @@ -17,7 +17,6 @@ #include "Prctl/Next.h" #include "Prctl/Not.h" #include "Prctl/Or.h" -#include "Prctl/ProbabilisticNoBoundOperator.h" #include "Prctl/ProbabilisticBoundOperator.h" #include "Prctl/Until.h" @@ -29,12 +28,10 @@ #include "Prctl/CumulativeReward.h" #include "Prctl/ReachabilityReward.h" #include "Prctl/RewardBoundOperator.h" -#include "Prctl/RewardNoBoundOperator.h" #include "Prctl/SteadyStateReward.h" #include "Prctl/AbstractPrctlFormula.h" #include "Prctl/AbstractStateFormula.h" -#include "Prctl/AbstractNoBoundOperator.h" #include "Prctl/AbstractPathFormula.h" #include "modelchecker/prctl/AbstractModelChecker.h" diff --git a/src/formula/Prctl/AbstractNoBoundOperator.h b/src/formula/Prctl/AbstractNoBoundOperator.h deleted file mode 100644 index 4605a590d..000000000 --- a/src/formula/Prctl/AbstractNoBoundOperator.h +++ /dev/null @@ -1,83 +0,0 @@ -/* - * AbstractNoBoundOperator.h - * - * Created on: 16.04.2013 - * Author: thomas - */ - -#ifndef STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ -#define STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ - -#include "src/formula/AbstractFormula.h" -#include "src/formula/abstract/IOptimizingOperator.h" - -namespace storm { -namespace property { -namespace prctl { - -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 PRCTL No bound operators - */ -template -class AbstractNoBoundOperator: public storm::property::AbstractFormula, - public virtual storm::property::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::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const = 0; -}; - -} /* namespace prctl */ -} /* namespace property */ -} /* namespace storm */ -#endif /* STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h index c7e20b9c6..1c0be2dd6 100644 --- a/src/formula/Prctl/AbstractPathFormula.h +++ b/src/formula/Prctl/AbstractPathFormula.h @@ -8,7 +8,7 @@ #ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_ #define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_ -#include "src/formula/AbstractFormula.h" +#include "src/formula/Prctl/AbstractPrctlFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" #include @@ -31,7 +31,7 @@ namespace prctl { * @note This class is intentionally not derived from AbstractPrctlFormula, as path formulas are not complete PRCTL formulas. */ template -class AbstractPathFormula : public virtual storm::property::AbstractFormula { +class AbstractPathFormula : public virtual storm::property::prctl::AbstractPrctlFormula { public: /*! diff --git a/src/formula/Prctl/AbstractPrctlFormula.h b/src/formula/Prctl/AbstractPrctlFormula.h new file mode 100644 index 000000000..3beddb206 --- /dev/null +++ b/src/formula/Prctl/AbstractPrctlFormula.h @@ -0,0 +1,31 @@ +/* + * AbstractPrctlFormula.h + * + * Created on: 16.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_ +#define STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_ + +#include "src/formula/AbstractFormula.h" + +namespace storm { +namespace property { +namespace prctl { + +/*! + * Interface class for all PRCTL root formulas. + */ +template +class AbstractPrctlFormula : public virtual storm::property::AbstractFormula { +public: + virtual ~AbstractPrctlFormula() { + // Intentionally left empty + } +}; + +} /* namespace prctl */ +} /* namespace property */ +} /* namespace storm */ +#endif /* ABSTRACTPRCTLFORMULA_H_ */ diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h index 1142d7754..b10a9e92a 100644 --- a/src/formula/Prctl/AbstractStateFormula.h +++ b/src/formula/Prctl/AbstractStateFormula.h @@ -8,7 +8,7 @@ #ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_ #define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_ -#include "src/formula/AbstractFormula.h" +#include "src/formula/Prctl/AbstractPrctlFormula.h" #include "src/storage/BitVector.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" @@ -26,7 +26,7 @@ namespace prctl { * clone(). */ template -class AbstractStateFormula : public virtual storm::property::AbstractFormula { +class AbstractStateFormula : public virtual storm::property::prctl::AbstractPrctlFormula { public: /*! diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h index 870d88e1d..0da53493f 100644 --- a/src/formula/Prctl/BoundedEventually.h +++ b/src/formula/Prctl/BoundedEventually.h @@ -8,7 +8,6 @@ #ifndef STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_ #define STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_ -#include "src/formula/abstract/BoundedEventually.h" #include "src/formula/Prctl/AbstractPathFormula.h" #include "src/formula/Prctl/AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" @@ -56,15 +55,14 @@ class IBoundedEventuallyModelChecker { * @see AbstractPrctlFormula */ template -class BoundedEventually : public storm::property::abstract::BoundedEventually>, - public AbstractPathFormula { +class BoundedEventually : public AbstractPathFormula { public: /*! * Empty constructor */ - BoundedEventually() { - //intentionally left empty + BoundedEventually() : child(nullptr), bound(0){ + // Intentionally left empty. } /*! @@ -73,9 +71,8 @@ public: * @param child The child formula subtree * @param bound The maximal number of steps */ - BoundedEventually(AbstractStateFormula* child, uint_fast64_t bound) : - storm::property::abstract::BoundedEventually>(child, bound){ - //intentionally left empty + BoundedEventually(AbstractStateFormula* child, uint_fast64_t bound) : child(child), bound(bound){ + // Intentionally left empty. } /*! @@ -85,7 +82,9 @@ public: * (this behaviour can be prevented by setting the subtrees to NULL before deletion) */ virtual ~BoundedEventually() { - //intentionally left empty + if (child != nullptr) { + delete child; + } } /*! @@ -117,6 +116,70 @@ public: virtual std::vector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkBoundedEventually(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "F<="; + result += std::to_string(bound); + 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 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 + */ + uint_fast64_t getBound() const { + 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; + } + +private: + AbstractStateFormula* child; + uint_fast64_t bound; }; } //namespace prctl diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h index e01169496..f59431447 100644 --- a/src/formula/Prctl/BoundedNaryUntil.h +++ b/src/formula/Prctl/BoundedNaryUntil.h @@ -8,7 +8,6 @@ #ifndef STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_ #define STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_ -#include "src/formula/abstract/BoundedNaryUntil.h" #include "src/formula/Prctl/AbstractPathFormula.h" #include "src/formula/Prctl/AbstractStateFormula.h" #include @@ -63,15 +62,16 @@ class IBoundedNaryUntilModelChecker { * @see AbstractPrctlFormula */ template -class BoundedNaryUntil : public storm::property::abstract::BoundedNaryUntil>, - public AbstractPathFormula { +class BoundedNaryUntil : public AbstractPathFormula { public: + /*! * Empty constructor */ BoundedNaryUntil() { - + this->left = nullptr; + this->right = new std::vector*,T,T>>(); } /*! @@ -80,9 +80,9 @@ public: * @param left The left formula subtree * @param right The left formula subtree */ - BoundedNaryUntil(AbstractStateFormula* left, std::vector*,T,T>>* right) : - storm::property::abstract::BoundedNaryUntil>(left, right){ - + BoundedNaryUntil(AbstractStateFormula* left, std::vector*,T,T>>* right) { + this->left = left; + this->right = right; } /*! @@ -92,10 +92,14 @@ public: * (this behaviour can be prevented by setting the subtrees to NULL before deletion) */ virtual ~BoundedNaryUntil() { - //intentionally left empty + if (left != nullptr) { + delete left; + } + if (right != nullptr) { + delete right; + } } - /*! * Clones the called object. * @@ -132,6 +136,89 @@ public: return modelChecker.template as()->checkBoundedNaryUntil(*this, qualitative); } + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::stringstream result; + result << "( " << left->toString(); + for (auto it = this->right->begin(); it != this->right->end(); ++it) { + result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString(); + } + result << ")"; + return result.str(); + } + + /*! + * @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 { + bool res = checker.validate(this->left); + for (auto it = this->right->begin(); it != this->right->end(); ++it) { + res &= checker.validate(std::get<0>(*it)); + } + return res; + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(AbstractStateFormula* newLeft) { + left = newLeft; + } + + void setRight(std::vector*,T,T>>* newRight) { + 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. + * + * @param newRight the new right child. + */ + void addRight(AbstractStateFormula* newRight, T upperBound, T lowerBound) { + this->right->push_back(std::tuple*,T,T>(newRight, upperBound, lowerBound)); + } + + /*! + * @returns a pointer to the left child node + */ + const AbstractStateFormula& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child nodes. + */ + const std::vector*,T,T>>& getRight() const { + return *right; + } + + +private: + AbstractStateFormula* left; + std::vector*,T,T>>* right; }; } //namespace prctl diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h index f17c9b743..d7c9d28ca 100644 --- a/src/formula/Prctl/BoundedUntil.h +++ b/src/formula/Prctl/BoundedUntil.h @@ -8,7 +8,6 @@ #ifndef STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ #define STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ -#include "src/formula/abstract/BoundedUntil.h" #include "src/formula/Prctl/AbstractPathFormula.h" #include "src/formula/Prctl/AbstractStateFormula.h" #include @@ -56,15 +55,15 @@ class IBoundedUntilModelChecker { * @see AbstractPrctlFormula */ template -class BoundedUntil : public storm::property::abstract::BoundedUntil>, - public AbstractPathFormula { +class BoundedUntil : public AbstractPathFormula { public: + /*! * Empty constructor */ - BoundedUntil() { - //Intentionally left empty + BoundedUntil() : left(nullptr), right(nullptr), bound(0){ + // Intentionally left empty. } /*! @@ -74,12 +73,11 @@ public: * @param right The left formula subtree * @param bound The maximal number of steps */ - BoundedUntil(AbstractStateFormula* left, AbstractStateFormula* right, - uint_fast64_t bound) : - storm::property::abstract::BoundedUntil>(left,right,bound) { - //intentionally left empty + BoundedUntil(AbstractStateFormula* left, AbstractStateFormula* right, uint_fast64_t bound) { + this->left = left; + this->right = right; + this->bound = bound; } - /*! * Destructor. * @@ -87,7 +85,12 @@ public: * (this behaviour can be prevented by setting the subtrees to NULL before deletion) */ virtual ~BoundedUntil() { - //intentionally left empty + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } } /*! @@ -122,6 +125,97 @@ public: virtual std::vector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkBoundedUntil(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = left->toString(); + result += " U<="; + result += std::to_string(bound); + result += " "; + 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; + } + + /*! + * @returns the maximally allowed number of steps for the bounded until operator + */ + uint_fast64_t getBound() const { + 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; + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; + uint_fast64_t bound; }; } //namespace prctl diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h index e1db7cb21..a31f75a5d 100644 --- a/src/formula/Prctl/CumulativeReward.h +++ b/src/formula/Prctl/CumulativeReward.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/abstract/CumulativeReward.h" #include "src/formula/AbstractFormulaChecker.h" #include @@ -49,14 +48,13 @@ class ICumulativeRewardModelChecker { * @see AbstractPrctlFormula */ template -class CumulativeReward : public storm::property::abstract::CumulativeReward, - public AbstractPathFormula { +class CumulativeReward : public AbstractPathFormula { public: /*! * Empty constructor */ - CumulativeReward() { + CumulativeReward() : bound(0){ // Intentionally left empty } @@ -65,9 +63,8 @@ public: * * @param bound The time bound of the reward formula */ - CumulativeReward(T bound) : - storm::property::abstract::CumulativeReward(bound) { - // Intentionally left empty + CumulativeReward(T bound) : bound(bound){ + // Intentionally left empty. } /*! @@ -101,6 +98,46 @@ public: virtual std::vector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkCumulativeReward(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "C <= "; + result += std::to_string(bound); + return result; + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * As CumulativeReward objects 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 time instance for the instantaneous reward operator + */ + T getBound() const { + return bound; + } + + /*! + * Sets the the time instance for the instantaneous reward operator + * + * @param bound the new bound. + */ + void setBound(T bound) { + this->bound = bound; + } + +private: + T bound; }; } //namespace prctl diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h index 4a0624df6..733fc924b 100644 --- a/src/formula/Prctl/Eventually.h +++ b/src/formula/Prctl/Eventually.h @@ -8,7 +8,6 @@ #ifndef STORM_FORMULA_PRCTL_EVENTUALLY_H_ #define STORM_FORMULA_PRCTL_EVENTUALLY_H_ -#include "src/formula/abstract/Eventually.h" #include "src/formula/Prctl/AbstractPathFormula.h" #include "src/formula/Prctl/AbstractStateFormula.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" @@ -53,15 +52,15 @@ class IEventuallyModelChecker { * @see AbstractPrctlFormula */ 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::prctl::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 prctl diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h index 272bbab26..eeb52e37f 100644 --- a/src/formula/Prctl/Globally.h +++ b/src/formula/Prctl/Globally.h @@ -8,7 +8,6 @@ #ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_ #define STORM_FORMULA_PRCTL_GLOBALLY_H_ -#include "src/formula/abstract/Globally.h" #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" #include "src/formula/AbstractFormulaChecker.h" @@ -54,15 +53,15 @@ class IGloballyModelChecker { * @see AbstractPrctlFormula */ 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,7 +80,9 @@ public: * (this behaviour can be prevented by setting the subtrees to nullptr before deletion) */ virtual ~Globally() { - //intentionally left empty + if (child != nullptr) { + delete child; + } } @@ -113,6 +113,51 @@ public: virtual std::vector check(const storm::modelchecker::prctl::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 prctl diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h index b28effffe..774d07e5e 100644 --- a/src/formula/Prctl/InstantaneousReward.h +++ b/src/formula/Prctl/InstantaneousReward.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/abstract/InstantaneousReward.h" #include "src/formula/AbstractFormulaChecker.h" #include #include @@ -50,15 +49,15 @@ class IInstantaneousRewardModelChecker { * @see AbstractPrctlFormula */ template -class InstantaneousReward : public storm::property::abstract::InstantaneousReward, - public AbstractPathFormula { +class InstantaneousReward : public AbstractPathFormula { public: + /*! * Empty constructor */ - InstantaneousReward() { - //intentionally left empty + InstantaneousReward() : bound(0) { + // Intentionally left empty. } /*! @@ -66,9 +65,8 @@ public: * * @param bound The time instance of the reward formula */ - InstantaneousReward(uint_fast64_t bound) : - storm::property::abstract::InstantaneousReward(bound) { - //intentionally left empty + InstantaneousReward(uint_fast64_t bound) : bound(bound) { + // Intentionally left empty. } /*! @@ -102,6 +100,46 @@ public: virtual std::vector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkInstantaneousReward(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + std::string result = "I="; + result += std::to_string(bound); + return result; + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * As InstantaneousReward formulas 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 time instance for the instantaneous reward operator + */ + uint_fast64_t getBound() const { + return bound; + } + + /*! + * Sets the the time instance for the instantaneous reward operator + * + * @param bound the new bound. + */ + void setBound(uint_fast64_t bound) { + this->bound = bound; + } + +private: + uint_fast64_t bound; }; } //namespace prctl diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h index 7197da30c..a50cfd005 100644 --- a/src/formula/Prctl/Next.h +++ b/src/formula/Prctl/Next.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/abstract/Next.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -53,15 +52,15 @@ class INextModelChecker { * @see AbstractPrctlFormula */ 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::prctl::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 prctl diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h index 6859d97b1..231ced8d9 100644 --- a/src/formula/Prctl/Not.h +++ b/src/formula/Prctl/Not.h @@ -129,7 +129,7 @@ public: /*! * @returns The child node */ - const FormulaType& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -137,7 +137,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(FormulaType* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h index cbac0c655..3f1b83f36 100644 --- a/src/formula/Prctl/Or.h +++ b/src/formula/Prctl/Or.h @@ -70,7 +70,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - Or(FormulaType* left, FormulaType* right) { + Or(AbstractStateFormula* left, AbstractStateFormula* right) { this->left = left; this->right = right; } @@ -148,7 +148,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(FormulaType* newLeft) { + void setLeft(AbstractStateFormula* newLeft) { left = newLeft; } @@ -157,21 +157,21 @@ public: * * @param newRight the new right child. */ - void setRight(FormulaType* newRight) { + void setRight(AbstractStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const FormulaType& getLeft() const { + const AbstractStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const FormulaType& getRight() const { + const AbstractStateFormula& getRight() const { return *right; } diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h index 6e171a517..9cbcee34c 100644 --- a/src/formula/Prctl/ProbabilisticBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticBoundOperator.h @@ -11,6 +11,7 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" #include "utility/constants.h" +#include "src/formula/ComparisonType.h" namespace storm { namespace property { @@ -52,54 +53,39 @@ class IProbabilisticBoundOperatorModelChecker { * @see AbstractPrctlFormula */ template -class ProbabilisticBoundOperator : public storm::property::abstract::ProbabilisticBoundOperator>, - public AbstractStateFormula { +class ProbabilisticBoundOperator : public AbstractStateFormula { public: + /*! * Empty constructor */ - ProbabilisticBoundOperator() { - // 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 - } - - /*! - * - * @param comparisonRelation - * @param bound - * @param pathFormula - * @param minimumOperator - */ - ProbabilisticBoundOperator( - storm::property::ComparisonType comparisonRelation, - T bound, - AbstractPathFormula* pathFormula, - bool minimumOperator) - : storm::property::abstract::ProbabilisticBoundOperator>(comparisonRelation, bound, pathFormula, minimumOperator){ - // Intentionally left empty + ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) + : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { + // 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() { - // Intentionally left empty + if (pathFormula != nullptr) { + delete pathFormula; + } } /*! @@ -129,6 +115,101 @@ public: virtual storm::storage::BitVector check(const storm::modelchecker::prctl::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 prctl diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h deleted file mode 100644 index 5591a9555..000000000 --- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h +++ /dev/null @@ -1,115 +0,0 @@ -/* - * ProbabilisticNoBoundOperator.h - * - * Created on: 12.12.2012 - * Author: thomas - */ - -#ifndef STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_ -#define STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_ - -#include "AbstractPathFormula.h" -#include "AbstractNoBoundOperator.h" -#include "src/formula/abstract/ProbabilisticNoBoundOperator.h" - -namespace storm { -namespace property { -namespace prctl { - -/*! - * @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 DtmcPrctlModelChecker 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 AbstractPrctlFormula - */ -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::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { - return this->getPathFormula().check(modelChecker, qualitative); - } -}; - -} //namespace prctl -} //namespace property -} //namespace storm - -#endif /* STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h index d0bcdfc69..0368b4ba9 100644 --- a/src/formula/Prctl/ReachabilityReward.h +++ b/src/formula/Prctl/ReachabilityReward.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "../abstract/Eventually.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -50,14 +49,13 @@ class IReachabilityRewardModelChecker { * @see AbstractPrctlFormula */ template -class ReachabilityReward : public storm::property::abstract::Eventually>, - public AbstractPathFormula { +class ReachabilityReward : public AbstractPathFormula { public: /*! * Empty constructor */ - ReachabilityReward() { + ReachabilityReward() : child(nullptr){ // Intentionally left empty } @@ -66,8 +64,7 @@ public: * * @param child The child node */ - ReachabilityReward(AbstractStateFormula* child) : - storm::property::abstract::Eventually>(child){ + ReachabilityReward(AbstractStateFormula* child) : child(child){ // Intentionally left empty } @@ -78,7 +75,9 @@ public: * (this behaviour can be prevented by setting the subtrees to nullptr before deletion) */ virtual ~ReachabilityReward() { - // Intentionally left empty + if (child != nullptr) { + delete child; + } } /*! @@ -108,6 +107,51 @@ public: virtual std::vector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkReachabilityReward(*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 prctl diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h index 4c5cf19d3..73dea7ab3 100644 --- a/src/formula/Prctl/RewardBoundOperator.h +++ b/src/formula/Prctl/RewardBoundOperator.h @@ -10,8 +10,8 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/abstract/RewardBoundOperator.h" #include "utility/constants.h" +#include "src/formula/ComparisonType.h" namespace storm { namespace property { @@ -52,48 +52,38 @@ class IRewardBoundOperatorModelChecker { * @see AbstractPrctlFormula */ template -class RewardBoundOperator : public storm::property::abstract::RewardBoundOperator>, - public AbstractStateFormula { +class RewardBoundOperator : public AbstractStateFormula { public: /*! * Empty constructor */ - RewardBoundOperator() { + RewardBoundOperator() : 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 */ - RewardBoundOperator( - storm::property::ComparisonType comparisonRelation, - T bound, - AbstractPathFormula* pathFormula) : - storm::property::abstract::RewardBoundOperator>(comparisonRelation, bound, pathFormula) { + RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) + : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { // Intentionally left empty } - /*! - * Constructor + * Destructor * - * @param comparisonRelation - * @param bound - * @param pathFormula - * @param minimumOperator + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) */ - RewardBoundOperator( - storm::property::ComparisonType comparisonRelation, - T bound, - AbstractPathFormula* pathFormula, - bool minimumOperator) - : storm::property::abstract::RewardBoundOperator>(comparisonRelation, bound, pathFormula, minimumOperator) { - // Intentionally left empty + virtual ~RewardBoundOperator() { + if (pathFormula != nullptr) { + delete pathFormula; + } } /*! @@ -123,6 +113,101 @@ public: virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker) const override { return modelChecker.template as()->checkRewardBoundOperator(*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 = "R "; + 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 prctl diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h deleted file mode 100644 index 97a8dfeaa..000000000 --- a/src/formula/Prctl/RewardNoBoundOperator.h +++ /dev/null @@ -1,108 +0,0 @@ -/* - * RewardNoBoundOperator.h - * - * Created on: 25.12.2012 - * Author: Christian Dehnert - */ - -#ifndef STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_ -#define STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_ - -#include "AbstractNoBoundOperator.h" -#include "AbstractPathFormula.h" -#include "src/formula/abstract/RewardNoBoundOperator.h" - -namespace storm { -namespace property { -namespace prctl { - -/*! - * @brief - * Class for an abstract formula tree with a R (reward) operator without declaration of reward values - * as root. - * - * Checking a formula with this operator as root returns the reward for the reward path formula for - * 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 checkRewardNoBoundOperator method from the DtmcPrctlModelChecker 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 AbstractPrctlFormula - */ -template -class RewardNoBoundOperator: public storm::property::abstract::RewardNoBoundOperator>, - public storm::property::prctl::AbstractNoBoundOperator { -public: - /*! - * Empty constructor - */ - RewardNoBoundOperator() { - // Intentionally left empty - } - - /*! - * Constructor - * - * @param pathFormula The child node. - */ - RewardNoBoundOperator(AbstractPathFormula* pathFormula) - : storm::property::abstract::RewardNoBoundOperator>(pathFormula) { - // Intentionally left empty - } - - /*! - * Constructor - * - * @param pathFormula The child node. - */ - RewardNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) - : storm::property::abstract::RewardNoBoundOperator>(pathFormula, minimumOperator) { - // Intentionally left empty - } - - virtual AbstractNoBoundOperator* clone() const override { - RewardNoBoundOperator* result = new RewardNoBoundOperator(); - 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::prctl::AbstractModelChecker& modelChecker, bool qualitative=false) const override { - return this->getPathFormula().check(modelChecker, qualitative); - } -}; - -} //namespace prctl -} //namespace property -} //namespace storm - -#endif /* STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h index f7c87e90d..f850988fa 100644 --- a/src/formula/Prctl/SteadyStateReward.h +++ b/src/formula/Prctl/SteadyStateReward.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/abstract/SteadyStateReward.h" #include "src/formula/AbstractFormulaChecker.h" #include @@ -46,8 +45,7 @@ class ISteadyStateRewardModelChecker { * @see AbstractPrctlFormula */ template -class SteadyStateReward: public storm::property::abstract::SteadyStateReward, - public AbstractPathFormula { +class SteadyStateReward: public AbstractPathFormula { public: /*! * Empty constructor @@ -83,6 +81,25 @@ public: virtual std::vector check(const storm::modelchecker::prctl::AbstractModelChecker& modelChecker, bool qualitative) const override { return modelChecker.template as()->checkSteadyStateReward(*this, qualitative); } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const override { + return "S"; + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * As SteadyStateReward objects have no subformulas, we return true here. + * + * @param checker Formula checker object. + * @return true + */ + virtual bool validate(const AbstractFormulaChecker& checker) const override { + return true; + } }; } //namespace prctl diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h index 53fb92f6b..1bca7037b 100644 --- a/src/formula/Prctl/Until.h +++ b/src/formula/Prctl/Until.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/abstract/Until.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -54,15 +53,15 @@ class IUntilModelChecker { * @see AbstractPrctlFormula */ 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 +70,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 +81,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 +119,78 @@ public: virtual std::vector check(const storm::modelchecker::prctl::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 prctl diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h index 5862fe9c9..888721a56 100644 --- a/src/modelchecker/prctl/AbstractModelChecker.h +++ b/src/modelchecker/prctl/AbstractModelChecker.h @@ -56,7 +56,6 @@ class AbstractModelChecker : public virtual storm::property::prctl::INextModelChecker, public virtual storm::property::prctl::IBoundedUntilModelChecker, public virtual storm::property::prctl::IBoundedEventuallyModelChecker, - public virtual storm::property::prctl::INoBoundOperatorModelChecker, public virtual storm::property::prctl::IProbabilisticBoundOperatorModelChecker, public virtual storm::property::prctl::IRewardBoundOperatorModelChecker, public virtual storm::property::prctl::IReachabilityRewardModelChecker,