diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h new file mode 100644 index 000000000..42ba7bc02 --- /dev/null +++ b/src/formula/AbstractFormula.h @@ -0,0 +1,73 @@ +/* + * Abstractformula.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_ +#define STORM_FORMULA_ABSTRACTFORMULA_H_ + +#include + +namespace storm { namespace formula { +template class AbstractFormula; +}} + +#include "src/modelChecker/AbstractModelChecker.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { + + +//abstract +/*! + * @brief Abstract base class for Abstract formulas in general. + * + * @attention This class is abstract. + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes + * AbstractPathFormula and AbstractStateFormula offer the method clone(). + * + * This is the base class for every formula class in every logic. + */ +template +class AbstractFormula { + +public: + /*! + * Virtual destructor. + */ + virtual ~AbstractFormula() { } + + /*! + * @brief Return string representation of this formula. + * + * @note very subclass must implement this method. + * + * @returns a string representation of the formula + */ + virtual std::string toString() const = 0; + + /*! + * @brief Checks if all subtrees are valid in some logic. + * + * @note Every subclass must implement this method. + * + * This method is given a checker object that knows which formula + * classes are allowed within the logic the checker represents. Every + * subclass is supposed to call checker.conforms() for all child + * formulas and return true if and only if all those calls returned + * true. + * + * @param checker Checker object. + * @return true iff all subtrees are valid. + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const = 0; +}; + +} // namespace formula +} // namespace storm + +#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */ diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h new file mode 100644 index 000000000..6e74c48a4 --- /dev/null +++ b/src/formula/AbstractFormulaChecker.h @@ -0,0 +1,56 @@ +#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_ +#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_ + +#include "src/formula/AbstractFormula.h" + +namespace storm { +namespace formula { + +/*! + * @brief Base class for all formula checkers. + * + * A formula checker is used to check if a given formula is valid in some + * logic. Hence, this pure virtual base class should be subclassed for + * every logic we support. + * + * Every subclass must implement conforms(). It gets a pointer to an + * AbstractFormula object and should return if the subtree represented by + * this formula is valid in the logic. + * + * Usually, this will be implemented like this: + * @code + * if ( + * dynamic_cast*>(formula) || + * dynamic_cast*>(formula) || + * dynamic_cast*>(formula) + * ) { + * return formula->conforms(*this); + * } else return false; + * @endcode + * + * Every formula class implements a conforms() method itself which calls + * conforms() on the given checker for every child in the formula tree. + * + * If the formula structure is not an actual tree, but an directed acyclic + * graph, the shared subtrees will be checked twice. If we have directed + * cycles, we will have infinite recursions. + */ +template +class AbstractFormulaChecker { + public: + /*! + * @brief Checks if the given formula is valid in some logic. + * + * Every subclass must implement this method and check, if the + * formula object is valid in the logic of the subclass. + * + * @param formula A pointer to some formula object. + * @return true iff the formula is valid. + */ + virtual bool conforms(const AbstractFormula* formula) const = 0; +}; + +} // namespace formula +} // namespace storm + +#endif \ No newline at end of file diff --git a/src/formula/PctlPathFormula.h b/src/formula/AbstractPathFormula.h similarity index 64% rename from src/formula/PctlPathFormula.h rename to src/formula/AbstractPathFormula.h index f929c642a..4337cbe19 100644 --- a/src/formula/PctlPathFormula.h +++ b/src/formula/AbstractPathFormula.h @@ -1,24 +1,30 @@ /* - * PctlPathFormula.h + * AbstractPathFormula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_PCTLPATHFORMULA_H_ -#define STORM_FORMULA_PCTLPATHFORMULA_H_ +#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_ +#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_ -#include "PctlFormula.h" -#include "modelChecker/DtmcPrctlModelChecker.h" +namespace storm { namespace formula { +template class AbstractPathFormula; +}} + +#include "src/formula/AbstractFormula.h" + +#include "modelChecker/AbstractModelChecker.h" #include +#include +#include namespace storm { - namespace formula { /*! * @brief - * Abstract base class for PCTL path formulas. + * Abstract base class for Abstract path formulas. * * @attention This class is abstract. * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so @@ -26,13 +32,13 @@ namespace formula { * clone(). */ template -class PctlPathFormula : public PctlFormula { +class AbstractPathFormula : public virtual AbstractFormula { public: /*! * empty destructor */ - virtual ~PctlPathFormula() { } + virtual ~AbstractPathFormula() { } /*! * Clones the called object. @@ -42,7 +48,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PctlPathFormula* clone() const = 0; + virtual AbstractPathFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -55,11 +61,10 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; + virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const = 0; }; } //namespace formula - } //namespace storm -#endif /* STORM_FORMULA_PCTLPATHFORMULA_H_ */ +#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */ diff --git a/src/formula/PctlStateFormula.h b/src/formula/AbstractStateFormula.h similarity index 67% rename from src/formula/PctlStateFormula.h rename to src/formula/AbstractStateFormula.h index bfd035e4d..9309bf610 100644 --- a/src/formula/PctlStateFormula.h +++ b/src/formula/AbstractStateFormula.h @@ -1,24 +1,27 @@ /* - * PctlStateFormula.h + * AbstractStateFormula.h * * Created on: 19.10.2012 * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_PCTLSTATEFORMULA_H_ -#define STORM_FORMULA_PCTLSTATEFORMULA_H_ +#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_ +#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_ -#include "PctlFormula.h" -#include "storage/BitVector.h" -#include "modelChecker/DtmcPrctlModelChecker.h" +namespace storm { namespace formula { +template class AbstractStateFormula; +}} -namespace storm { +#include "AbstractFormula.h" +#include "src/storage/BitVector.h" +#include "src/modelChecker/AbstractModelChecker.h" +namespace storm { namespace formula { /*! * @brief - * Abstract base class for PCTL state formulas. + * Abstract base class for Abstract state formulas. * * @attention This class is abstract. * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so @@ -26,13 +29,13 @@ namespace formula { * clone(). */ template -class PctlStateFormula : public PctlFormula { +class AbstractStateFormula : public AbstractFormula { public: /*! * empty destructor */ - virtual ~PctlStateFormula() { } + virtual ~AbstractStateFormula() { } /*! * Clones the called object. @@ -42,7 +45,7 @@ public: * @note This function is not implemented in this class. * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const = 0; + virtual AbstractStateFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -55,12 +58,11 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; + virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const = 0; // { }; } //namespace formula - } //namespace storm -#endif /* STORM_FORMULA_PCTLSTATEFORMULA_H_ */ +#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */ diff --git a/src/formula/And.h b/src/formula/And.h index d166fd7c5..d8078cd15 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -8,18 +8,39 @@ #ifndef STORM_FORMULA_AND_H_ #define STORM_FORMULA_AND_H_ -#include "PctlStateFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelChecker/AbstractModelChecker.h" #include namespace storm { - namespace formula { +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 PCTL formula tree with AND node as root. + * Class for a Abstract formula tree with AND node as root. * - * Has two PCTL state formulas as sub formulas/trees. + * 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. @@ -27,11 +48,11 @@ namespace 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 PctlStateFormula - * @see PctlFormula + * @see AbstractStateFormula + * @see AbstractFormula */ template -class And : public PctlStateFormula { +class And : public AbstractStateFormula { public: /*! @@ -50,7 +71,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - And(PctlStateFormula* left, PctlStateFormula* right) { + And(AbstractStateFormula* left, AbstractStateFormula* right) { this->left = left; this->right = right; } @@ -75,7 +96,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PctlStateFormula* newLeft) { + void setLeft(AbstractStateFormula* newLeft) { left = newLeft; } @@ -84,21 +105,21 @@ public: * * @param newRight the new right child. */ - void setRight(PctlStateFormula* newRight) { + void setRight(AbstractStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PctlStateFormula& getLeft() const { + const AbstractStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PctlStateFormula& getRight() const { + const AbstractStateFormula& getRight() const { return *right; } @@ -121,7 +142,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { + virtual AbstractStateFormula* clone() const { And* result = new And(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -141,13 +162,23 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkAnd(*this); + virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkAnd(*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: - PctlStateFormula* left; - PctlStateFormula* right; + AbstractStateFormula* left; + AbstractStateFormula* right; }; } //namespace formula diff --git a/src/formula/Ap.h b/src/formula/Ap.h index e479d0c61..ba5c13287 100644 --- a/src/formula/Ap.h +++ b/src/formula/Ap.h @@ -8,23 +8,44 @@ #ifndef STORM_FORMULA_AP_H_ #define STORM_FORMULA_AP_H_ -#include "PctlStateFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelChecker/AbstractModelChecker.h" namespace storm { - namespace formula { +template class Ap; + +/*! + * @brief Interface class for model checkers that support Ap. + * + * All model checkers that support the formula class Ap must inherit + * this pure virtual class. + */ +template +class IApModelChecker { + public: + /*! + * @brief Evaluates Ap formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual storm::storage::BitVector* checkAp(const Ap& obj) const = 0; +}; + /*! * @brief - * Class for a PCTL formula tree with atomic proposition as root. + * Class for a Abstract formula tree with atomic proposition as root. * * This class represents the leaves in the formula tree. * - * @see PctlStateFormula - * @see PctlFormula + * @see AbstractStateFormula + * @see AbstractFormula */ template -class Ap : public PctlStateFormula { +class Ap : public AbstractStateFormula { public: /*! @@ -64,7 +85,7 @@ public: * * @returns a new Ap-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { + virtual AbstractStateFormula* clone() const { return new Ap(ap); } @@ -77,8 +98,20 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkAp(*this); + virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkAp(*this); + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * As atomic propositions have no subformulas, we return true here. + * + * @param checker Formula checker object. + * @return true + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return true; } private: diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h index 0d0abedbd..cb57f9edc 100644 --- a/src/formula/BoundOperator.h +++ b/src/formula/BoundOperator.h @@ -8,20 +8,36 @@ #ifndef STORM_FORMULA_BOUNDOPERATOR_H_ #define STORM_FORMULA_BOUNDOPERATOR_H_ -#include "PctlStateFormula.h" -#include "PctlPathFormula.h" -#include "utility/ConstTemplates.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 { +template class BoundOperator; + +/*! + * @brief Interface class for model checkers that support BoundOperator. + * + * All model checkers that support the formula class BoundOperator must inherit + * this pure virtual class. + */ +template +class IBoundOperatorModelChecker { + public: + virtual storm::storage::BitVector* checkBoundOperator(const BoundOperator& obj) const = 0; +}; + /*! * @brief - * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval + * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * - * Has one PCTL path formula as sub formula/tree. + * 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 @@ -31,14 +47,14 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PctlStateFormula - * @see PctlPathFormula + * @see AbstractStateFormula + * @see AbstractPathFormula * @see ProbabilisticOperator * @see ProbabilisticNoBoundsOperator - * @see PctlFormula + * @see AbstractFormula */ template -class BoundOperator : public PctlStateFormula { +class BoundOperator : public AbstractStateFormula { public: enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; @@ -50,7 +66,7 @@ public: * @param upperBound The upper bound for the probability * @param pathFormula The child node */ - BoundOperator(ComparisonType comparisonOperator, T bound, PctlPathFormula* pathFormula) + BoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { // Intentionally left empty } @@ -68,9 +84,9 @@ public: } /*! - * @returns the child node (representation of a PCTL path formula) + * @returns the child node (representation of a Abstract path formula) */ - const PctlPathFormula& getPathFormula () const { + const AbstractPathFormula& getPathFormula () const { return *pathFormula; } @@ -79,7 +95,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PctlPathFormula* pathFormula) { + void setPathFormula(AbstractPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -134,7 +150,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const = 0; + virtual AbstractStateFormula* clone() const = 0; /*! * Calls the model checker to check this formula. @@ -145,14 +161,24 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkBoundOperator(*this); + virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkBoundOperator(*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->pathFormula); + } private: ComparisonType comparisonOperator; T bound; - PctlPathFormula* pathFormula; + AbstractPathFormula* pathFormula; }; } //namespace formula diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h index 0a66f6b83..4be075840 100644 --- a/src/formula/BoundedEventually.h +++ b/src/formula/BoundedEventually.h @@ -8,20 +8,42 @@ #ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_ #define STORM_FORMULA_BOUNDEDEVENTUALLY_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include +#include "src/modelChecker/AbstractModelChecker.h" namespace storm { namespace formula { +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) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with a BoundedEventually node as root. + * Class for a Abstract (path) formula tree with a BoundedEventually node as root. * - * Has one PCTL state formulas as sub formula/tree. + * 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. @@ -29,11 +51,11 @@ namespace 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class BoundedEventually : public PctlPathFormula { +class BoundedEventually : public AbstractPathFormula { public: /*! @@ -50,7 +72,7 @@ public: * @param child The child formula subtree * @param bound The maximal number of steps */ - BoundedEventually(PctlStateFormula* child, uint_fast64_t bound) { + BoundedEventually(AbstractStateFormula* child, uint_fast64_t bound) { this->child = child; this->bound = bound; } @@ -70,7 +92,7 @@ public: /*! * @returns the child node */ - const PctlStateFormula& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -78,7 +100,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PctlStateFormula* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } @@ -116,7 +138,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { BoundedEventually* result = new BoundedEventually(); result->setBound(bound); if (child != nullptr) { @@ -135,12 +157,22 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkBoundedEventually(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkBoundedEventually(*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: - PctlStateFormula* child; + AbstractStateFormula* child; uint_fast64_t bound; }; diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h new file mode 100644 index 000000000..c42dab12b --- /dev/null +++ b/src/formula/BoundedNaryUntil.h @@ -0,0 +1,211 @@ +/* + * BoundedNaryUntil.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_ +#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_ + +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/modelChecker/AbstractModelChecker.h" +#include "boost/integer/integer_mask.hpp" +#include +#include +#include +#include +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { + +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) 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 AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + BoundedNaryUntil() { + this->left = NULL; + this->right = new std::vector*,T,T>>(); + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + * @param bound The maximal number of steps + */ + BoundedNaryUntil(AbstractStateFormula* left, std::vector*,T,T>>* 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 ~BoundedNaryUntil() { + 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; + } + + void setRight(std::vector*,T,T>>* newRight) { + right = newRight; + } + + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void addRight(AbstractStateFormula* newRight, T upperBound, T lowerBound) { + this->right->push_back(std::tuple*,T,T>(newRight, upperBound, lowerBound)); + } + + /*! + * @returns a pointer to the left child node + */ + const AbstractStateFormula& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child nodes. + */ + const std::vector*,T,T>>& getRight() const { + return *right; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::stringstream result; + result << "( " << left->toString(); + for (auto it = this->right->begin(); it != this->right->end(); ++it) { + result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString(); + } + result << ")"; + return result.str(); + } + + /*! + * 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) const { + return modelChecker.template as()->checkBoundedNaryUntil(*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 { + bool res = checker.conforms(this->left); + for (auto it = this->right->begin(); it != this->right->end(); ++it) { + res &= checker.conforms(std::get<0>(*it)); + } + return res; + } + +private: + AbstractStateFormula* left; + std::vector*,T,T>>* right; +}; + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */ diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 675138e27..e00acac74 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -8,20 +8,41 @@ #ifndef STORM_FORMULA_BOUNDEDUNTIL_H_ #define STORM_FORMULA_BOUNDEDUNTIL_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/modelChecker/AbstractModelChecker.h" #include "boost/integer/integer_mask.hpp" #include +#include "src/formula/AbstractFormulaChecker.h" namespace storm { - namespace formula { +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) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with a BoundedUntil node as root. + * Class for a Abstract (path) formula tree with a BoundedUntil node as root. * - * Has two PCTL state formulas as sub formulas/trees. + * 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, @@ -30,11 +51,11 @@ namespace 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class BoundedUntil : public PctlPathFormula { +class BoundedUntil : public AbstractPathFormula { public: /*! @@ -53,7 +74,7 @@ public: * @param right The left formula subtree * @param bound The maximal number of steps */ - BoundedUntil(PctlStateFormula* left, PctlStateFormula* right, + BoundedUntil(AbstractStateFormula* left, AbstractStateFormula* right, uint_fast64_t bound) { this->left = left; this->right = right; @@ -80,7 +101,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PctlStateFormula* newLeft) { + void setLeft(AbstractStateFormula* newLeft) { left = newLeft; } @@ -89,21 +110,21 @@ public: * * @param newRight the new right child. */ - void setRight(PctlStateFormula* newRight) { + void setRight(AbstractStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PctlStateFormula& getLeft() const { + const AbstractStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PctlStateFormula& getRight() const { + const AbstractStateFormula& getRight() const { return *right; } @@ -144,7 +165,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { BoundedUntil* result = new BoundedUntil(); result->setBound(bound); if (left != NULL) { @@ -166,13 +187,23 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkBoundedUntil(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkBoundedUntil(*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: - PctlStateFormula* left; - PctlStateFormula* right; + AbstractStateFormula* left; + AbstractStateFormula* right; uint_fast64_t bound; }; diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h index cbbf1e18b..e89bcfbaf 100644 --- a/src/formula/CumulativeReward.h +++ b/src/formula/CumulativeReward.h @@ -8,8 +8,9 @@ #ifndef STORM_FORMULA_CUMULATIVEREWARD_H_ #define STORM_FORMULA_CUMULATIVEREWARD_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include @@ -17,18 +18,38 @@ namespace storm { namespace formula { +template class CumulativeReward; + +/*! + * @brief Interface class for model checkers that support CumulativeReward. + * + * All model checkers that support the formula class CumulativeReward must inherit + * this pure virtual class. + */ +template +class ICumulativeRewardModelChecker { + public: + /*! + * @brief Evaluates CumulativeReward formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkCumulativeReward(const CumulativeReward& obj) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with a Cumulative Reward node as root. + * Class for a Abstract (path) formula tree with a Cumulative Reward node as root. * * 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class CumulativeReward : public PctlPathFormula { +class CumulativeReward : public AbstractPathFormula { public: /*! @@ -84,9 +105,9 @@ public: * * 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. + * @returns a new CumulativeReward-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { return new CumulativeReward(bound); } @@ -100,8 +121,20 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkCumulativeReward(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkCumulativeReward(*this); + } + + /*! + * @brief Checks if all subtrees conform to some logic. + * + * As CumulativeReward objects have no subformulas, we return true here. + * + * @param checker Formula checker object. + * @return true + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return true; } private: diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h index 1a781fbb7..4b2ca1ba3 100644 --- a/src/formula/Eventually.h +++ b/src/formula/Eventually.h @@ -8,18 +8,39 @@ #ifndef STORM_FORMULA_EVENTUALLY_H_ #define STORM_FORMULA_EVENTUALLY_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/modelChecker/AbstractModelChecker.h" namespace storm { namespace formula { +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) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with an Eventually node as root. + * Class for a Abstract (path) formula tree with an Eventually node as root. * - * Has one PCTL state formula as sub formula/tree. + * Has one Abstract state formula as sub formula/tree. * * @par Semantics * The formula holds iff eventually \e child holds. @@ -27,11 +48,11 @@ namespace formula { * 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class Eventually : public PctlPathFormula { +class Eventually : public AbstractPathFormula { public: /*! @@ -46,7 +67,7 @@ public: * * @param child The child node */ - Eventually(PctlStateFormula* child) { + Eventually(AbstractStateFormula* child) { this->child = child; } @@ -65,7 +86,7 @@ public: /*! * @returns the child node */ - const PctlStateFormula& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -73,7 +94,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PctlStateFormula* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } @@ -91,9 +112,9 @@ public: * * 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. + * @returns a new Eventually-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { Eventually* result = new Eventually(); if (child != nullptr) { result->setChild(child); @@ -110,12 +131,22 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkEventually(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkEventually(*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: - PctlStateFormula* child; + AbstractStateFormula* child; }; } //namespace formula diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 70ed03c75..1a750f674 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -8,15 +8,17 @@ #ifndef STORM_FORMULA_FORMULAS_H_ #define STORM_FORMULA_FORMULAS_H_ +#include "AbstractFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" + #include "And.h" #include "Ap.h" #include "BoundedUntil.h" +#include "BoundedNaryUntil.h" #include "Next.h" #include "Not.h" #include "Or.h" -#include "PctlFormula.h" -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" #include "ProbabilisticNoBoundOperator.h" #include "ProbabilisticBoundOperator.h" #include "Until.h" diff --git a/src/formula/Globally.h b/src/formula/Globally.h index 02a18b884..e42837091 100644 --- a/src/formula/Globally.h +++ b/src/formula/Globally.h @@ -8,18 +8,39 @@ #ifndef STORM_FORMULA_GLOBALLY_H_ #define STORM_FORMULA_GLOBALLY_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace formula { +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) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with a Globally node as root. + * Class for a Abstract (path) formula tree with a Globally node as root. * - * Has one PCTL state formula as sub formula/tree. + * Has one Abstract state formula as sub formula/tree. * * @par Semantics * The formula holds iff globally \e child holds. @@ -27,11 +48,11 @@ namespace formula { * 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class Globally : public PctlPathFormula { +class Globally : public AbstractPathFormula { public: /*! @@ -46,7 +67,7 @@ public: * * @param child The child node */ - Globally(PctlStateFormula* child) { + Globally(AbstractStateFormula* child) { this->child = child; } @@ -65,7 +86,7 @@ public: /*! * @returns the child node */ - const PctlStateFormula& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -73,7 +94,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PctlStateFormula* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } @@ -91,9 +112,9 @@ public: * * 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. + * @returns a new Globally-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { Next* result = new Next(); if (child != nullptr) { result->setChild(child); @@ -110,12 +131,22 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkGlobally(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkGlobally(*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: - PctlStateFormula* child; + AbstractStateFormula* child; }; } //namespace formula diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h index d6067d344..8f55b2c7c 100644 --- a/src/formula/InstantaneousReward.h +++ b/src/formula/InstantaneousReward.h @@ -8,8 +8,9 @@ #ifndef STORM_FORMULA_INSTANTANEOUSREWARD_H_ #define STORM_FORMULA_INSTANTANEOUSREWARD_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include @@ -17,18 +18,38 @@ namespace storm { namespace formula { +template class InstantaneousReward; + +/*! + * @brief Interface class for model checkers that support InstantaneousReward. + * + * All model checkers that support the formula class InstantaneousReward must inherit + * this pure virtual class. + */ +template +class IInstantaneousRewardModelChecker { + public: + /*! + * @brief Evaluates InstantaneousReward formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkInstantaneousReward(const InstantaneousReward& obj) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with a Instantaneous Reward node as root. + * Class for a Abstract (path) formula tree with a Instantaneous Reward node as root. * * 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class InstantaneousReward : public PctlPathFormula { +class InstantaneousReward : public AbstractPathFormula { public: /*! @@ -84,9 +105,9 @@ public: * * 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. + * @returns a new InstantaneousReward-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { return new InstantaneousReward(bound); } @@ -100,8 +121,20 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkInstantaneousReward(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkInstantaneousReward(*this); + } + + /*! + * @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: diff --git a/src/formula/Next.h b/src/formula/Next.h index 7b8214757..a91a39ce1 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -8,18 +8,39 @@ #ifndef STORM_FORMULA_NEXT_H_ #define STORM_FORMULA_NEXT_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace formula { +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) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with a Next node as root. + * Class for a Abstract (path) formula tree with a Next node as root. * - * Has two PCTL state formulas as sub formulas/trees. + * Has two Abstract state formulas as sub formulas/trees. * * @par Semantics * The formula holds iff in the next step, \e child holds @@ -27,11 +48,11 @@ namespace formula { * 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class Next : public PctlPathFormula { +class Next : public AbstractPathFormula { public: /*! @@ -46,7 +67,7 @@ public: * * @param child The child node */ - Next(PctlStateFormula* child) { + Next(AbstractStateFormula* child) { this->child = child; } @@ -65,7 +86,7 @@ public: /*! * @returns the child node */ - const PctlStateFormula& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -73,7 +94,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PctlStateFormula* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } @@ -95,7 +116,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { Next* result = new Next(); if (child != NULL) { result->setChild(child); @@ -112,12 +133,22 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkNext(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNext(*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: - PctlStateFormula* child; + AbstractStateFormula* child; }; } //namespace formula diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h index 204c102a8..4a459c5e8 100644 --- a/src/formula/NoBoundOperator.h +++ b/src/formula/NoBoundOperator.h @@ -8,26 +8,47 @@ #ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_ #define STORM_FORMULA_NOBOUNDOPERATOR_H_ -#include "PctlFormula.h" -#include "PctlPathFormula.h" +#include "AbstractFormula.h" +#include "AbstractPathFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace formula { +template class NoBoundOperator; + +/*! + * @brief Interface class for model checkers that support NoBoundOperator. + * + * All model checkers that support the formula class NoBoundOperator must inherit + * this pure virtual class. + */ +template +class INoBoundOperatorModelChecker { + public: + /*! + * @brief Evaluates NoBoundOperator formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkNoBoundOperator(const NoBoundOperator& obj) const = 0; +}; + /*! * @brief - * Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities + * 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 PCTL path formula as sub formula/tree. + * 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 PctlFormula. + * 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. @@ -39,14 +60,14 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PctlStateFormula - * @see PctlPathFormula + * @see AbstractStateFormula + * @see AbstractPathFormula * @see ProbabilisticOperator * @see ProbabilisticIntervalOperator - * @see PctlFormula + * @see AbstractFormula */ template -class NoBoundOperator: public storm::formula::PctlFormula { +class NoBoundOperator: public storm::formula::AbstractFormula { public: /*! * Empty constructor @@ -60,7 +81,7 @@ public: * * @param pathFormula The child node. */ - NoBoundOperator(PctlPathFormula* pathFormula) { + NoBoundOperator(AbstractPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -74,9 +95,9 @@ public: } /*! - * @returns the child node (representation of a PCTL path formula) + * @returns the child node (representation of a Abstract path formula) */ - const PctlPathFormula& getPathFormula () const { + const AbstractPathFormula& getPathFormula () const { return *pathFormula; } @@ -85,7 +106,7 @@ public: * * @param pathFormula the path formula that becomes the new child node */ - void setPathFormula(PctlPathFormula* pathFormula) { + void setPathFormula(AbstractPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -100,17 +121,27 @@ public: * * @returns A vector indicating all states that satisfy the formula represented by the called object. */ - virtual std::vector* check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkNoBoundOperator(*this); + virtual std::vector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNoBoundOperator(*this); } /*! * @returns a string representation of the formula */ virtual std::string toString() const = 0; + + /*! + * @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->pathFormula); + } private: - PctlPathFormula* pathFormula; + AbstractPathFormula* pathFormula; }; } /* namespace formula */ diff --git a/src/formula/Not.h b/src/formula/Not.h index 03d5cf572..cd7a20399 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -8,26 +8,48 @@ #ifndef STORM_FORMULA_NOT_H_ #define STORM_FORMULA_NOT_H_ -#include "PctlStateFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelChecker/AbstractModelChecker.h" namespace storm { namespace formula { +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 PCTL formula tree with NOT node as root. + * Class for a Abstract formula tree with NOT node as root. * - * Has one PCTL state formula as sub formula/tree. + * 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 PctlStateFormula - * @see PctlFormula + * @see AbstractStateFormula + * @see AbstractFormula */ template -class Not : public PctlStateFormula { +class Not : public AbstractStateFormula { public: /*! @@ -41,7 +63,7 @@ public: * Constructor * @param child The child node */ - Not(PctlStateFormula* child) { + Not(AbstractStateFormula* child) { this->child = child; } @@ -60,7 +82,7 @@ public: /*! * @returns The child node */ - const PctlStateFormula& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -68,7 +90,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PctlStateFormula* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } @@ -88,7 +110,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { + virtual AbstractStateFormula* clone() const { Not* result = new Not(); if (child != NULL) { result->setChild(child); @@ -105,12 +127,22 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkNot(*this); + 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: - PctlStateFormula* child; + AbstractStateFormula* child; }; } //namespace formula diff --git a/src/formula/Or.h b/src/formula/Or.h index 524ca58e7..e7dd117e5 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -8,17 +8,37 @@ #ifndef STORM_FORMULA_OR_H_ #define STORM_FORMULA_OR_H_ -#include "PctlStateFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { - namespace formula { +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 PCTL formula tree with OR node as root. + * Class for a Abstract formula tree with OR node as root. * - * Has two PCTL state formulas as sub formulas/trees. + * 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. @@ -26,11 +46,11 @@ namespace 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 PctlStateFormula - * @see PctlFormula + * @see AbstractStateFormula + * @see AbstractFormula */ template -class Or : public PctlStateFormula { +class Or : public AbstractStateFormula { public: /*! @@ -49,7 +69,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - Or(PctlStateFormula* left, PctlStateFormula* right) { + Or(AbstractStateFormula* left, AbstractStateFormula* right) { this->left = left; this->right = right; } @@ -74,7 +94,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PctlStateFormula* newLeft) { + void setLeft(AbstractStateFormula* newLeft) { left = newLeft; } @@ -83,21 +103,21 @@ public: * * @param newRight the new right child. */ - void setRight(PctlStateFormula* newRight) { + void setRight(AbstractStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PctlStateFormula& getLeft() const { + const AbstractStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PctlStateFormula& getRight() const { + const AbstractStateFormula& getRight() const { return *right; } @@ -120,7 +140,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { + virtual AbstractStateFormula* clone() const { Or* result = new Or(); if (this->left != NULL) { result->setLeft(left->clone()); @@ -130,7 +150,7 @@ public: } return result; } - + /*! * Calls the model checker to check this formula. * Needed to infer the correct type of formula class. @@ -140,13 +160,23 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkOr(*this); + 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: - PctlStateFormula* left; - PctlStateFormula* right; + AbstractStateFormula* left; + AbstractStateFormula* right; }; } //namespace formula diff --git a/src/formula/PctlFormula.h b/src/formula/PctlFormula.h deleted file mode 100644 index 394e3cfa2..000000000 --- a/src/formula/PctlFormula.h +++ /dev/null @@ -1,48 +0,0 @@ -/* - * Pctlformula.h - * - * Created on: 19.10.2012 - * Author: Thomas Heinemann - */ - -#ifndef STORM_FORMULA_PCTLFORMULA_H_ -#define STORM_FORMULA_PCTLFORMULA_H_ - -#include - -namespace storm { - -namespace formula { - - -//abstract -/*! - * @brief - * Abstract base class for PCTL formulas in general. - * - * @attention This class is abstract. - * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so - * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes - * PctlPathFormula and PctlStateFormula offer the method clone(). - */ -template -class PctlFormula { - -public: - /*! - * virtual destructor - */ - virtual ~PctlFormula() { } - - /*! - * @note This function is not implemented in this class. - * @returns a string representation of the formula - */ - virtual std::string toString() const = 0; -}; - -} //namespace formula - -} //namespace storm - -#endif /* STORM_FORMULA_PCTLFORMULA_H_ */ diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h new file mode 100644 index 000000000..e99cb0666 --- /dev/null +++ b/src/formula/PrctlFormulaChecker.h @@ -0,0 +1,46 @@ +#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_ +#define STORM_FORMULA_PRCTLFORMULACHECKER_H_ + +#include "src/formula/AbstractFormulaChecker.h" +#include "src/formula/Formulas.h" + +#include + +namespace storm { +namespace formula { + +/*! + * @brief Checks formulas if they are within PRCTL. + * + * This class implements AbstractFormulaChecker to check if a given formula + * is part of PRCTL logic. + */ +template +class PrctlFormulaChecker : public AbstractFormulaChecker { + public: + /*! + * Implementation of AbstractFormulaChecker::conforms() using code + * looking exactly like the sample code given there. + * + * We currently allow And, Ap, Eventually, Not, Or, + * ProbabilisticNoBoundOperator. + */ + virtual bool conforms(const AbstractFormula* formula) const { + if ( + dynamic_cast*>(formula) || + dynamic_cast*>(formula) || + dynamic_cast*>(formula) || + dynamic_cast*>(formula) || + dynamic_cast*>(formula) || + dynamic_cast*>(formula) + ) { + return formula->conforms(*this); + } + return false; + } +}; + +} // namespace formula +} // namespace storm + +#endif \ No newline at end of file diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index e541619c1..5ac0ff606 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -8,21 +8,20 @@ #ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ #define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ -#include "PctlStateFormula.h" -#include "PctlPathFormula.h" +#include "AbstractStateFormula.h" +#include "AbstractPathFormula.h" #include "BoundOperator.h" #include "utility/ConstTemplates.h" namespace storm { - namespace formula { /*! * @brief - * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval + * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval * as root. * - * Has one PCTL path formula as sub formula/tree. + * 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 @@ -32,11 +31,11 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PctlStateFormula - * @see PctlPathFormula + * @see AbstractStateFormula + * @see AbstractPathFormula * @see ProbabilisticOperator * @see ProbabilisticNoBoundsOperator - * @see PctlFormula + * @see AbstractFormula */ template class ProbabilisticBoundOperator : public BoundOperator { @@ -45,10 +44,12 @@ public: /*! * Empty constructor */ +//! TODO: this constructor should give a comparisontype as first argument ProbabilisticBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { // Intentionally left empty } + /*! * Constructor * @@ -56,7 +57,7 @@ public: * @param upperBound The upper bound for the probability * @param pathFormula The child node */ - ProbabilisticBoundOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { + ProbabilisticBoundOperator(T lowerBound, T upperBound, AbstractPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { // Intentionally left empty } @@ -81,7 +82,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { + virtual AbstractStateFormula* clone() const { ProbabilisticBoundOperator* result = new ProbabilisticBoundOperator(); result->setInterval(this->getLowerBound(), this->getUpperBound()); result->setPathFormula(this->getPathFormula()->clone()); @@ -90,7 +91,6 @@ public: }; } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/ProbabilisticNoBoundOperator.h index ad4ab4851..07e79659c 100644 --- a/src/formula/ProbabilisticNoBoundOperator.h +++ b/src/formula/ProbabilisticNoBoundOperator.h @@ -8,27 +8,26 @@ #ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ #define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ -#include "PctlFormula.h" -#include "PctlPathFormula.h" +#include "AbstractFormula.h" +#include "AbstractPathFormula.h" #include "NoBoundOperator.h" namespace storm { - namespace formula { /*! * @brief - * Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities + * 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 PCTL path formula as sub formula/tree. + * 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 PctlFormula. + * 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. @@ -40,11 +39,11 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PctlStateFormula - * @see PctlPathFormula + * @see AbstractStateFormula + * @see AbstractPathFormula * @see ProbabilisticOperator * @see ProbabilisticIntervalOperator - * @see PctlFormula + * @see AbstractFormula */ template class ProbabilisticNoBoundOperator: public NoBoundOperator { @@ -61,7 +60,7 @@ public: * * @param pathFormula The child node. */ - ProbabilisticNoBoundOperator(PctlPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) : NoBoundOperator(pathFormula) { // Intentionally left empty } @@ -77,7 +76,6 @@ public: }; } /* namespace formula */ - } /* namespace storm */ #endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h index 9f5d6ee43..54e2f447b 100644 --- a/src/formula/ReachabilityReward.h +++ b/src/formula/ReachabilityReward.h @@ -8,27 +8,48 @@ #ifndef STORM_FORMULA_REACHABILITYREWARD_H_ #define STORM_FORMULA_REACHABILITYREWARD_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelChecker/AbstractModelChecker.h" namespace storm { - namespace formula { +template class ReachabilityReward; + +/*! + * @brief Interface class for model checkers that support ReachabilityReward. + * + * All model checkers that support the formula class ReachabilityReward must inherit + * this pure virtual class. + */ +template +class IReachabilityRewardModelChecker { + public: + /*! + * @brief Evaluates ReachabilityReward formula within a model checker. + * + * @param obj Formula object with subformulas. + * @return Result of the formula for every node. + */ + virtual std::vector* checkReachabilityReward(const ReachabilityReward& obj) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with an Reachability Reward node as root. + * Class for a Abstract (path) formula tree with an Reachability Reward node as root. * - * Has one PCTL state formula as sub formula/tree. + * 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 nullptr before deletion) * - * @see PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class ReachabilityReward : public PctlPathFormula { +class ReachabilityReward : public AbstractPathFormula { public: /*! @@ -43,7 +64,7 @@ public: * * @param child The child node */ - ReachabilityReward(PctlStateFormula* child) { + ReachabilityReward(AbstractStateFormula* child) { this->child = child; } @@ -62,7 +83,7 @@ public: /*! * @returns the child node */ - const PctlStateFormula& getChild() const { + const AbstractStateFormula& getChild() const { return *child; } @@ -70,7 +91,7 @@ public: * Sets the subtree * @param child the new child node */ - void setChild(PctlStateFormula* child) { + void setChild(AbstractStateFormula* child) { this->child = child; } @@ -88,9 +109,9 @@ public: * * 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. + * @returns a new ReachabilityReward-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { ReachabilityReward* result = new ReachabilityReward(); if (child != nullptr) { result->setChild(child); @@ -107,16 +128,25 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkReachabilityReward(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkReachabilityReward(*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: - PctlStateFormula* child; + AbstractStateFormula* child; }; } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_REACHABILITYREWARD_H_ */ diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index 8118fdbe2..3f30ec0c7 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -8,18 +8,17 @@ #ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_ #define STORM_FORMULA_REWARDBOUNDOPERATOR_H_ -#include "PctlStateFormula.h" -#include "PctlPathFormula.h" +#include "AbstractStateFormula.h" +#include "AbstractPathFormula.h" #include "BoundOperator.h" #include "utility/ConstTemplates.h" namespace storm { - namespace formula { /*! * @brief - * Class for a PCTL formula tree with a R (reward) operator node over a reward interval as root. + * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root. * * Has a reward path formula as sub formula/tree. * @@ -31,11 +30,11 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PctlStateFormula - * @see PctlPathFormula + * @see AbstractStateFormula + * @see AbstractPathFormula * @see ProbabilisticOperator * @see ProbabilisticNoBoundsOperator - * @see PctlFormula + * @see AbstractFormula */ template class RewardBoundOperator : public BoundOperator { @@ -44,6 +43,7 @@ public: /*! * Empty constructor */ +//! TODO: this constructor should give a comparisontype as first argument RewardBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -55,7 +55,7 @@ public: * @param upperBound The upper bound for the probability * @param pathFormula The child node */ - RewardBoundOperator(T lowerBound, T upperBound, PctlPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { + RewardBoundOperator(T lowerBound, T upperBound, AbstractPathFormula& pathFormula) : BoundOperator(lowerBound, upperBound, pathFormula) { // Intentionally left empty } @@ -80,7 +80,7 @@ public: * * @returns a new AND-object that is identical the called object. */ - virtual PctlStateFormula* clone() const { + virtual AbstractStateFormula* clone() const { RewardBoundOperator* result = new RewardBoundOperator(); result->setBound(this->getLowerBound(), this->getUpperBound()); result->setPathFormula(this->getPathFormula()->clone()); @@ -89,7 +89,6 @@ public: }; } //namespace formula - } //namespace storm #endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */ diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/RewardNoBoundOperator.h index 3362ff136..f362a5232 100644 --- a/src/formula/RewardNoBoundOperator.h +++ b/src/formula/RewardNoBoundOperator.h @@ -8,27 +8,26 @@ #ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ #define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ -#include "PctlFormula.h" -#include "PctlPathFormula.h" +#include "AbstractFormula.h" +#include "AbstractPathFormula.h" #include "NoBoundOperator.h" namespace storm { - namespace formula { /*! * @brief - * Class for a PCTL formula tree with a R (reward) operator without declaration of reward values + * Class for a Abstract formula tree with a R (reward) operator without declaration of reward values * as root. * * Checking a formula with this operator as root returns the reward for the reward path formula for * each state * - * Has one PCTL path formula as sub formula/tree. + * 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 PctlFormula. + * 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. @@ -40,11 +39,11 @@ namespace formula { * (this behavior can be prevented by setting them to NULL before deletion) * * - * @see PctlStateFormula - * @see PctlPathFormula + * @see AbstractStateFormula + * @see AbstractPathFormula * @see ProbabilisticOperator * @see ProbabilisticIntervalOperator - * @see PctlFormula + * @see AbstractFormula */ template class RewardNoBoundOperator: public NoBoundOperator { @@ -61,7 +60,7 @@ public: * * @param pathFormula The child node. */ - RewardNoBoundOperator(PctlPathFormula* pathFormula) : NoBoundOperator(pathFormula) { + RewardNoBoundOperator(AbstractPathFormula* pathFormula) : NoBoundOperator(pathFormula) { // Intentionally left empty } @@ -77,7 +76,6 @@ public: }; } /* namespace formula */ - } /* namespace storm */ #endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Until.h b/src/formula/Until.h index be86a1153..82ac05c9d 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -8,18 +8,38 @@ #ifndef STORM_FORMULA_UNTIL_H_ #define STORM_FORMULA_UNTIL_H_ -#include "PctlPathFormula.h" -#include "PctlStateFormula.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { - namespace formula { +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) const = 0; +}; + /*! * @brief - * Class for a PCTL (path) formula tree with an Until node as root. + * Class for a Abstract (path) formula tree with an Until node as root. * - * Has two PCTL state formulas as sub formulas/trees. + * 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, @@ -28,11 +48,11 @@ namespace 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 PctlPathFormula - * @see PctlFormula + * @see AbstractPathFormula + * @see AbstractFormula */ template -class Until : public PctlPathFormula { +class Until : public AbstractPathFormula { public: /*! @@ -49,7 +69,7 @@ public: * @param left The left formula subtree * @param right The left formula subtree */ - Until(PctlStateFormula* left, PctlStateFormula* right) { + Until(AbstractStateFormula* left, AbstractStateFormula* right) { this->left = left; this->right = right; } @@ -74,7 +94,7 @@ public: * * @param newLeft the new left child. */ - void setLeft(PctlStateFormula* newLeft) { + void setLeft(AbstractStateFormula* newLeft) { left = newLeft; } @@ -83,21 +103,21 @@ public: * * @param newRight the new right child. */ - void setRight(PctlStateFormula* newRight) { + void setRight(AbstractStateFormula* newRight) { right = newRight; } /*! * @returns a pointer to the left child node */ - const PctlStateFormula& getLeft() const { + const AbstractStateFormula& getLeft() const { return *left; } /*! * @returns a pointer to the right child node */ - const PctlStateFormula& getRight() const { + const AbstractStateFormula& getRight() const { return *right; } @@ -120,7 +140,7 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - virtual PctlPathFormula* clone() const { + virtual AbstractPathFormula* clone() const { Until* result = new Until(); if (left != NULL) { result->setLeft(left->clone()); @@ -140,13 +160,23 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { - return modelChecker.checkUntil(*this); + virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkUntil(*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: - PctlStateFormula* left; - PctlStateFormula* right; + AbstractStateFormula* left; + AbstractStateFormula* right; }; } //namespace formula diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelChecker/AbstractModelChecker.h new file mode 100644 index 000000000..110d355dd --- /dev/null +++ b/src/modelChecker/AbstractModelChecker.h @@ -0,0 +1,57 @@ +/* + * DtmcPrctlModelChecker.h + * + * Created on: 22.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ +#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_ + +namespace storm { namespace modelChecker { +template class AbstractModelChecker; +}} + +//#include "src/formula/Formulas.h" +#include "src/formula/Or.h" +#include "src/formula/Ap.h" +#include "src/storage/BitVector.h" + +#include + +namespace storm { +namespace modelChecker { + +/*! + * @brief + * Interface for model checker classes. + * + * This class provides basic functions that are the same for all subclasses, but mainly only declares + * abstract methods that are to be implemented in concrete instances. + * + * @attention This class is abstract. + */ +template +class AbstractModelChecker : + public virtual storm::formula::IOrModelChecker, + public virtual storm::formula::IApModelChecker + { + +public: + template