From a1ec7a5d549b8d4b2aa7284794e85d24dc1befc2 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 16 Apr 2013 11:56:08 +0200 Subject: [PATCH] Derived PRCTL formula classes from abstract ones --- .../{Prtl => Prctl}/AbstractPathFormula.h | 8 +- .../{Prtl => Prctl}/AbstractStateFormula.h | 8 +- src/formula/Prctl/And.h | 129 ++++++++++++ src/formula/Prctl/BoundedEventually.h | 126 +++++++++++ src/formula/Prctl/BoundedNaryUntil.h | 141 +++++++++++++ src/formula/Prctl/BoundedUntil.h | 131 ++++++++++++ src/formula/{Csl => Prctl}/CumulativeReward.h | 8 +- src/formula/Prctl/Eventually.h | 120 +++++++++++ src/formula/Prctl/Globally.h | 132 ++++++++++++ .../{Prtl => Prctl}/InstantaneousReward.h | 55 +---- src/formula/Prctl/Next.h | 120 +++++++++++ src/formula/Prctl/Not.h | 152 +++++++++++++ src/formula/Prctl/Or.h | 187 ++++++++++++++++ .../Prctl/ProbabilisticBoundOperator.h | 130 ++++++++++++ .../Prctl/ProbabilisticNoBoundOperator.h | 91 ++++++++ .../{Prtl => Prctl}/ReachabilityReward.h | 2 + .../{Prtl => Prctl}/RewardBoundOperator.h | 2 + .../{Prtl => Prctl}/RewardNoBoundOperator.h | 6 +- src/formula/Prctl/StateBoundOperator.h | 199 ++++++++++++++++++ src/formula/Prctl/StateNoBoundOperator.h | 150 +++++++++++++ .../{Prtl => Prctl}/SteadyStateReward.h | 6 +- src/formula/Prctl/Until.h | 185 ++++++++++++++++ 22 files changed, 2029 insertions(+), 59 deletions(-) rename src/formula/{Prtl => Prctl}/AbstractPathFormula.h (89%) rename src/formula/{Prtl => Prctl}/AbstractStateFormula.h (89%) create mode 100644 src/formula/Prctl/And.h create mode 100644 src/formula/Prctl/BoundedEventually.h create mode 100644 src/formula/Prctl/BoundedNaryUntil.h create mode 100644 src/formula/Prctl/BoundedUntil.h rename src/formula/{Csl => Prctl}/CumulativeReward.h (94%) create mode 100644 src/formula/Prctl/Eventually.h create mode 100644 src/formula/Prctl/Globally.h rename src/formula/{Prtl => Prctl}/InstantaneousReward.h (72%) create mode 100644 src/formula/Prctl/Next.h create mode 100644 src/formula/Prctl/Not.h create mode 100644 src/formula/Prctl/Or.h create mode 100644 src/formula/Prctl/ProbabilisticBoundOperator.h create mode 100644 src/formula/Prctl/ProbabilisticNoBoundOperator.h rename src/formula/{Prtl => Prctl}/ReachabilityReward.h (99%) rename src/formula/{Prtl => Prctl}/RewardBoundOperator.h (99%) rename src/formula/{Prtl => Prctl}/RewardNoBoundOperator.h (96%) create mode 100644 src/formula/Prctl/StateBoundOperator.h create mode 100644 src/formula/Prctl/StateNoBoundOperator.h rename src/formula/{Prtl => Prctl}/SteadyStateReward.h (97%) create mode 100644 src/formula/Prctl/Until.h diff --git a/src/formula/Prtl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h similarity index 89% rename from src/formula/Prtl/AbstractPathFormula.h rename to src/formula/Prctl/AbstractPathFormula.h index 459cbd057..9127a10c8 100644 --- a/src/formula/Prtl/AbstractPathFormula.h +++ b/src/formula/Prctl/AbstractPathFormula.h @@ -12,7 +12,7 @@ namespace storm { namespace formula { template class AbstractPathFormula; }} -#include "src/formula/AbstractFormula.h" +#include "src/formula/abstract/AbstractFormula.h" #include "src/modelchecker/ForwardDeclarations.h" #include @@ -21,6 +21,7 @@ template class AbstractPathFormula; namespace storm { namespace formula { +namespace prctl { /*! * @brief @@ -32,13 +33,13 @@ namespace formula { * clone(). */ template -class AbstractPathFormula : public virtual AbstractFormula { +class AbstractPathFormula : public virtual storm::formula::abstract::AbstractFormula { public: /*! * empty destructor */ - virtual ~AbstractPathFormula() { } + virtual ~AbstractPathFormula() = 0; /*! * Clones the called object. @@ -64,6 +65,7 @@ public: virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; }; +} //namespace prctl } //namespace formula } //namespace storm diff --git a/src/formula/Prtl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h similarity index 89% rename from src/formula/Prtl/AbstractStateFormula.h rename to src/formula/Prctl/AbstractStateFormula.h index cf15fdb30..51b59b118 100644 --- a/src/formula/Prtl/AbstractStateFormula.h +++ b/src/formula/Prctl/AbstractStateFormula.h @@ -12,12 +12,13 @@ namespace storm { namespace formula { template class AbstractStateFormula; }} -#include "src/formula/AbstractFormula.h" +#include "src/formula/abstract/AbstractFormula.h" #include "src/storage/BitVector.h" #include "src/modelchecker/ForwardDeclarations.h" namespace storm { namespace formula { +namespace prctl { /*! * @brief @@ -29,13 +30,13 @@ namespace formula { * clone(). */ template -class AbstractStateFormula : public AbstractFormula { +class AbstractStateFormula : public storm::formula::abstract::AbstractFormula { public: /*! * empty destructor */ - virtual ~AbstractStateFormula() { } + virtual ~AbstractStateFormula() = 0; /*! * Clones the called object. @@ -61,6 +62,7 @@ public: virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const = 0; // { }; +} //namespace prctl } //namespace formula } //namespace storm diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h new file mode 100644 index 000000000..84e78e669 --- /dev/null +++ b/src/formula/Prctl/And.h @@ -0,0 +1,129 @@ +/* + * And.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_PRCTL_AND_H_ +#define STORM_FORMULA_PRCTL_AND_H_ + +#include "AbstractStateFormula.h" +#include "src/formula/abstract/And.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" +#include + +namespace storm { +namespace formula { +namespace prctl { + +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 storm::storage::BitVector* 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 AbstractStateFormula + * @see AbstractFormula + */ +template +class And : public storm::formula::abstract::And>, public AbstractStateFormula { + +public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ + And() { + //intentionally left empty + } + + /*! + * Constructor. + * Creates an AND note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + And(AbstractStateFormula* left, AbstractStateFormula* 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 AbstractStateFormula* clone() const { + And* result = new And(); + if (this->left != NULL) { + result->setLeft(left->clone()); + } + if (this->right != NULL) { + 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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkAnd(*this); + } + +}; + +} //namespace prctl + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_PRCTL_AND_H_ */ diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h new file mode 100644 index 000000000..7f104ecd6 --- /dev/null +++ b/src/formula/Prctl/BoundedEventually.h @@ -0,0 +1,126 @@ +/* + * BoundedUntil.h + * + * Created on: 27.11.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_ +#define STORM_FORMULA_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" +#include "boost/integer/integer_mask.hpp" +#include +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl{ + +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 AbstractPathFormula + * @see AbstractFormula + */ +template +class BoundedEventually : public storm::formula::abstract::BoundedEventually>, + public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + BoundedEventually() { + //intentionally left empty + } + + /*! + * Constructor + * + * @param child The child formula subtree + * @param bound The maximal number of steps + */ + BoundedEventually(AbstractStateFormula* 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 AbstractPathFormula* clone() const { + BoundedEventually* result = new BoundedEventually(); + result->setBound(bound); + 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()->checkBoundedEventually(*this, qualitative); + } +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h new file mode 100644 index 000000000..64dda0452 --- /dev/null +++ b/src/formula/Prctl/BoundedNaryUntil.h @@ -0,0 +1,141 @@ +/* + * BoundedNaryUntil.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_ +#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_ + +#include "src/formula/abstract/BoundedNaryUntil.h" +#include "src/formula/Prctl/AbstractPathFormula.h" +#include "src/formula/Prctl/AbstractStateFormula.h" +#include "boost/integer/integer_mask.hpp" +#include +#include +#include +#include +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl { + + +template class BoundedNaryUntil; + +/*! + * @brief Interface class for model checkers that support BoundedNaryUntil. + * + * All model checkers that support the formula class BoundedNaryUntil must inherit + * this pure virtual class. + */ +template +class IBoundedNaryUntilModelChecker { + public: + /*! + * @brief Evaluates BoundedNaryUntil formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkBoundedNaryUntil(const BoundedNaryUntil& obj, bool qualitative) const = 0; +}; + +/*! + * @brief + * Class for a Abstract (path) formula tree with a BoundedNaryUntil node as root. + * + * Has at least two Abstract state formulas as sub formulas and an interval + * associated with all but the first sub formula. We'll call the first one + * \e left and all other one \e right. + * + * @par Semantics + * The formula holds iff \e left holds until eventually any of the \e right + * formulas holds after a number of steps contained in the interval + * associated with this formula. + * + * 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 AbstractPathFormula + * @see AbstractFormula + */ +template +class BoundedNaryUntil : public storm::formula::abstract::BoundedNaryUntil>, + public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + BoundedNaryUntil() { + + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + */ + BoundedNaryUntil(AbstractStateFormula* left, std::vector*,T,T>>* right) : + storm::formula::abstract::BoundedNaryUntil>(left, right){ + + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~BoundedNaryUntil() { + //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 BoundedNaryUntil-object that is identical the called object. + */ + virtual AbstractPathFormula* clone() const { + BoundedNaryUntil* result = new BoundedNaryUntil(); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + std::vector*,T,T>>* newright = new std::vector*,T,T>>(); + for (auto it = this->right->begin(); it != this->right->end(); ++it) { + newright->push_back(std::tuple*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it))); + } + result->setRight(newright); + } + 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()->checkBoundedNaryUntil(*this, qualitative); + } + +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */ diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h new file mode 100644 index 000000000..7ef1349ef --- /dev/null +++ b/src/formula/Prctl/BoundedUntil.h @@ -0,0 +1,131 @@ +/* + * BoundedUntil.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_ +#define STORM_FORMULA_BOUNDEDUNTIL_H_ + +#include "src/formula/abstract/BoundedUntil.h" +#include "src/formula/Prctl/AbstractPathFormula.h" +#include "src/formula/Prctl/AbstractStateFormula.h" +#include "boost/integer/integer_mask.hpp" +#include +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl { + +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 AbstractPathFormula + * @see AbstractFormula + */ +template +class BoundedUntil : public storm::formula::abstract::BoundedUntil, + public AbstractPathFormula { + +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(AbstractStateFormula* left, AbstractStateFormula* 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 AbstractPathFormula* clone() const { + BoundedUntil* result = new BoundedUntil(); + result->setBound(bound); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + 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()->checkBoundedUntil(*this, qualitative); + } +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/Csl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h similarity index 94% rename from src/formula/Csl/CumulativeReward.h rename to src/formula/Prctl/CumulativeReward.h index 5d3dfa667..ddd8242a9 100644 --- a/src/formula/Csl/CumulativeReward.h +++ b/src/formula/Prctl/CumulativeReward.h @@ -10,12 +10,13 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/abstract/CumulativeReward.h" #include "src/formula/AbstractFormulaChecker.h" #include namespace storm { - namespace formula { +namespace prctl { template class CumulativeReward; @@ -48,7 +49,8 @@ class ICumulativeRewardModelChecker { * @see AbstractFormula */ template -class CumulativeReward : public AbstractPathFormula { +class CumulativeReward : public storm::formula::abstract::CumulativeReward, + public AbstractPathFormula { public: /*! @@ -140,8 +142,8 @@ private: T bound; }; +} //namespace prctl } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_INSTANTANEOUSREWARD_H_ */ diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h new file mode 100644 index 000000000..8fd5e7200 --- /dev/null +++ b/src/formula/Prctl/Eventually.h @@ -0,0 +1,120 @@ +/* + * Next.h + * + * Created on: 26.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_EVENTUALLY_H_ +#define STORM_FORMULA_EVENTUALLY_H_ + +#include "src/formula/abstract/Eventually.h" +#include "src/formula/Prctl/AbstractPathFormula.h" +#include "src/formula/Prctl/AbstractStateFormula.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl { + +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 AbstractPathFormula + * @see AbstractFormula + */ +template +class Eventually : public storm::formula::abstract::Eventually>, + public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + Eventually() { + this->child = nullptr; + } + + /*! + * Constructor + * + * @param child The child node + */ + Eventually(AbstractStateFormula* 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 AbstractPathFormula* clone() const { + Eventually* result = new Eventually(); + if (child != nullptr) { + result->setChild(child); + } + 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 prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_EVENTUALLY_H_ */ diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h new file mode 100644 index 000000000..c4b7fb3a4 --- /dev/null +++ b/src/formula/Prctl/Globally.h @@ -0,0 +1,132 @@ +/* + * Next.h + * + * Created on: 26.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_GLOBALLY_H_ +#define STORM_FORMULA_GLOBALLY_H_ + +#include "src/formula/abstract/Globally.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl { + +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 AbstractPathFormula + * @see AbstractFormula + */ +template +class Globally : public storm::formula::abstract::Globally>, + public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + Globally() { + //intentionally left empty + } + + /*! + * Constructor + * + * @param child The child node + */ + Globally(AbstractStateFormula* 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 AbstractPathFormula* clone() const { + Next* result = new Next(); + if (child != nullptr) { + result->setChild(child); + } + 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); + } + + /*! + * @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); + } +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_GLOBALLY_H_ */ diff --git a/src/formula/Prtl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h similarity index 72% rename from src/formula/Prtl/InstantaneousReward.h rename to src/formula/Prctl/InstantaneousReward.h index c2001540f..b182a4201 100644 --- a/src/formula/Prtl/InstantaneousReward.h +++ b/src/formula/Prctl/InstantaneousReward.h @@ -10,13 +10,14 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/abstract/InstantaneousReward.h" #include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include namespace storm { - namespace formula { +namespace prctl { template class InstantaneousReward; @@ -49,14 +50,15 @@ class IInstantaneousRewardModelChecker { * @see AbstractFormula */ template -class InstantaneousReward : public AbstractPathFormula { +class InstantaneousReward : public storm::formula::abstract::InstantaneousReward, + public AbstractPathFormula { public: /*! * Empty constructor */ InstantaneousReward() { - bound = 0; + //intentionally left empty } /*! @@ -64,8 +66,9 @@ public: * * @param bound The time instance of the reward formula */ - InstantaneousReward(uint_fast64_t bound) { - this->bound = bound; + InstantaneousReward(uint_fast64_t bound) : + storm::formula::abstract::InstantaneousReward(bound) { + //intentionally left empty } /*! @@ -75,31 +78,6 @@ public: // Intentionally left empty. } - /*! - * @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; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() const { - std::string result = "I="; - result += std::to_string(bound); - return result; - } - /*! * Clones the called object. * @@ -124,25 +102,10 @@ public: virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkInstantaneousReward(*this, qualitative); } - - /*! - * @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 conforms(const AbstractFormulaChecker& checker) const { - return true; - } - -private: - uint_fast64_t bound; }; +} //namespace prctl } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_INSTANTANEOUSREWARD_H_ */ diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h new file mode 100644 index 000000000..0464291be --- /dev/null +++ b/src/formula/Prctl/Next.h @@ -0,0 +1,120 @@ +/* + * Next.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_NEXT_H_ +#define STORM_FORMULA_NEXT_H_ + +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/abstract/Next.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace prctl { + +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 AbstractPathFormula + * @see AbstractFormula + */ +template +class Next : public storm::formula::abstract::Next>, + public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + Next() { + //intentionally left empty + } + + /*! + * Constructor + * + * @param child The child node + */ + Next(AbstractStateFormula* 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 AbstractPathFormula* clone() const { + Next* result = new Next(); + if (child != NULL) { + result->setChild(child); + } + 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 prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_NEXT_H_ */ diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h new file mode 100644 index 000000000..b1d67423d --- /dev/null +++ b/src/formula/Prctl/Not.h @@ -0,0 +1,152 @@ +/* + * Not.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_NOT_H_ +#define STORM_FORMULA_NOT_H_ + +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl { + +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 storm::storage::BitVector* 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 AbstractStateFormula + * @see AbstractFormula + */ +template +class Not : public AbstractStateFormula { + +public: + /*! + * Empty constructor + */ + Not() { + this->child = NULL; + } + + /*! + * Constructor + * @param child The child node + */ + Not(AbstractStateFormula* child) { + this->child = child; + } + + /*! + * Destructor + * + * Also deletes the subtree + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Not() { + 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; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string 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 AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const { + Not* result = new Not(); + if (child != NULL) { + 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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNot(*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 prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_NOT_H_ */ diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h new file mode 100644 index 000000000..484ab8557 --- /dev/null +++ b/src/formula/Prctl/Or.h @@ -0,0 +1,187 @@ +/* + * Or.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_OR_H_ +#define STORM_FORMULA_OR_H_ + +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace prctl { + +template class Or; + +/*! + * @brief Interface class for model checkers that support Or. + * + * All model checkers that support the formula class Or must inherit + * this pure virtual class. + */ +template +class IOrModelChecker { + public: + /*! + * @brief Evaluates Or formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual storm::storage::BitVector* checkOr(const Or& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract formula tree with OR node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * As OR 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 AbstractStateFormula + * @see AbstractFormula + */ +template +class Or : public AbstractStateFormula { + +public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ + Or() { + left = NULL; + right = NULL; + } + + /*! + * Constructor. + * Creates an AND note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + Or(AbstractStateFormula* left, AbstractStateFormula* right) { + this->left = left; + this->right = right; + } + + /*! + * Destructor. + * + * The subtrees are deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Or() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * 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 = "("; + result += left->toString(); + result += " | "; + result += right->toString(); + result += ")"; + 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 AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const { + Or* result = new Or(); + if (this->left != NULL) { + result->setLeft(left->clone()); + } + if (this->right != NULL) { + 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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkOr(*this); + } + + /*! + * @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 conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->left) && checker.conforms(this->right); + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_OR_H_ */ diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h new file mode 100644 index 000000000..b0d89e707 --- /dev/null +++ b/src/formula/Prctl/ProbabilisticBoundOperator.h @@ -0,0 +1,130 @@ +/* + * ProbabilisticBoundOperator.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ + +#include "AbstractStateFormula.h" +#include "AbstractPathFormula.h" +#include "src/formula/PathBoundOperator.h" +#include "src/formula/OptimizingOperator.h" +#include "utility/ConstTemplates.h" + +namespace storm { +namespace formula { +namespace prctl { + +template class ProbabilisticBoundOperator; + +/*! + * @brief Interface class for model checkers that support ProbabilisticBoundOperator. + * + * All model checkers that support the formula class PathBoundOperator must inherit + * this pure virtual class. + */ +template +class IProbabilisticBoundOperatorModelChecker { + public: + virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * as root. + * + * Has one Abstract path formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff the probability that the path formula holds is inside the bounds + * specified in this operator + * + * 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 ProbabilisticNoBoundsOperator + * @see AbstractFormula + */ +template +class ProbabilisticBoundOperator : public PathBoundOperator { + +public: + /*! + * Empty constructor + */ + ProbabilisticBoundOperator() : PathBoundOperator + (PathBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + // Intentionally left empty + } + + + /*! + * Constructor + * + * @param comparisonRelation The relation to compare the actual value and the bound + * @param bound The bound for the probability + * @param pathFormula The child node + */ + ProbabilisticBoundOperator( + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) + : PathBoundOperator(comparisonRelation, bound, pathFormula) { + // Intentionally left empty + } + + ProbabilisticBoundOperator( + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) + : PathBoundOperator(comparisonRelation, bound, pathFormula, minimumOperator){ + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "P "; + result += PathBoundOperator::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 AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const { + ProbabilisticBoundOperator* result = new ProbabilisticBoundOperator(); + result->setComparisonOperator(this->getComparisonOperator()); + result->setBound(this->getBound()); + 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. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkProbabilisticBoundOperator(*this); + } +}; + +} //namespace formula +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h new file mode 100644 index 000000000..af9bc29d0 --- /dev/null +++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h @@ -0,0 +1,91 @@ +/* + * ProbabilisticNoBoundOperator.h + * + * Created on: 12.12.2012 + * Author: thomas + */ + +#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ + +#include "AbstractFormula.h" +#include "AbstractPathFormula.h" +#include "PathNoBoundOperator.h" + +namespace storm { +namespace formula { +namespace prctl { + +/*! + * @brief + * Class for a 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 AbstractFormula + */ +template +class ProbabilisticNoBoundOperator: public PathNoBoundOperator { +public: + /*! + * Empty constructor + */ + ProbabilisticNoBoundOperator() : PathNoBoundOperator(nullptr) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param pathFormula The child node. + */ + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) : PathNoBoundOperator(pathFormula) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param pathFormula The child node. + */ + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) : PathNoBoundOperator(pathFormula, minimumOperator) { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "P"; + result += PathNoBoundOperator::toString(); + return result; + } +}; + +} //namespace formula +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prtl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h similarity index 99% rename from src/formula/Prtl/ReachabilityReward.h rename to src/formula/Prctl/ReachabilityReward.h index f88deb30e..3289f3df9 100644 --- a/src/formula/Prtl/ReachabilityReward.h +++ b/src/formula/Prctl/ReachabilityReward.h @@ -14,6 +14,7 @@ namespace storm { namespace formula { +namespace prctl { template class ReachabilityReward; @@ -145,6 +146,7 @@ private: AbstractStateFormula* child; }; +} //namespace prctl } //namespace formula } //namespace storm diff --git a/src/formula/Prtl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h similarity index 99% rename from src/formula/Prtl/RewardBoundOperator.h rename to src/formula/Prctl/RewardBoundOperator.h index 18d715fbc..452d10685 100644 --- a/src/formula/Prtl/RewardBoundOperator.h +++ b/src/formula/Prctl/RewardBoundOperator.h @@ -15,6 +15,7 @@ namespace storm { namespace formula { +namespace prctl { template class RewardBoundOperator; @@ -118,6 +119,7 @@ public: } }; +} //namespace prctl } //namespace formula } //namespace storm diff --git a/src/formula/Prtl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h similarity index 96% rename from src/formula/Prtl/RewardNoBoundOperator.h rename to src/formula/Prctl/RewardNoBoundOperator.h index 8bb0b7f66..ed65a5f3c 100644 --- a/src/formula/Prtl/RewardNoBoundOperator.h +++ b/src/formula/Prctl/RewardNoBoundOperator.h @@ -14,6 +14,7 @@ namespace storm { namespace formula { +namespace prctl { /*! * @brief @@ -83,7 +84,8 @@ public: } }; -} /* namespace formula */ -} /* namespace storm */ +} //namespace prctl +} //namespace formula +} //namespace storm #endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/StateBoundOperator.h b/src/formula/Prctl/StateBoundOperator.h new file mode 100644 index 000000000..1b6367cfd --- /dev/null +++ b/src/formula/Prctl/StateBoundOperator.h @@ -0,0 +1,199 @@ +/* + * BoundOperator.h + * + * Created on: 27.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_ +#define STORM_FORMULA_STATEBOUNDOPERATOR_H_ + +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/AbstractModelChecker.h" +#include "src/utility/ConstTemplates.h" + +namespace storm { +namespace formula { +namespace prctl { + +template class StateBoundOperator; + +/*! + * @brief Interface class for model checkers that support StateBoundOperator. + * + * All model checkers that support the formula class StateBoundOperator must inherit + * this pure virtual class. + */ +template +class IStateBoundOperatorModelChecker { + public: + virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator& obj) const = 0; +}; + +/*! + * @brief + * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval + * as root. + * + * Has one Abstract state formula as sub formula/tree. + * + * @par Semantics + * The formula holds iff the probability that the state formula holds is inside the bounds + * specified in this operator + * + * 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 ProbabilisticNoBoundsOperator + * @see AbstractFormula + */ +template +class StateBoundOperator : public AbstractStateFormula { + +public: + enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; + + /*! + * Constructor + * + * @param comparisonOperator The relation for the bound. + * @param bound The bound for the probability + * @param stateFormula The child node + */ + StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula* stateFormula) + : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { + // Intentionally left empty + } + + /*! + * Destructor + * + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~StateBoundOperator() { + if (stateFormula != nullptr) { + delete stateFormula; + } + } + + /*! + * @returns the child node (representation of a Abstract state formula) + */ + const AbstractStateFormula& getStateFormula () const { + return *stateFormula; + } + + /*! + * Sets the child node + * + * @param stateFormula the state formula that becomes the new child node + */ + void setStateFormula(AbstractStateFormula* stateFormula) { + this->stateFormula = stateFormula; + } + + /*! + * @returns the comparison relation + */ + const ComparisonType getComparisonOperator() const { + return comparisonOperator; + } + + void setComparisonOperator(ComparisonType comparisonOperator) { + this->comparisonOperator = comparisonOperator; + } + + /*! + * @returns the bound for the measure + */ + const T& getBound() const { + return bound; + } + + /*! + * Sets the interval in which the probability that the path formula holds may lie in. + * + * @param bound The bound for the measure + */ + void setBound(T bound) { + this->bound = bound; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = " "; + switch (comparisonOperator) { + case LESS: result += "< "; break; + case LESS_EQUAL: result += "<= "; break; + case GREATER: result += "> "; break; + case GREATER_EQUAL: result += ">= "; break; + } + result += std::to_string(bound); + result += " ["; + result += stateFormula->toString(); + result += "]"; + return result; + } + + 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; + } + } + + /*! + * 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 AbstractStateFormula* 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. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkStateBoundOperator(*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->stateFormula); + } + +private: + ComparisonType comparisonOperator; + T bound; + AbstractStateFormula* stateFormula; +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/StateNoBoundOperator.h b/src/formula/Prctl/StateNoBoundOperator.h new file mode 100644 index 000000000..f18edc23e --- /dev/null +++ b/src/formula/Prctl/StateNoBoundOperator.h @@ -0,0 +1,150 @@ +/* + * StateNoBoundOperator.h + * + * Created on: 09.04.2013 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_STATENOBOUNDOPERATOR_H_ +#define STORM_FORMULA_STATENOBOUNDOPERATOR_H_ + +#include "src/formula/AbstractFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractFormulaChecker.h" + +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace prctl { + +template class StateNoBoundOperator; + +/*! + * @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 IStateNoBoundOperatorModelChecker { + 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* checkStateNoBoundOperator(const StateNoBoundOperator& obj) const = 0; +}; + + +/*! + * @brief + * Class for a Abstract formula tree with an 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 state 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 SteadyStateNoBoundOperator + * @see AbstractFormula + */ +template +class StateNoBoundOperator: public storm::formula::AbstractFormula { +public: + /*! + * Empty constructor + */ + StateNoBoundOperator() { + stateFormula = nullptr; + } + + /*! + * Constructor + */ + StateNoBoundOperator(AbstractStateFormula* stateFormula) { + this->stateFormula = stateFormula; + } + + /*! + * Destructor + * + * Deletes the subtree + */ + virtual ~StateNoBoundOperator() { + if (stateFormula != nullptr) { + delete stateFormula; + } + } + + const AbstractStateFormula& getStateFormula() const { + return *(this->stateFormula); + } + + void setStateFormula(AbstractStateFormula* stateFormula) { + this->stateFormula = stateFormula; + } + + /*! + * 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 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()->checkStateNoBoundOperator(*this); + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result; + result += " = ? ["; + result += this->getStateFormula().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 conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->stateFormula); + } + +private: + AbstractStateFormula* stateFormula; +}; + +} //namespace prctl +} //namespace formula +} //namespace storm +#endif /* STORM_FORMULA_STATENOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prtl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h similarity index 97% rename from src/formula/Prtl/SteadyStateReward.h rename to src/formula/Prctl/SteadyStateReward.h index 70db11a46..51c895b5c 100644 --- a/src/formula/Prtl/SteadyStateReward.h +++ b/src/formula/Prctl/SteadyStateReward.h @@ -15,6 +15,7 @@ namespace storm { namespace formula { +namespace prctl { template class SteadyStateReward; @@ -101,6 +102,7 @@ public: } }; -} /* namespace formula */ -} /* namespace storm */ +} //namespace prctl +} //namespace formula +} //namespace storm #endif /* STORM_FORMULA_STEADYSTATEREWARD_H_ */ diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h new file mode 100644 index 000000000..5f66e47a6 --- /dev/null +++ b/src/formula/Prctl/Until.h @@ -0,0 +1,185 @@ +/* + * Until.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_UNTIL_H_ +#define STORM_FORMULA_UNTIL_H_ + +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace prctl { + +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 AbstractPathFormula + * @see AbstractFormula + */ +template +class Until : public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + Until() { + this->left = NULL; + this->right = NULL; + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + */ + Until(AbstractStateFormula* left, AbstractStateFormula* right) { + this->left = left; + this->right = right; + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Until() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + 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 += 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 { + Until* result = new Until(); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + 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()->checkUntil(*this, qualitative); + } + + /*! + * @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 conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->left) && checker.conforms(this->right); + } + +private: + AbstractStateFormula* left; + AbstractStateFormula* right; +}; + +} //namespace prctl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_UNTIL_H_ */