diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index f7630a113..980c3ca34 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -34,6 +34,7 @@ #include "ReachabilityReward.h" #include "RewardBoundOperator.h" #include "RewardNoBoundOperator.h" +#include "SteadyStateOperator.h" #include "modelchecker/DtmcPrctlModelChecker.h" diff --git a/src/formula/StateBoundOperator.h b/src/formula/StateBoundOperator.h index 05c213c07..9cfcfb862 100644 --- a/src/formula/StateBoundOperator.h +++ b/src/formula/StateBoundOperator.h @@ -11,7 +11,7 @@ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractFormulaChecker.h" -#include "src/modelChecker/AbstractModelChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" #include "src/utility/ConstTemplates.h" namespace storm { diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateOperator.h index 0c0543016..bce02ff5c 100644 --- a/src/formula/SteadyStateOperator.h +++ b/src/formula/SteadyStateOperator.h @@ -8,9 +8,9 @@ #ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_ #define STORM_FORMULA_STEADYSTATEOPERATOR_H_ -#include "AbstractPathFormula.h" -#include "AbstractStateFormula.h" -#include "BoundOperator.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/StateBoundOperator.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -53,14 +53,14 @@ class ISteadyStateOperatorModelChecker { * @see AbstractFormula */ template -class SteadyStateOperator : public BoundOperator { +class SteadyStateOperator : public StateBoundOperator { public: /*! * Empty constructor */ - SteadyStateOperator() : BoundOperator - (BoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + SteadyStateOperator() : StateBoundOperator + (StateBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -70,35 +70,8 @@ public: * @param child The child node */ SteadyStateOperator( - BoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* child) { - this->child = child; - } - - /*! - * Constructor. - * - * Also deletes the subtree. - * (this behaviour can be prevented by setting the subtrees to NULL before deletion) - */ - virtual ~SteadyStateOperator() { - if (child != NULL) { - delete 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; + typename StateBoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : + StateBoundOperator(comparisonRelation, bound, stateFormula) { } /*! @@ -107,7 +80,7 @@ public: virtual std::string toString() const { std::string result = "("; result += " S "; - result += child->toString(); + result += StateBoundOperator::toString(); result += ")"; return result; } @@ -119,11 +92,9 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual AbstractPathFormula* clone() const { + virtual AbstractStateFormula* clone() const { SteadyStateOperator* result = new SteadyStateOperator(); - if (child != NULL) { - result->setChild(child); - } + result->setStateFormula(this->getStateFormula().clone()); return result; } @@ -140,22 +111,9 @@ public: return modelChecker.template as()->checkSteadyStateOperator(*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 conforms(const AbstractFormulaChecker& checker) const { - return checker.conforms(this->child); - } - -private: - AbstractStateFormula* child; }; } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */