From 96fa125fe4ae666b9947daef85a9557251966dd2 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Wed, 10 Apr 2013 14:04:19 +0200 Subject: [PATCH] Added time bounded operators for CSL. --- src/formula/Formulas.h | 3 + src/formula/TimeBoundedEventually.h | 133 ++++++++++++++++++++++ src/formula/TimeBoundedOperator.h | 101 +++++++++++++++++ src/formula/TimeBoundedUntil.h | 168 ++++++++++++++++++++++++++++ 4 files changed, 405 insertions(+) create mode 100644 src/formula/TimeBoundedEventually.h create mode 100644 src/formula/TimeBoundedOperator.h create mode 100644 src/formula/TimeBoundedUntil.h diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index d2b4e98da..475bce23d 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -35,6 +35,9 @@ #include "SteadyStateNoBoundOperator.h" #include "SteadyStateBoundOperator.h" +#include "TimeBoundedUntil.h" +#include "TimeBoundedEventually.h" + #include "AbstractFormula.h" #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" diff --git a/src/formula/TimeBoundedEventually.h b/src/formula/TimeBoundedEventually.h new file mode 100644 index 000000000..01c67d00c --- /dev/null +++ b/src/formula/TimeBoundedEventually.h @@ -0,0 +1,133 @@ +/* + * TimeBoundedEventually.h + * + * Created on: 10.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ +#define STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ + +#include "TimeBoundedOperator.h" +#include "AbstractStateFormula.h" + +namespace storm { +namespace formula { + +template class TimeBoundedEventually; + +/*! + * @brief Interface class for model checkers that support TimeBoundedEventually. + * + * All model checkers that support the formula class BoundedEventually must inherit + * this pure virtual class. + */ +template +class ITimeBoundedEventuallyModelChecker { + public: + /*! + * @brief Evaluates TimeBoundedUntil formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkTimeBoundedEventually(const TimeBoundedEventually& obj, bool qualitative) const = 0; +}; + + +template +class TimeBoundedEventually: public storm::formula::TimeBoundedOperator { +public: + /** + * Simple constructor: Only sets the bounds + * + * @param lowerBound + * @param upperBound + */ + TimeBoundedEventually(T lowerBound, T upperBound) : TimeBoundedOperator(lowerBound, upperBound) { + child = nullptr; + } + + TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula* child) : + TimeBoundedOperator(lowerBound, upperBound) { + this->child = child; + } + + virtual ~TimeBoundedEventually() { + if (child != nullptr) { + 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; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "F"; + result += TimeBoundedOperator::toString(); + result += " "; + result += child->toString(); + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual AbstractPathFormula* clone() const { + TimeBoundedEventually* result = new TimeBoundedEventually(this->getLowerBound(), this->getUpperBound()); + if (child != nullptr) { + result->setChild(child->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::AbstractModelChecker& modelChecker, bool qualitative) const { + 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 conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->child); + } + +private: + AbstractStateFormula* child; +}; + +} /* namespace formula */ +} /* namespace storm */ +#endif /* STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ */ diff --git a/src/formula/TimeBoundedOperator.h b/src/formula/TimeBoundedOperator.h new file mode 100644 index 000000000..b14df9cbb --- /dev/null +++ b/src/formula/TimeBoundedOperator.h @@ -0,0 +1,101 @@ +/* + * TimeBoundedOperator.h + * + * Created on: 10.04.2013 + * Author: thomas + */ + +#ifndef TIMEBOUNDEDOPERATOR_H_ +#define TIMEBOUNDEDOPERATOR_H_ + +#include "AbstractPathFormula.h" +#include "exceptions/InvalidArgumentException.h" + +namespace storm { +namespace formula { + +/*! + * @brief + * Class for a Abstract formula tree with a operator node as root that uses a time interval + * (with upper and lower bound) + * + * This class does not provide support for sub formulas; this has to be done in concretizations of this abstract class. + * + * + * @see AbstractStateFormula + * @see AbstractPathFormula + * @see AbstractFormula + */ +template +class TimeBoundedOperator: public storm::formula::AbstractPathFormula { +public: + /** + * Constructor + * + * @param lowerBound The lower bound + * @param upperBound The upper bound + * @throw InvalidArgumentException if the lower bound is larger than the upper bound. + */ + TimeBoundedOperator(T lowerBound, T upperBound) { + setInterval(lowerBound, upperBound); + } + + /** + * Destructor + */ + virtual ~TimeBoundedOperator() { + // Intentionally left empty + } + + /** + * 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; + } + + + /*! + * @returns a string representation of the Interval of the formula + * May be used in subclasses to simplify string output. + */ + virtual std::string toString() const { + std::string result = "["; + result += std::to_string(lowerBound); + result += ";"; + result += "]"; + return result; + } + +private: + T lowerBound, upperBound; +}; + +} /* namespace formula */ +} /* namespace storm */ +#endif /* TIMEBOUNDEDOPERATOR_H_ */ diff --git a/src/formula/TimeBoundedUntil.h b/src/formula/TimeBoundedUntil.h new file mode 100644 index 000000000..a0cceac78 --- /dev/null +++ b/src/formula/TimeBoundedUntil.h @@ -0,0 +1,168 @@ +/* + * TimeBoundedUntil.h + * + * Created on: 10.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ +#define STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ + +#include "TimeBoundedOperator.h" + +namespace storm { +namespace formula { + +template class TimeBoundedUntil; + +/*! + * @brief Interface class for model checkers that support TimeBoundedUntil. + * + * All model checkers that support the formula class BoundedEventually must inherit + * this pure virtual class. + */ +template +class ITimeBoundedUntilModelChecker { + public: + /*! + * @brief Evaluates TimeBoundedUntil formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkTimeBoundedUntil(const TimeBoundedUntil& obj, bool qualitative) const = 0; +}; + +template +class TimeBoundedUntil: public storm::formula::TimeBoundedOperator { +public: + /** + * Constructor providing bounds only; + * Sub formulas are set to null. + * + * @param lowerBound + * @param upperBound + */ + TimeBoundedUntil(T lowerBound, T upperBound) : + TimeBoundedOperator(lowerBound, upperBound) { + this->left = nullptr; + this->right = nullptr; + } + + + /** + * Full constructor + * @param lowerBound + * @param upperBound + * @param left + * @param right + */ + TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula* left, AbstractStateFormula* right) : + TimeBoundedOperator(lowerBound, upperBound) { + this->left = left; + this->right = right; + } + + virtual ~TimeBoundedUntil() { + if (left != nullptr) { + delete left; + } + if (right != nullptr) { + delete 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; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = left->toString(); + result += " U"; + result += TimeBoundedOperator::toString(); + result += " "; + result += right->toString(); + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual AbstractPathFormula* clone() const { + TimeBoundedUntil* result = new TimeBoundedUntil(this->getLowerBound(), this->getUpperBound()); + if (left != nullptr) { + result->setLeft(left->clone()); + } + if (right != nullptr) { + result->setRight(right->clone()); + } + return result; + } + + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { + 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 conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->left) && checker.conforms(this->right); + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; +}; + +} /* namespace formula */ +} /* namespace storm */ +#endif /* STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ */