diff --git a/src/formula/Csl.h b/src/formula/Csl.h new file mode 100644 index 000000000..9266df327 --- /dev/null +++ b/src/formula/Csl.h @@ -0,0 +1,28 @@ +/* + * Csl.h + * + * Created on: 19.04.2013 + * Author: thomas + */ + +#ifndef CSL_H_ +#define CSL_H_ + +#include "Csl/And.h" +#include "Csl/Ap.h" +#include "Csl/Next.h" +#include "Csl/Not.h" +#include "Csl/Or.h" +#include "Csl/ProbabilisticNoBoundOperator.h" +#include "Csl/ProbabilisticBoundOperator.h" +#include "Csl/SteadyStateNoBoundOperator.h" +#include "Csl/SteadyStateBoundOperator.h" + +#include "Csl/Until.h" +#include "Csl/Eventually.h" +#include "Csl/Globally.h" +#include "Csl/TimeBoundedEventually.h" +#include "Csl/TimeBoundedUntil.h" + + +#endif /* CSL_H_ */ diff --git a/src/formula/Csl/AbstractCslFormula.h b/src/formula/Csl/AbstractCslFormula.h new file mode 100644 index 000000000..af32a9ad1 --- /dev/null +++ b/src/formula/Csl/AbstractCslFormula.h @@ -0,0 +1,28 @@ +/* + * AbstractCslFormula.h + * + * Created on: 19.04.2013 + * Author: thomas + */ + +#ifndef ABSTRACTCSLFORMULA_H_ +#define ABSTRACTCSLFORMULA_H_ + +#include "src/formula/abstract/AbstractFormula.h" + +namespace storm { +namespace formula { +namespace csl { + +template +class AbstractCslFormula : public virtual storm::formula::abstract::AbstractFormula{ +public: + virtual ~AbstractCslFormula() { + // Intentionally left empty + } +}; + +} /* namespace csl */ +} /* namespace formula */ +} /* namespace storm */ +#endif /* ABSTRACTCSLFORMULA_H_ */ diff --git a/src/formula/Csl/AbstractNoBoundOperator.h b/src/formula/Csl/AbstractNoBoundOperator.h new file mode 100644 index 000000000..860bd51cf --- /dev/null +++ b/src/formula/Csl/AbstractNoBoundOperator.h @@ -0,0 +1,80 @@ +/* + * AbstractNoBoundOperator.h + * + * Created on: 16.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ +#define STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ + +#include "AbstractCslFormula.h" +#include "src/formula/abstract/IOptimizingOperator.h" + +namespace storm { +namespace formula { +namespace csl { + +template +class AbstractNoBoundOperator; + +/*! + * @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 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 AbstractNoBoundOperator& obj) const = 0; + + +}; + +template +class AbstractNoBoundOperator: public AbstractCslFormula/*, + public virtual storm::formula::abstract::IOptimizingOperator*/ { +public: + AbstractNoBoundOperator() { + // TODO Auto-generated constructor stub + + } + virtual ~AbstractNoBoundOperator() { + // TODO Auto-generated destructor stub + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @note This function is not implemented in this class. + * @returns a new AND-object that is identical the called object. + */ + virtual AbstractNoBoundOperator* 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. + * + * @note This function is not implemented in this class. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative=false) const = 0; +}; + +} /* namespace csl */ +} /* namespace formula */ +} /* namespace storm */ +#endif /* STORM_FORMULA_CSL_ABSTRACTNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/AbstractPathFormula.h b/src/formula/Csl/AbstractPathFormula.h index 459cbd057..f3369558c 100644 --- a/src/formula/Csl/AbstractPathFormula.h +++ b/src/formula/Csl/AbstractPathFormula.h @@ -5,14 +5,18 @@ * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_ -#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_ +#ifndef STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ +#define STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ -namespace storm { namespace formula { -template class AbstractPathFormula; -}} +namespace storm { +namespace formula { +namespace csl { +template class AbstractPathFormula; +} //namespace csl +} //namespace formula +} //namespace storm -#include "src/formula/AbstractFormula.h" +#include "src/formula/abstract/AbstractFormula.h" #include "src/modelchecker/ForwardDeclarations.h" #include @@ -21,6 +25,7 @@ template class AbstractPathFormula; namespace storm { namespace formula { +namespace csl { /*! * @brief @@ -32,13 +37,15 @@ namespace formula { * clone(). */ template -class AbstractPathFormula : public virtual AbstractFormula { +class AbstractPathFormula : public virtual storm::formula::abstract::AbstractFormula { public: /*! * empty destructor */ - virtual ~AbstractPathFormula() { } + virtual ~AbstractPathFormula() { + // Intentionally left empty + } /*! * Clones the called object. @@ -64,7 +71,8 @@ public: virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; }; +} //namespace csl } //namespace formula } //namespace storm -#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */ +#endif /* STORM_FORMULA_CSL_ABSTRACTPATHFORMULA_H_ */ diff --git a/src/formula/Csl/AbstractStateFormula.h b/src/formula/Csl/AbstractStateFormula.h index cf15fdb30..08347c2a1 100644 --- a/src/formula/Csl/AbstractStateFormula.h +++ b/src/formula/Csl/AbstractStateFormula.h @@ -5,19 +5,24 @@ * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_ -#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_ +#ifndef STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_ +#define STORM_FORMULA_CSL_ABSTRACTSTATEFORMULA_H_ -namespace storm { namespace formula { -template class AbstractStateFormula; -}} +namespace storm { +namespace formula { +namespace csl { +template class AbstractStateFormula; +} +} +} -#include "src/formula/AbstractFormula.h" +#include "AbstractCslFormula.h" #include "src/storage/BitVector.h" #include "src/modelchecker/ForwardDeclarations.h" namespace storm { namespace formula { +namespace csl { /*! * @brief @@ -29,13 +34,15 @@ namespace formula { * clone(). */ template -class AbstractStateFormula : public AbstractFormula { +class AbstractStateFormula : public AbstractCslFormula { public: /*! * empty destructor */ - virtual ~AbstractStateFormula() { } + virtual ~AbstractStateFormula() { + // Intentionally left empty + } /*! * Clones the called object. @@ -58,11 +65,12 @@ 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::AbstractModelChecker& modelChecker) const = 0; // { + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const = 0; }; +} //namespace csl } //namespace formula } //namespace storm -#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */ +#endif /* STORM_FORMULA_CSL_AbstractSTATEFORMULA_H_ */ diff --git a/src/formula/Csl/And.h b/src/formula/Csl/And.h new file mode 100644 index 000000000..74371bae7 --- /dev/null +++ b/src/formula/Csl/And.h @@ -0,0 +1,129 @@ +/* + * And.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_AND_H_ +#define STORM_FORMULA_CSL_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 csl { + +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->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkAnd(*this); + } + +}; + +} //namespace csl + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_CSL_AND_H_ */ diff --git a/src/formula/Csl/Ap.h b/src/formula/Csl/Ap.h new file mode 100644 index 000000000..c5617ce6c --- /dev/null +++ b/src/formula/Csl/Ap.h @@ -0,0 +1,106 @@ +/* + * Ap.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_AP_H_ +#define STORM_FORMULA_CSL_AP_H_ + +#include "AbstractStateFormula.h" +#include "src/formula/abstract/Ap.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace csl { + +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 Abstract formula tree with atomic proposition as root. + * + * This class represents the leaves in the formula tree. + * + * @see AbstractFormula + * @see AbstractFormula + */ +template +class Ap : public storm::formula::abstract::Ap, + public AbstractStateFormula { + +public: + /*! + * Constructor + * + * Creates a new atomic proposition leaf, with the label Ap + * + * @param ap The string representing the atomic proposition + */ + Ap(std::string ap) + : storm::formula::abstract::Ap(ap) { + // Intentionally left empty + } + + /*! + * Destructor. + * At this time, empty... + */ + virtual ~Ap() { + // 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 { + return new Ap(this->getAp()); + } + + /*! + * 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()->checkAp(*this); + } + +}; + +} //namespace abstract + +} //namespace formula + +} //namespace storm + +#endif /* STORM_FORMULA_CSL_AP_H_ */ diff --git a/src/formula/Csl/Eventually.h b/src/formula/Csl/Eventually.h new file mode 100644 index 000000000..2730615a7 --- /dev/null +++ b/src/formula/Csl/Eventually.h @@ -0,0 +1,120 @@ +/* + * Next.h + * + * Created on: 26.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_CSL_EVENTUALLY_H_ +#define STORM_FORMULA_CSL_EVENTUALLY_H_ + +#include "src/formula/abstract/Eventually.h" +#include "src/formula/Csl/AbstractPathFormula.h" +#include "src/formula/Csl/AbstractStateFormula.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace csl { + +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() { + // Intentionally left empty + } + + /*! + * 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 (this->childIsSet()) { + result->setChild(this->getChild().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkEventually(*this, qualitative); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_EVENTUALLY_H_ */ diff --git a/src/formula/Csl/Globally.h b/src/formula/Csl/Globally.h new file mode 100644 index 000000000..0693ea92c --- /dev/null +++ b/src/formula/Csl/Globally.h @@ -0,0 +1,122 @@ +/* + * Next.h + * + * Created on: 26.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_FORMULA_CSL_GLOBALLY_H_ +#define STORM_FORMULA_CSL_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 csl { + +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 { + Globally* result = new Globally(); + if (this->childIsSet()) { + result->setChild(this->getChild().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkGlobally(*this, qualitative); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_GLOBALLY_H_ */ diff --git a/src/formula/Csl/Next.h b/src/formula/Csl/Next.h new file mode 100644 index 000000000..2c4a81cde --- /dev/null +++ b/src/formula/Csl/Next.h @@ -0,0 +1,120 @@ +/* + * Next.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_NEXT_H_ +#define STORM_FORMULA_CSL_NEXT_H_ + +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/abstract/Next.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace csl { + +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 (this->childIsSet()) { + result->setChild(this->getChild().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkNext(*this, qualitative); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_NEXT_H_ */ diff --git a/src/formula/Csl/Not.h b/src/formula/Csl/Not.h new file mode 100644 index 000000000..6829ab72a --- /dev/null +++ b/src/formula/Csl/Not.h @@ -0,0 +1,116 @@ +/* + * Not.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_NOT_H_ +#define STORM_FORMULA_CSL_NOT_H_ + +#include "AbstractStateFormula.h" +#include "src/formula/abstract/Not.h" +#include "src/formula/AbstractFormulaChecker.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { +namespace csl { + +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 storm::formula::abstract::Not>, + public AbstractStateFormula { + +public: + /*! + * Empty constructor + */ + Not() { + //intentionally left empty + } + + /*! + * Constructor + * @param child The child node + */ + Not(AbstractStateFormula* child) : + storm::formula::abstract::Not>(child){ + //intentionally left empty + } + + /*! + * Destructor + * + * Also deletes the subtree + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Not() { + //intentionally left empty + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const { + Not* result = new Not(); + if (this->childIsSet()) { + result->setChild(this->getChild().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkNot(*this); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_NOT_H_ */ diff --git a/src/formula/Csl/Or.h b/src/formula/Csl/Or.h new file mode 100644 index 000000000..2cf5c106d --- /dev/null +++ b/src/formula/Csl/Or.h @@ -0,0 +1,125 @@ +/* + * Or.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_OR_H_ +#define STORM_FORMULA_CSL_OR_H_ + +#include "AbstractStateFormula.h" +#include "src/formula/abstract/Or.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace csl { + +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 storm::formula::abstract::Or>, + public AbstractStateFormula { + +public: + /*! + * Empty constructor. + * Will create an OR-node without subnotes. The result does not represent a complete formula! + */ + Or() { + //intentionally left empty + } + + /*! + * Constructor. + * Creates an OR note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + Or(AbstractStateFormula* left, AbstractStateFormula* right) : + storm::formula::abstract::Or>(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 ~Or() { + //intentionally left empty + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const { + Or* result = new Or(); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + return modelChecker.template as()->checkOr(*this); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_OR_H_ */ diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h new file mode 100644 index 000000000..45ed587fc --- /dev/null +++ b/src/formula/Csl/ProbabilisticBoundOperator.h @@ -0,0 +1,121 @@ +/* + * ProbabilisticBoundOperator.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ +#define STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ + +#include "AbstractStateFormula.h" +#include "AbstractPathFormula.h" +#include "src/formula/abstract/ProbabilisticBoundOperator.h" +#include "utility/ConstTemplates.h" + +namespace storm { +namespace formula { +namespace csl { + +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 storm::formula::abstract::ProbabilisticBoundOperator>, + public AbstractStateFormula { + +public: + /*! + * Empty constructor + */ + ProbabilisticBoundOperator() : storm::formula::abstract::ProbabilisticBoundOperator> + (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( + storm::formula::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) + : storm::formula::abstract::ProbabilisticBoundOperator>(comparisonRelation, bound, pathFormula) { + // Intentionally left empty + } + + ProbabilisticBoundOperator( + storm::formula::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) + : storm::formula::abstract::ProbabilisticBoundOperator>(comparisonRelation, bound, pathFormula, minimumOperator){ + // 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 { + 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 csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_PROBABILISTICBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/ProbabilisticNoBoundOperator.h b/src/formula/Csl/ProbabilisticNoBoundOperator.h new file mode 100644 index 000000000..7bd3175a3 --- /dev/null +++ b/src/formula/Csl/ProbabilisticNoBoundOperator.h @@ -0,0 +1,115 @@ +/* + * ProbabilisticNoBoundOperator.h + * + * Created on: 12.12.2012 + * Author: thomas + */ + +#ifndef STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ +#define STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ + +#include "AbstractPathFormula.h" +#include "AbstractNoBoundOperator.h" +#include "src/formula/abstract/ProbabilisticNoBoundOperator.h" + +namespace storm { +namespace formula { +namespace csl { + +/*! + * @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 storm::formula::abstract::ProbabilisticNoBoundOperator>, + public AbstractNoBoundOperator { +public: + /*! + * Empty constructor + */ + ProbabilisticNoBoundOperator() { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param pathFormula The child node. + */ + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula) + : storm::formula::abstract::ProbabilisticNoBoundOperator>(pathFormula) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param pathFormula The child node. + */ + ProbabilisticNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) + : storm::formula::abstract::ProbabilisticNoBoundOperator>(pathFormula, minimumOperator) { + // Intentionally left empty + } + + /*! + * Destructor + */ + virtual ~ProbabilisticNoBoundOperator() { + // Intentionally left empty + } + + virtual AbstractNoBoundOperator* clone() const { + ProbabilisticNoBoundOperator* result = new ProbabilisticNoBoundOperator(); + if (this->pathFormulaIsSet()) { + 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. + * + * @note This function is not implemented in this class. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative=false) const { + return this->getPathFormula().check(modelChecker, qualitative); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_PROBABILISTICNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h index 3296c0452..875de1a50 100644 --- a/src/formula/Csl/SteadyStateBoundOperator.h +++ b/src/formula/Csl/SteadyStateBoundOperator.h @@ -5,18 +5,19 @@ * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_ -#define STORM_FORMULA_STEADYSTATEOPERATOR_H_ +#ifndef STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ +#define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ -#include "src/formula/AbstractPathFormula.h" -#include "src/formula/AbstractStateFormula.h" -#include "src/formula/StateBoundOperator.h" +#include "AbstractStateFormula.h" +#include "src/formula/abstract/SteadyStateBoundOperator.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace formula { +namespace csl { + template class SteadyStateBoundOperator; /*! @@ -53,14 +54,15 @@ class ISteadyStateBoundOperatorModelChecker { * @see AbstractFormula */ template -class SteadyStateBoundOperator : public StateBoundOperator { +class SteadyStateBoundOperator : public storm::formula::abstract::SteadyStateBoundOperator>, + public AbstractStateFormula { public: /*! * Empty constructor */ - SteadyStateBoundOperator() : StateBoundOperator - (StateBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + SteadyStateBoundOperator() : storm::formula::abstract::SteadyStateBoundOperator> + (LESS_EQUAL, storm::utility::constGetZero(), nullptr) { // Intentionally left empty } @@ -70,15 +72,15 @@ public: * @param stateFormula The child node */ SteadyStateBoundOperator( - typename StateBoundOperator::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : - StateBoundOperator(comparisonRelation, bound, stateFormula) { + storm::formula::ComparisonType comparisonRelation, T bound, AbstractStateFormula* stateFormula) : + storm::formula::abstract::SteadyStateBoundOperator>(comparisonRelation, bound, stateFormula) { } /*! - * @returns a string representation of the formula + * Destructor */ - virtual std::string toString() const { - return "S" + StateBoundOperator::toString(); + virtual ~SteadyStateBoundOperator() { + // Intentionally left empty } /*! @@ -109,7 +111,8 @@ public: }; +} //namespace csl } //namespace formula } //namespace storm -#endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */ +#endif /* STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ */ diff --git a/src/formula/Csl/SteadyStateNoBoundOperator.h b/src/formula/Csl/SteadyStateNoBoundOperator.h index c48354dea..41fabc942 100644 --- a/src/formula/Csl/SteadyStateNoBoundOperator.h +++ b/src/formula/Csl/SteadyStateNoBoundOperator.h @@ -5,13 +5,16 @@ * Author: thomas */ -#ifndef STORM_FORMULA_STEADYSTATENOBOUNDOPERATOR_H_ -#define STORM_FORMULA_STEADYSTATENOBOUNDOPERATOR_H_ +#ifndef STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ +#define STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ -#include "StateNoBoundOperator.h" +#include "AbstractStateFormula.h" +#include "AbstractNoBoundOperator.h" +#include "src/formula/abstract/SteadyStateNoBoundOperator.h" namespace storm { namespace formula { +namespace csl { template class SteadyStateNoBoundOperator; @@ -34,12 +37,13 @@ class ISteadyStateNoBoundOperatorModelChecker { }; template -class SteadyStateNoBoundOperator: public storm::formula::StateNoBoundOperator { +class SteadyStateNoBoundOperator: public storm::formula::abstract::SteadyStateNoBoundOperator>, + public AbstractNoBoundOperator { public: /*! * Empty constructor */ - SteadyStateNoBoundOperator() : StateNoBoundOperator() { + SteadyStateNoBoundOperator() : storm::formula::abstract::SteadyStateNoBoundOperator>() { // Intentionally left empty } @@ -49,15 +53,16 @@ public: * * @param stateFormula The state formula that forms the subtree */ - SteadyStateNoBoundOperator(AbstractStateFormula* stateFormula) : StateNoBoundOperator(stateFormula) { + SteadyStateNoBoundOperator(AbstractStateFormula* stateFormula) + : storm::formula::abstract::SteadyStateNoBoundOperator>(stateFormula) { // Intentionally left empty } /*! - * @returns a string representation of the formula + * Destructor */ - virtual std::string toString() const { - return "S" + StateNoBoundOperator::toString(); + ~SteadyStateNoBoundOperator() { + // Intentionally left empty } /*! @@ -67,12 +72,11 @@ public: * * @returns a new BoundedUntil-object that is identical the called object. */ - /* TODO: Add clone method to StateNoBoundOperator and use matching return type - virtual AbstractStateFormula* clone() const { + virtual AbstractNoBoundOperator * clone() const { SteadyStateNoBoundOperator* result = new SteadyStateNoBoundOperator(); result->setStateFormula(this->getStateFormula().clone()); return result; - }*/ + } /*! * Calls the model checker to check this formula. @@ -83,12 +87,14 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker) const { + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative=false) const { return modelChecker.template as()->checkSteadyStateNoBoundOperator(*this); } }; +} /* namespace csl */ } /* namespace formula */ } /* namespace storm */ -#endif /* STORM_FORMULA_STEADYSTATENOBOUNDOPERATOR_H_ */ + +#endif /* STORM_FORMULA_CSL_STEADYSTATENOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Csl/TimeBoundedEventually.h b/src/formula/Csl/TimeBoundedEventually.h index 01c67d00c..71c0def54 100644 --- a/src/formula/Csl/TimeBoundedEventually.h +++ b/src/formula/Csl/TimeBoundedEventually.h @@ -5,14 +5,16 @@ * Author: thomas */ -#ifndef STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ -#define STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ +#ifndef STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ +#define STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ -#include "TimeBoundedOperator.h" +#include "src/formula/abstract/TimeBoundedEventually.h" +#include "AbstractPathFormula.h" #include "AbstractStateFormula.h" namespace storm { namespace formula { +namespace csl { template class TimeBoundedEventually; @@ -36,7 +38,8 @@ class ITimeBoundedEventuallyModelChecker { template -class TimeBoundedEventually: public storm::formula::TimeBoundedOperator { +class TimeBoundedEventually: public storm::formula::abstract::TimeBoundedEventually>, + public AbstractPathFormula { public: /** * Simple constructor: Only sets the bounds @@ -44,46 +47,18 @@ public: * @param lowerBound * @param upperBound */ - TimeBoundedEventually(T lowerBound, T upperBound) : TimeBoundedOperator(lowerBound, upperBound) { - child = nullptr; + TimeBoundedEventually(T lowerBound, T upperBound) + : storm::formula::abstract::TimeBoundedEventually>(lowerBound, upperBound) { + // Intentionally left empty } - TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula* child) : - TimeBoundedOperator(lowerBound, upperBound) { - this->child = child; + TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula* child) + : storm::formula::abstract::TimeBoundedEventually>(lowerBound, upperBound, child) { + // Intentionally left empty } virtual ~TimeBoundedEventually() { - if (child != nullptr) { - delete child; - } - } - - - /*! - * @returns the child node - */ - const AbstractStateFormula& getChild() const { - return *child; - } - - /*! - * Sets the subtree - * @param child the new child node - */ - void setChild(AbstractStateFormula* child) { - this->child = child; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() const { - std::string result = "F"; - result += TimeBoundedOperator::toString(); - result += " "; - result += child->toString(); - return result; + // Intentionally left empty } /*! @@ -95,8 +70,8 @@ public: */ virtual AbstractPathFormula* clone() const { TimeBoundedEventually* result = new TimeBoundedEventually(this->getLowerBound(), this->getUpperBound()); - if (child != nullptr) { - result->setChild(child->clone()); + if (this->childIsSet()) { + result->setChild(this->getChild().clone()); } return result; } @@ -113,21 +88,10 @@ public: virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkTimeBoundedEventually(*this, qualitative); } - - /*! - * @brief Checks if the subtree conforms to some logic. - * - * @param checker Formula checker object. - * @return true iff the subtree conforms to some logic. - */ - virtual bool conforms(const AbstractFormulaChecker& checker) const { - return checker.conforms(this->child); - } - -private: - AbstractStateFormula* child; }; +} /* namespace csl */ } /* namespace formula */ } /* namespace storm */ -#endif /* STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ */ + +#endif /* STORM_FORMULA_CSL_TIMEBOUNDEDEVENTUALLY_H_ */ diff --git a/src/formula/Csl/TimeBoundedUntil.h b/src/formula/Csl/TimeBoundedUntil.h index a0cceac78..657fb66a6 100644 --- a/src/formula/Csl/TimeBoundedUntil.h +++ b/src/formula/Csl/TimeBoundedUntil.h @@ -5,13 +5,16 @@ * Author: thomas */ -#ifndef STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ -#define STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ +#ifndef STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ +#define STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ -#include "TimeBoundedOperator.h" +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/abstract/TimeBoundedUntil.h" namespace storm { namespace formula { +namespace csl { template class TimeBoundedUntil; @@ -34,7 +37,8 @@ class ITimeBoundedUntilModelChecker { }; template -class TimeBoundedUntil: public storm::formula::TimeBoundedOperator { +class TimeBoundedUntil: public storm::formula::abstract::TimeBoundedUntil>, + public AbstractPathFormula { public: /** * Constructor providing bounds only; @@ -44,12 +48,10 @@ public: * @param upperBound */ TimeBoundedUntil(T lowerBound, T upperBound) : - TimeBoundedOperator(lowerBound, upperBound) { - this->left = nullptr; - this->right = nullptr; + storm::formula::abstract::TimeBoundedUntil>(lowerBound, upperBound) { + // Intentionally left empty } - /** * Full constructor * @param lowerBound @@ -58,62 +60,15 @@ public: * @param right */ TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula* left, AbstractStateFormula* right) : - TimeBoundedOperator(lowerBound, upperBound) { - this->left = left; - this->right = right; - } - - virtual ~TimeBoundedUntil() { - if (left != nullptr) { - delete left; - } - if (right != nullptr) { - delete right; - } - } - - /*! - * Sets the left child node. - * - * @param newLeft the new left child. - */ - void setLeft(AbstractStateFormula* newLeft) { - left = newLeft; - } - - /*! - * Sets the right child node. - * - * @param newRight the new right child. - */ - void setRight(AbstractStateFormula* newRight) { - right = newRight; - } + storm::formula::abstract::TimeBoundedUntil>(lowerBound, upperBound, left, right) { - /*! - * @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 + * Destructor */ - virtual std::string toString() const { - std::string result = left->toString(); - result += " U"; - result += TimeBoundedOperator::toString(); - result += " "; - result += right->toString(); - return result; + virtual ~TimeBoundedUntil() { + // Intentionally left empty } /*! @@ -125,11 +80,11 @@ public: */ virtual AbstractPathFormula* clone() const { TimeBoundedUntil* result = new TimeBoundedUntil(this->getLowerBound(), this->getUpperBound()); - if (left != nullptr) { - result->setLeft(left->clone()); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); } - if (right != nullptr) { - result->setRight(right->clone()); + if (this->rightIsSet()) { + result->setRight(this->getRight().clone()); } return result; } @@ -147,22 +102,10 @@ public: virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { return modelChecker.template as()->checkTimeBoundedUntil(*this, qualitative); } - - /*! - * @brief Checks if the subtree conforms to some logic. - * - * @param checker Formula checker object. - * @return true iff the subtree conforms to some logic. - */ - virtual bool conforms(const AbstractFormulaChecker& checker) const { - return checker.conforms(this->left) && checker.conforms(this->right); - } - -private: - AbstractStateFormula* left; - AbstractStateFormula* right; }; +} /* namespace csl */ } /* namespace formula */ } /* namespace storm */ -#endif /* STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ */ + +#endif /* STORM_FORMULA_CSL_TIMEBOUNDEDUNTIL_H_ */ diff --git a/src/formula/Csl/Until.h b/src/formula/Csl/Until.h new file mode 100644 index 000000000..7ffe73647 --- /dev/null +++ b/src/formula/Csl/Until.h @@ -0,0 +1,125 @@ +/* + * Until.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_CSL_UNTIL_H_ +#define STORM_FORMULA_CSL_UNTIL_H_ + +#include "AbstractPathFormula.h" +#include "AbstractStateFormula.h" +#include "src/formula/abstract/Until.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace csl { + +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 storm::formula::abstract::Until>, + public AbstractPathFormula { + +public: + /*! + * Empty constructor + */ + Until() { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + */ + Until(AbstractStateFormula* left, AbstractStateFormula* right) + : storm::formula::abstract::Until>(left, right) { + // Intentionally left empty + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Until() { + // Intentionally left empty + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual AbstractPathFormula* clone() const { + Until* result = new Until(); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); + } + if (this->rightIsSet()) { + result->setRight(this->getRight().clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const { + return modelChecker.template as()->checkUntil(*this, qualitative); + } +}; + +} //namespace csl +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_CSL_UNTIL_H_ */ diff --git a/src/formula/Prctl/AbstractNoBoundOperator.h b/src/formula/Prctl/AbstractNoBoundOperator.h index 05d036e9b..7cb38319c 100644 --- a/src/formula/Prctl/AbstractNoBoundOperator.h +++ b/src/formula/Prctl/AbstractNoBoundOperator.h @@ -5,8 +5,8 @@ * Author: thomas */ -#ifndef ABSTRACTNOBOUNDOPERATOR_H_ -#define ABSTRACTNOBOUNDOPERATOR_H_ +#ifndef STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ +#define STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ #include "AbstractPrctlFormula.h" #include "src/formula/abstract/IOptimizingOperator.h" @@ -77,4 +77,4 @@ public: } /* namespace prctl */ } /* namespace formula */ } /* namespace storm */ -#endif /* ABSTRACTNOBOUNDOPERATOR_H_ */ +#endif /* STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_ */ diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h index a9de70cc0..4b49f7c40 100644 --- a/src/formula/Prctl/ProbabilisticBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticBoundOperator.h @@ -132,7 +132,7 @@ public: } }; -} //namespace formula +} //namespace prctl } //namespace formula } //namespace storm diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h index 331f4c9f3..b2fb1d71c 100644 --- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h +++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h @@ -108,7 +108,7 @@ public: } }; -} //namespace formula +} //namespace prctl } //namespace formula } //namespace storm diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h index 3456f21de..5db41d0b5 100644 --- a/src/formula/abstract/StateBoundOperator.h +++ b/src/formula/abstract/StateBoundOperator.h @@ -11,6 +11,7 @@ #include "src/formula/abstract/AbstractFormula.h" #include "src/formula/abstract/AbstractFormula.h" #include "src/formula/AbstractFormulaChecker.h" +#include "src/formula/ComparisonType.h" #include "src/modelchecker/AbstractModelChecker.h" #include "src/utility/ConstTemplates.h" @@ -39,11 +40,10 @@ namespace abstract { * @see ProbabilisticNoBoundsOperator * @see AbstractFormula */ -template +template class StateBoundOperator : public virtual AbstractFormula { public: - enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; /*! * Constructor @@ -52,7 +52,7 @@ public: * @param bound The bound for the probability * @param stateFormula The child node */ - StateBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* stateFormula) + StateBoundOperator(storm::formula::ComparisonType comparisonOperator, T bound, FormulaType* stateFormula) : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) { // Intentionally left empty } diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h index 794bb448f..d21690a45 100644 --- a/src/formula/abstract/StateNoBoundOperator.h +++ b/src/formula/abstract/StateNoBoundOperator.h @@ -8,7 +8,7 @@ #ifndef STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_ #define STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_ -#include "src/formula/abstract/AbstractFormula.h" +#include "AbstractFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/ForwardDeclarations.h" @@ -47,7 +47,7 @@ namespace abstract { * @see AbstractFormula */ template -class StateNoBoundOperator: public storm::formula::AbstractFormula { +class StateNoBoundOperator: public virtual AbstractFormula { public: /*! * Empty constructor @@ -90,21 +90,6 @@ public: return stateFormula != nullptr; } - /*! - * 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 */ diff --git a/src/formula/abstract/SteadyStateBoundOperator.h b/src/formula/abstract/SteadyStateBoundOperator.h new file mode 100644 index 000000000..2ce8d683f --- /dev/null +++ b/src/formula/abstract/SteadyStateBoundOperator.h @@ -0,0 +1,74 @@ +/* + * SteadyState.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_ +#define STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_ + +#include "StateBoundOperator.h" +#include "src/formula/AbstractFormulaChecker.h" + +namespace storm { +namespace formula { +namespace abstract { + +/*! + * @brief + * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root. + * + * Has two Abstract state formulas as sub formulas/trees. + * + * @par Semantics + * The formula holds iff \e child holds SteadyStateOperator 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 SteadyStateBoundOperator : public StateBoundOperator { + +public: + /*! + * Empty constructor + */ + SteadyStateBoundOperator() : StateBoundOperator + (LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + // Intentionally left empty + } + + /*! + * Constructor + * + * @param stateFormula The child node + */ + SteadyStateBoundOperator( + storm::formula::ComparisonType comparisonRelation, T bound, FormulaType* stateFormula) : + StateBoundOperator(comparisonRelation, bound, stateFormula) { + } + + /*! + * Destructor + */ + virtual ~SteadyStateBoundOperator() { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + return "S" + StateBoundOperator::toString(); + } +}; + +} //namespace abstract +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_ */ diff --git a/src/formula/abstract/SteadyStateNoBoundOperator.h b/src/formula/abstract/SteadyStateNoBoundOperator.h new file mode 100644 index 000000000..500b53a3a --- /dev/null +++ b/src/formula/abstract/SteadyStateNoBoundOperator.h @@ -0,0 +1,58 @@ +/* + * SteadyStateNoBoundOperator.h + * + * Created on: 09.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_ +#define STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_ + +#include "StateNoBoundOperator.h" + +namespace storm { +namespace formula { +namespace abstract { + +template +class SteadyStateNoBoundOperator: public StateNoBoundOperator { +public: + /*! + * Empty constructor + */ + SteadyStateNoBoundOperator() : StateNoBoundOperator() { + // Intentionally left empty + + } + + /*! + * Constructor + * + * @param stateFormula The state formula that forms the subtree + */ + SteadyStateNoBoundOperator(FormulaType* stateFormula) + : StateNoBoundOperator(stateFormula) { + // Intentionally left empty + } + + /*! + * Destructor + */ + virtual ~SteadyStateNoBoundOperator() { + // Intentionally left empty + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + return "S" + StateNoBoundOperator::toString(); + } + +}; + +} /* namespace abstract */ +} /* namespace formula */ +} /* namespace storm */ + +#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_ */ diff --git a/src/formula/abstract/TimeBoundedEventually.h b/src/formula/abstract/TimeBoundedEventually.h new file mode 100644 index 000000000..567cb1464 --- /dev/null +++ b/src/formula/abstract/TimeBoundedEventually.h @@ -0,0 +1,94 @@ +/* + * TimeBoundedEventually.h + * + * Created on: 10.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_ +#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_ + +#include "TimeBoundedOperator.h" + +namespace storm { +namespace formula { +namespace abstract { + + +template +class TimeBoundedEventually: public storm::formula::abstract::TimeBoundedOperator { +public: + /** + * Simple constructor: Only sets the bounds + * + * @param lowerBound + * @param upperBound + */ + TimeBoundedEventually(T lowerBound, T upperBound) : TimeBoundedOperator(lowerBound, upperBound) { + child = nullptr; + } + + TimeBoundedEventually(T lowerBound, T upperBound, FormulaType* child) : + TimeBoundedOperator(lowerBound, upperBound) { + this->child = child; + } + + virtual ~TimeBoundedEventually() { + if (child != nullptr) { + delete child; + } + } + + /*! + * @returns the child node + */ + const FormulaType& getChild() const { + return *child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(FormulaType* child) { + this->child = child; + } + + /*! + * + * @return True if the child is set, i.e. it does not point to nullptr; false otherwise + */ + bool childIsSet() const { + return child != nullptr; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "F"; + result += TimeBoundedOperator::toString(); + result += " "; + result += child->toString(); + return result; + } + + /*! + * @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: + FormulaType* child; +}; + +} /* namespace abstract */ +} /* namespace formula */ +} /* namespace storm */ + +#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_ */ diff --git a/src/formula/abstract/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h index 9dea94ef0..f0882d6ed 100644 --- a/src/formula/abstract/TimeBoundedOperator.h +++ b/src/formula/abstract/TimeBoundedOperator.h @@ -30,7 +30,7 @@ namespace abstract { * @see AbstractFormula */ template -class TimeBoundedOperator: public storm::formula::AbstractFormula { +class TimeBoundedOperator: public virtual AbstractFormula { public: /** * Constructor diff --git a/src/formula/abstract/TimeBoundedUntil.h b/src/formula/abstract/TimeBoundedUntil.h new file mode 100644 index 000000000..61841ac57 --- /dev/null +++ b/src/formula/abstract/TimeBoundedUntil.h @@ -0,0 +1,135 @@ +/* + * TimeBoundedUntil.h + * + * Created on: 10.04.2013 + * Author: thomas + */ + +#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_ +#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_ + +#include "TimeBoundedOperator.h" + +namespace storm { +namespace formula { +namespace abstract { + +template +class TimeBoundedUntil: public TimeBoundedOperator { +public: + /** + * Constructor providing bounds only; + * Sub formulas are set to null. + * + * @param lowerBound + * @param upperBound + */ + TimeBoundedUntil(T lowerBound, T upperBound) : + TimeBoundedOperator(lowerBound, upperBound) { + this->left = nullptr; + this->right = nullptr; + } + + + /** + * Full constructor + * @param lowerBound + * @param upperBound + * @param left + * @param right + */ + TimeBoundedUntil(T lowerBound, T upperBound, FormulaType* left, FormulaType* right) : + TimeBoundedOperator(lowerBound, upperBound) { + this->left = left; + this->right = right; + } + + virtual ~TimeBoundedUntil() { + if (left != nullptr) { + delete left; + } + if (right != nullptr) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(FormulaType* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(FormulaType* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + const FormulaType& getLeft() const { + return *left; + } + + /*! + * @returns a pointer to the right child node + */ + const FormulaType& getRight() const { + return *right; + } + + /*! + * + * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise + */ + bool leftIsSet() const { + return left != nullptr; + } + + /*! + * + * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise + */ + bool rightIsSet() const { + return right != nullptr; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = left->toString(); + result += " U"; + result += TimeBoundedOperator::toString(); + result += " "; + result += right->toString(); + return result; + } + + /*! + * @brief Checks if the subtree conforms to some logic. + * + * @param checker Formula checker object. + * @return true iff the subtree conforms to some logic. + */ + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->left) && checker.conforms(this->right); + } + +private: + FormulaType* left; + FormulaType* right; +}; + +} /* namespace abstract */ +} /* namespace formula */ +} /* namespace storm */ + +#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_ */ diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp index e69de29bb..e04e0c651 100644 --- a/src/parser/CslParser.cpp +++ b/src/parser/CslParser.cpp @@ -0,0 +1,220 @@ +/* + * CslParser.cpp + * + * Created on: 08.04.2013 + * Author: Thomas Heinemann + */ + +#include "src/parser/CslParser.h" +#include "src/utility/OsDetection.h" +#include "src/utility/ConstTemplates.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFormatException.h" + +// Used for Boost spirit. +#include +#include +#include + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +// Needed for file IO. +#include +#include +#include + + +// Some typedefs and namespace definitions to reduce code size. +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + + +namespace storm { +namespace parser { + +template +struct CslParser::CslGrammar : qi::grammar*(), Skipper > { + CslGrammar() : CslGrammar::base_type(start) { + freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; + + //This block defines rules for parsing state formulas + stateFormula %= orFormula; + stateFormula.name("state formula"); + orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = + phoenix::new_>(qi::_val, qi::_1)]; + orFormula.name("state formula"); + andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = + phoenix::new_>(qi::_val, qi::_1)]; + andFormula.name("state formula"); + notFormula = atomicStateFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicStateFormula)[qi::_val = + phoenix::new_>(qi::_1)]; + notFormula.name("state formula"); + + //This block defines rules for "atomic" state formulas + //(Propositions, probabilistic/reward formulas, and state formulas in brackets) + atomicStateFormula %= probabilisticBoundOperator | steadyStateBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")"); + atomicStateFormula.name("state formula"); + atomicProposition = (freeIdentifierName)[qi::_val = + phoenix::new_>(qi::_1)]; + atomicProposition.name("state formula"); + probabilisticBoundOperator = ( + (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::GREATER, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::GREATER_EQUAL, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::LESS, qi::_1, qi::_2)] | + (qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)] + ); + probabilisticBoundOperator.name("state formula"); + steadyStateBoundOperator = ( + (qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::GREATER, qi::_1, qi::_2)] | + (qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::GREATER_EQUAL, qi::_1, qi::_2)] | + (qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::LESS, qi::_1, qi::_2)] | + (qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)] + ); + steadyStateBoundOperator.name("state formula"); + + //This block defines rules for parsing formulas with noBoundOperators + noBoundOperator = (probabilisticNoBoundOperator | steadyStateNoBoundOperator); + noBoundOperator.name("no bound operator"); + probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)]; + probabilisticNoBoundOperator.name("no bound operator"); + steadyStateNoBoundOperator = (qi::lit("S") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> stateFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)]; + steadyStateNoBoundOperator.name("no bound operator"); + + //This block defines rules for parsing probabilistic path formulas + pathFormula = (timeBoundedEventually | eventually | globally | timeBoundedUntil | until); + pathFormula.name("path formula"); + timeBoundedEventually = ( + (qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val = + phoenix::new_>(qi::_1, qi::_2, qi::_3)] | + (qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val = + phoenix::new_>(0, qi::_1, qi::_2)] | + (qi::lit("F") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)[qi::_val = + phoenix::new_>(qi::_1, std::numeric_limits::infinity(), qi::_2)] + ); + timeBoundedEventually.name("path formula (for probabilistic operator)"); + eventually = (qi::lit("F") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + eventually.name("path formula (for probabilistic operator)"); + globally = (qi::lit("G") > stateFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + globally.name("path formula (for probabilistic operator)"); + timeBoundedUntil = ( + (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula) + [qi::_val = phoenix::new_>(qi::_2, qi::_3, phoenix::bind(&storm::formula::csl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_4)] | + (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula) + [qi::_val = phoenix::new_>(0, qi::_2, phoenix::bind(&storm::formula::csl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3)] | + (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula) + [qi::_val = phoenix::new_>(qi::_2, std::numeric_limits::infinity(), phoenix::bind(&storm::formula::csl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3)] + ); + timeBoundedUntil.name("path formula (for probabilistic operator)"); + until = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val = + phoenix::new_>(phoenix::bind(&storm::formula::csl::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; + until.name("path formula (for probabilistic operator)"); + + start = (noBoundOperator | stateFormula); + start.name("CSL formula"); + } + + qi::rule*(), Skipper> start; + + qi::rule*(), Skipper> stateFormula; + qi::rule*(), Skipper> atomicStateFormula; + + qi::rule*(), Skipper> andFormula; + qi::rule*(), Skipper> atomicProposition; + qi::rule*(), Skipper> orFormula; + qi::rule*(), Skipper> notFormula; + qi::rule*(), Skipper> probabilisticBoundOperator; + qi::rule*(), Skipper> steadyStateBoundOperator; + + qi::rule*(), Skipper> noBoundOperator; + qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> steadyStateNoBoundOperator; + + qi::rule*(), Skipper> pathFormula; + qi::rule*(), Skipper> timeBoundedEventually; + qi::rule*(), Skipper> eventually; + qi::rule*(), Skipper> globally; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> timeBoundedUntil; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; + + + qi::rule freeIdentifierName; + +}; + +CslParser::CslParser(std::string formulaString) { + // Prepare iterators to input. + BaseIteratorType stringIteratorBegin = formulaString.begin(); + BaseIteratorType stringIteratorEnd = formulaString.end(); + PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); + PositionIteratorType positionIteratorEnd; + + + // Prepare resulting intermediate representation of input. + storm::formula::csl::AbstractCslFormula* result_pointer = nullptr; + + CslGrammar grammar; + + // Now, parse the formula from the given string + try { + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << e.first.get_currentline() << std::endl << "\t"; + int i = 0; + for (i = 0; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + + std::cerr << msg.str(); + + // Now propagate exception. + throw storm::exceptions::WrongFormatException() << msg.str(); + } + + // The syntax can be so wrong that no rule can be matched at all + // In that case, no expectation failure is thrown, but the parser just returns nullptr + // Then, of course the result is not usable, hence we throw a WrongFormatException, too. + if (result_pointer == nullptr) { + throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; + } + + formula = result_pointer; +} + +CslParser::~CslParser() { + // Intentionally left empty + // Parsed formula is not deleted with the parser! +} + +} /* namespace parser */ +} /* namespace storm */ diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h index e69de29bb..bf8977348 100644 --- a/src/parser/CslParser.h +++ b/src/parser/CslParser.h @@ -0,0 +1,53 @@ +/* + * CslParser.h + * + * Created on: 08.04.2013 + * Author: Thomas Heinemann + */ + +#ifndef STORM_PARSER_CSLPARSER_H_ +#define STORM_PARSER_CSLPARSER_H_ + +#include "Parser.h" + +#include "src/formula/Csl.h" +//#include + +namespace storm { +namespace parser { + +class CslParser: public storm::parser::Parser { +public: + /*! + * Reads a CSL formula from its string representation and parses it into a formula tree, consisting of + * classes in the namespace storm::formula. + * + * If the string could not be parsed successfully, it will throw a wrongFormatException. + * + * @param formulaString The string representation of the formula + * @throw wrongFormatException If the input could not be parsed successfully + */ + CslParser(std::string formulaString); + virtual ~CslParser(); + + /*! + * @return a pointer to the parsed formula object + */ + storm::formula::csl::AbstractCslFormula* getFormula() { + return this->formula; + } + +private: +private: + storm::formula::csl::AbstractCslFormula* formula; + + /*! + * Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas. + */ + template + struct CslGrammar; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_CSLPARSER_H_ */ diff --git a/test/parser/CslParserTest.cpp b/test/parser/CslParserTest.cpp index 2d497b3d7..313142a14 100644 --- a/test/parser/CslParserTest.cpp +++ b/test/parser/CslParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/CslParser.h" -/* + TEST(CslParserTest, parseApOnlyTest) { std::string ap = "ap"; storm::parser::CslParser* cslParser = nullptr; @@ -50,9 +50,9 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) { ASSERT_NE(cslParser->getFormula(), nullptr); - storm::formula::ProbabilisticBoundOperator* op = static_cast*>(cslParser->getFormula()); + storm::formula::csl::ProbabilisticBoundOperator* op = static_cast*>(cslParser->getFormula()); - ASSERT_EQ(storm::formula::PathBoundOperator::GREATER, op->getComparisonOperator()); + ASSERT_EQ(storm::formula::GREATER, op->getComparisonOperator()); ASSERT_EQ(0.5, op->getBound()); ASSERT_EQ(cslParser->getFormula()->toString(), "P > 0.500000 [F a]"); @@ -70,9 +70,9 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { ASSERT_NE(cslParser->getFormula(), nullptr); - storm::formula::SteadyStateBoundOperator* op = static_cast*>(cslParser->getFormula()); + storm::formula::csl::SteadyStateBoundOperator* op = static_cast*>(cslParser->getFormula()); - ASSERT_EQ(storm::formula::StateBoundOperator::GREATER_EQUAL, op->getComparisonOperator()); + ASSERT_EQ(storm::formula::GREATER_EQUAL, op->getComparisonOperator()); ASSERT_EQ(15.0, op->getBound()); ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", cslParser->getFormula()->toString()); @@ -84,13 +84,13 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) { TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) { storm::parser::CslParser* cslParser = nullptr; ASSERT_NO_THROW( - cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F a ] ]") + cslParser = new storm::parser::CslParser("S = ? [ P <= 0.5 [ F<=3 a ] ]") ); ASSERT_NE(cslParser->getFormula(), nullptr); - ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F a]]"); + ASSERT_EQ(cslParser->getFormula()->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]"); delete cslParser->getFormula(); delete cslParser; @@ -113,6 +113,7 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) { } + TEST(CslParserTest, parseComplexFormulaTest) { storm::parser::CslParser* cslParser = nullptr; ASSERT_NO_THROW( @@ -128,6 +129,7 @@ TEST(CslParserTest, parseComplexFormulaTest) { } + TEST(CslParserTest, wrongProbabilisticFormulaTest) { storm::parser::CslParser* cslParser = nullptr; ASSERT_THROW( @@ -155,4 +157,3 @@ TEST(CslParserTest, wrongFormulaTest2) { ); delete cslParser; } -*/