From 9e3ec6c403264162b1b789b38862eb6aeae0e9be Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 22 Apr 2013 11:00:17 +0200 Subject: [PATCH] Added LTL --- src/formula/Ltl.h | 22 +++++ src/formula/Ltl/AbstractLtlFormula.h | 21 ++++- src/formula/Ltl/And.h | 129 ++++++++++++++++++++++++++ src/formula/Ltl/Ap.h | 98 ++++++++++++++++++++ src/formula/Ltl/BoundedEventually.h | 125 ++++++++++++++++++++++++++ src/formula/Ltl/BoundedUntil.h | 130 +++++++++++++++++++++++++++ src/formula/Ltl/Eventually.h | 119 ++++++++++++++++++++++++ src/formula/Ltl/Globally.h | 121 +++++++++++++++++++++++++ src/formula/Ltl/Next.h | 119 ++++++++++++++++++++++++ src/formula/Ltl/Not.h | 116 ++++++++++++++++++++++++ src/formula/Ltl/Or.h | 105 ++++++++++++++++++++++ src/formula/Ltl/Until.h | 124 +++++++++++++++++++++++++ 12 files changed, 1226 insertions(+), 3 deletions(-) create mode 100644 src/formula/Ltl.h create mode 100644 src/formula/Ltl/And.h create mode 100644 src/formula/Ltl/Ap.h create mode 100644 src/formula/Ltl/BoundedEventually.h create mode 100644 src/formula/Ltl/BoundedUntil.h create mode 100644 src/formula/Ltl/Eventually.h create mode 100644 src/formula/Ltl/Globally.h create mode 100644 src/formula/Ltl/Next.h create mode 100644 src/formula/Ltl/Not.h create mode 100644 src/formula/Ltl/Or.h create mode 100644 src/formula/Ltl/Until.h diff --git a/src/formula/Ltl.h b/src/formula/Ltl.h new file mode 100644 index 000000000..e37aabeca --- /dev/null +++ b/src/formula/Ltl.h @@ -0,0 +1,22 @@ +/* + * Ltl.h + * + * Created on: 22.04.2013 + * Author: thomas + */ + +#ifndef LTL_H_ +#define LTL_H_ + +#include "Ltl/And.h" +#include "Ltl/Ap.h" +#include "Ltl/BoundedEventually.h" +#include "Ltl/BoundedUntil.h" +#include "Ltl/Eventually.h" +#include "Ltl/Globally.h" +#include "Ltl/Next.h" +#include "Ltl/Not.h" +#include "Ltl/Or.h" +#include "Ltl/Until.h" + +#endif /* LTL_H_ */ diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h index ba258a3fc..053f00d1f 100644 --- a/src/formula/Ltl/AbstractLtlFormula.h +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -5,12 +5,17 @@ * Author: thomas */ -#ifndef ABSTRACTLTLFORMULA_H_ -#define ABSTRACTLTLFORMULA_H_ +#ifndef STORM_LTL_ABSTRACTLTLFORMULA_H_ +#define STORM_LTL_ABSTRACTLTLFORMULA_H_ + +#include +#include "src/modelchecker/ForwardDeclarations.h" namespace storm { namespace formula { +namespace ltl { +template class AbstractLtlFormula { public: /** @@ -32,8 +37,18 @@ public: * @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 = 0; + + /*! + * 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 AND-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const = 0; }; +} /* namespace ltl */ } /* namespace formula */ } /* namespace storm */ -#endif /* ABSTRACTLTLFORMULA_H_ */ +#endif /* STORM_LTL_ABSTRACTLTLFORMULA_H_ */ diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h new file mode 100644 index 000000000..7f574ba05 --- /dev/null +++ b/src/formula/Ltl/And.h @@ -0,0 +1,129 @@ +/* + * And.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_LTL_AND_H_ +#define STORM_FORMULA_LTL_AND_H_ + +#include "AbstractLtlFormula.h" +#include "src/formula/abstract/And.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" +#include + +namespace storm { +namespace formula { +namespace ltl { + +template class And; + +/*! + * @brief Interface class for model checkers that support And. + * + * All model checkers that support the formula class And must inherit + * this pure virtual class. + */ +template +class IAndModelChecker { + public: + /*! + * @brief Evaluates And formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkAnd(const And& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract formula tree with AND node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * As AND is commutative, the order is \e theoretically not important, but will influence the order in which + * the model checker works. + * + * The subtrees are seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class And : public storm::formula::abstract::And>, public AbstractLtlFormula { + +public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ + And() { + //intentionally left empty + } + + /*! + * Constructor. + * Creates an AND node with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + And(AbstractLtlFormula* left, AbstractLtlFormula* right) + : storm::formula::abstract::And>(left, right) { + //intentionally left empty + } + + /*! + * Destructor. + * + * The subtrees are deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~And() { + //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 AND-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const { + And* result = new And(); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkAnd(*this); + } + +}; + +} //namespace ltl + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_LTL_AND_H_ */ diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h new file mode 100644 index 000000000..19372d771 --- /dev/null +++ b/src/formula/Ltl/Ap.h @@ -0,0 +1,98 @@ +/* + * Ap.h + * + * Created on: 22.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_LTL_AP_H_ +#define STORM_FORMULA_LTL_AP_H_ + +#include "AbstractLtlFormula.h" +#include "src/formula/abstract/Ap.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class Ap; + +/*! + * @brief Interface class for model checkers that support And. + * + * All model checkers that support the formula class And must inherit + * this pure virtual class. + */ +template +class IApModelChecker { + public: + /*! + * @brief Evaluates And formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkAp(const Ap& obj) const = 0; +}; + +template +class Ap: public storm::formula::abstract::Ap, + public storm::formula::ltl::AbstractLtlFormula { +public: + /*! + * Empty constructor + */ + Ap() { + // Intentionally left empty + } + + /*! + * Constructor + * + * Creates a new atomic proposition leaf, with the label Ap + * + * @param ap The string representing the atomic proposition + */ + Ap(std::string ap) : + storm::formula::abstract::Ap(ap) { + // Intentionally left empty + } + + /*! + * Destructor + */ + virtual ~Ap() { + // Intentionally left empty + } + + /*! + * 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::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as>.check(*this); + } + + /*! + * 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 AND-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const { + return new Ap(this->getAp()); + } +}; + +} /* namespace ltl */ +} /* namespace formula */ +} /* namespace storm */ +#endif /* STORM_FORMULA_LTL_AP_H_ */ diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h new file mode 100644 index 000000000..4cf0ab0b9 --- /dev/null +++ b/src/formula/Ltl/BoundedEventually.h @@ -0,0 +1,125 @@ +/* + * BoundedUntil.h + * + * Created on: 27.11.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_ +#define STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_ + +#include "src/formula/abstract/BoundedEventually.h" +#include "AbstractLtlFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "boost/integer/integer_mask.hpp" +#include +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class BoundedEventually; + +/*! + * @brief Interface class for model checkers that support BoundedEventually. + * + * All model checkers that support the formula class BoundedEventually must inherit + * this pure virtual class. + */ +template +class IBoundedEventuallyModelChecker { + public: + /*! + * @brief Evaluates BoundedEventually formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkBoundedEventually(const BoundedEventually& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with a BoundedEventually node as root. + * + * Has one Abstract state formulas as sub formula/tree. + * + * @par Semantics + * The formula holds iff in at most \e bound steps, formula \e child holds. + * + * The subtrees are seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class BoundedEventually : public storm::formula::abstract::BoundedEventually>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + BoundedEventually() { + //intentionally left empty + } + + /*! + * Constructor + * + * @param child The child formula subtree + * @param bound The maximal number of steps + */ + BoundedEventually(AbstractLtlFormula* child, uint_fast64_t bound) : + storm::formula::abstract::BoundedEventually>(child, bound){ + //intentionally left empty + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~BoundedEventually() { + //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 AbstractLtlFormula* clone() const { + BoundedEventually* result = new BoundedEventually(); + result->setBound(this->getBound()); + if (this->childIsSet()) { + result->setChild(this->getChild().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()->checkBoundedEventually(*this, qualitative); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h new file mode 100644 index 000000000..f7ef572f9 --- /dev/null +++ b/src/formula/Ltl/BoundedUntil.h @@ -0,0 +1,130 @@ +/* + * BoundedUntil.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ +#define STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ + +#include "src/formula/abstract/BoundedUntil.h" +#include "AbstractLtlFormula.h" +#include "boost/integer/integer_mask.hpp" +#include +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class BoundedUntil; + +/*! + * @brief Interface class for model checkers that support BoundedUntil. + * + * All model checkers that support the formula class BoundedUntil must inherit + * this pure virtual class. + */ +template +class IBoundedUntilModelChecker { + public: + /*! + * @brief Evaluates BoundedUntil formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkBoundedUntil(const BoundedUntil& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with a BoundedUntil node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * @par Semantics + * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before, + * \e left holds. + * + * The subtrees are seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class BoundedUntil : public storm::formula::abstract::BoundedUntil>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + BoundedUntil() { + //Intentionally left empty + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + * @param bound The maximal number of steps + */ + BoundedUntil(AbstractLtlFormula* left, AbstractLtlFormula* right, + uint_fast64_t bound) : + storm::formula::abstract::BoundedUntil>(left,right,bound) { + //intentionally left empty + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~BoundedUntil() { + //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 AbstractLtlFormula* clone() const { + BoundedUntil* result = new BoundedUntil(); + result->setBound(this->getBound()); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().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()->checkBoundedUntil(*this, qualitative); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h new file mode 100644 index 000000000..a9ffc21bd --- /dev/null +++ b/src/formula/Ltl/Eventually.h @@ -0,0 +1,119 @@ +/* + * Next.h + * + * Created on: 26.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_LTL_EVENTUALLY_H_ +#define STORM_FORMULA_LTL_EVENTUALLY_H_ + +#include "src/formula/abstract/Eventually.h" +#include "AbstractLtlFormula.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class Eventually; + +/*! + * @brief Interface class for model checkers that support Eventually. + * + * All model checkers that support the formula class Eventually must inherit + * this pure virtual class. + */ +template +class IEventuallyModelChecker { + public: + /*! + * @brief Evaluates Eventually formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkEventually(const Eventually& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with an Eventually node as root. + * + * Has one Abstract state formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff eventually \e child holds. + * + * The subtree is seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to nullptr before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class Eventually : public storm::formula::abstract::Eventually>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + Eventually() { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param child The child node + */ + Eventually(AbstractLtlFormula* child) + : storm::formula::abstract::Eventually>(child) { + + } + + /*! + * Constructor. + * + * Also deletes the subtree. + * (this behaviour can be prevented by setting the subtrees to nullptr before deletion) + */ + virtual ~Eventually() { + //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 Eventually-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const { + Eventually* result = new Eventually(); + if (this->childIsSet()) { + result->setChild(this->getChild().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()->checkEventually(*this, qualitative); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_EVENTUALLY_H_ */ diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h new file mode 100644 index 000000000..00a0f19dd --- /dev/null +++ b/src/formula/Ltl/Globally.h @@ -0,0 +1,121 @@ +/* + * Next.h + * + * Created on: 26.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_LTL_GLOBALLY_H_ +#define STORM_FORMULA_LTL_GLOBALLY_H_ + +#include "src/formula/abstract/Globally.h" +#include "AbstractLtlFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class Globally; + +/*! + * @brief Interface class for model checkers that support Globally. + * + * All model checkers that support the formula class Globally must inherit + * this pure virtual class. + */ +template +class IGloballyModelChecker { + public: + /*! + * @brief Evaluates Globally formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkGlobally(const Globally& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with a Globally node as root. + * + * Has one Abstract state formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff globally \e child holds. + * + * The subtree is seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to nullptr before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class Globally : public storm::formula::abstract::Globally>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + Globally() { + //intentionally left empty + } + + /*! + * Constructor + * + * @param child The child node + */ + Globally(AbstractLtlFormula* child) + : storm::formula::abstract::Globally>(child) { + //intentionally left empty + } + + /*! + * Constructor. + * + * Also deletes the subtree. + * (this behaviour can be prevented by setting the subtrees to nullptr before deletion) + */ + virtual ~Globally() { + //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 Globally-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const { + Globally* result = new Globally(); + if (this->childIsSet()) { + result->setChild(this->getChild().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()->checkGlobally(*this, qualitative); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_GLOBALLY_H_ */ diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h new file mode 100644 index 000000000..5bf50c9c2 --- /dev/null +++ b/src/formula/Ltl/Next.h @@ -0,0 +1,119 @@ +/* + * Next.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_LTL_NEXT_H_ +#define STORM_FORMULA_LTL_NEXT_H_ + +#include "AbstractLtlFormula.h" +#include "src/formula/abstract/Next.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class Next; + +/*! + * @brief Interface class for model checkers that support Next. + * + * All model checkers that support the formula class Next must inherit + * this pure virtual class. + */ +template +class INextModelChecker { + public: + /*! + * @brief Evaluates Next formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkNext(const Next& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with a Next node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * @par Semantics + * The formula holds iff in the next step, \e child holds + * + * The subtree is seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class Next : public storm::formula::abstract::Next>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + Next() { + //intentionally left empty + } + + /*! + * Constructor + * + * @param child The child node + */ + Next(AbstractLtlFormula* child) + : storm::formula::abstract::Next>(child) { + //intentionally left empty + } + + /*! + * Constructor. + * + * Also deletes the subtree. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Next() { + //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 AbstractLtlFormula* clone() const { + Next* result = new Next(); + if (this->childIsSet()) { + result->setChild(this->getChild().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()->checkNext(*this, qualitative); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_NEXT_H_ */ diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h new file mode 100644 index 000000000..aee6197a2 --- /dev/null +++ b/src/formula/Ltl/Not.h @@ -0,0 +1,116 @@ +/* + * Not.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_LTL_NOT_H_ +#define STORM_FORMULA_LTL_NOT_H_ + +#include "AbstractLtlFormula.h" +#include "src/formula/abstract/Not.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class Not; + +/*! + * @brief Interface class for model checkers that support Not. + * + * All model checkers that support the formula class Not must inherit + * this pure virtual class. + */ +template +class INotModelChecker { + public: + /*! + * @brief Evaluates Not formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkNot(const Not& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract formula tree with NOT node as root. + * + * Has one Abstract state formula as sub formula/tree. + * + * The subtree is seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class Not : public storm::formula::abstract::Not>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + Not() { + //intentionally left empty + } + + /*! + * Constructor + * @param child The child node + */ + Not(AbstractLtlFormula* child) : + storm::formula::abstract::Not>(child){ + //intentionally left empty + } + + /*! + * Destructor + * + * Also deletes the subtree + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Not() { + //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 AND-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const { + Not* result = new Not(); + if (this->childIsSet()) { + result->setChild(this->getChild().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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNot(*this); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_NOT_H_ */ diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h new file mode 100644 index 000000000..99d687c16 --- /dev/null +++ b/src/formula/Ltl/Or.h @@ -0,0 +1,105 @@ +/* + * Or.h + * + * Created on: 22.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_LTL_OR_H_ +#define STORM_FORMULA_LTL_OR_H_ + +#include "AbstractLtlFormula.h" +#include "src/formula/abstract/Or.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class And; + +/*! + * @brief Interface class for model checkers that support And. + * + * All model checkers that support the formula class And must inherit + * this pure virtual class. + */ +template +class IOrModelChecker { + public: + /*! + * @brief Evaluates And formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkOr(const And& obj) const = 0; +}; + +template +class Or: public storm::formula::abstract::Or>, + public storm::formula::ltl::AbstractLtlFormula { +public: + /*! + * Empty constructor + */ + Or() { + // Intentionally left empty + + } + + /*! + * Constructor + * Creates an OR node with the parameters as subtrees. + * + * @param left The left subformula + * @param right The right subformula + */ + Or(AbstractLtlFormula left, AbstractLtlFormula right) + : storm::formula::abstract::Or>(left, right) { + // Intentionally left empty + } + + /*! + * Destructor + */ + virtual ~Or() { + // 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 AND-object that is identical the called object. + */ + virtual AbstractLtlFormula* clone() const { + Or* result = new Or(); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkOr(*this); + } + +}; + +} /* namespace ltl */ +} /* namespace formula */ +} /* namespace storm */ +#endif /* OR_H_ */ diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h new file mode 100644 index 000000000..d3a1120d7 --- /dev/null +++ b/src/formula/Ltl/Until.h @@ -0,0 +1,124 @@ +/* + * Until.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_LTL_UNTIL_H_ +#define STORM_FORMULA_LTL_UNTIL_H_ + +#include "AbstractLtlFormula.h" +#include "src/formula/abstract/Until.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace ltl { + +template class Until; + +/*! + * @brief Interface class for model checkers that support Until. + * + * All model checkers that support the formula class Until must inherit + * this pure virtual class. + */ +template +class IUntilModelChecker { + public: + /*! + * @brief Evaluates Until formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkUntil(const Until& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with an Until node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * @par Semantics + * The formula holds iff eventually, formula \e right (the right subtree) holds, and before, + * \e left holds always. + * + * The subtrees are seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see AbstractLtlFormula + * @see AbstractFormula + */ +template +class Until : public storm::formula::abstract::Until>, + public AbstractLtlFormula { + +public: + /*! + * Empty constructor + */ + Until() { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + */ + Until(AbstractLtlFormula* left, AbstractLtlFormula* right) + : storm::formula::abstract::Until>(left, right) { + // Intentionally left empty + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Until() { + // 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 AbstractLtlFormula* clone() const { + Until* result = new Until(); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().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()->checkUntil(*this, qualitative); + } +}; + +} //namespace ltl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_LTL_UNTIL_H_ */