From 43b56fce62f13d525d2c4a8e4018396d1fec3cf4 Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 29 Jan 2013 21:22:56 +0100 Subject: [PATCH] first version of BoundedNaryUntil. clone() does not work yet... --- src/formula/BoundedNaryUntil.h | 209 +++++++++++++++++++++++++++++++++ src/formula/Formulas.h | 1 + 2 files changed, 210 insertions(+) create mode 100644 src/formula/BoundedNaryUntil.h diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h new file mode 100644 index 000000000..bbd370cd9 --- /dev/null +++ b/src/formula/BoundedNaryUntil.h @@ -0,0 +1,209 @@ +/* + * 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, AbstractStateFormula* right, + uint_fast64_t bound) { + 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) { + //TODO: implement clone of std::vector + //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) 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/Formulas.h b/src/formula/Formulas.h index 09de1acf0..1a750f674 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -15,6 +15,7 @@ #include "And.h" #include "Ap.h" #include "BoundedUntil.h" +#include "BoundedNaryUntil.h" #include "Next.h" #include "Not.h" #include "Or.h"