diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 58b679d8b..d37972987 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -18,6 +18,7 @@ #include "PCTLPathFormula.h" #include "PCTLStateFormula.h" #include "ProbabilisticOperator.h" +#include "ProbabilisticIntervalOperator.h" #include "Until.h" #endif /* FORMULAS_H_ */ diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h new file mode 100644 index 000000000..acc6f5b5f --- /dev/null +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -0,0 +1,176 @@ +/* + * ProbabilisticOperator.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef PROBABILISTICINTERVALOPERATOR_H_ +#define PROBABILISTICINTERVALOPERATOR_H_ + +#include "PCTLStateFormula.h" +#include "PCTLPathFormula.h" +#include "utility/const_templates.h" + +namespace mrmc { + +namespace formula { + +/*! + * @brief + * Class for a PCTL formula tree with a P (probablistic) operator node over a probability interval + * as root. + * + * If the probability interval consist just of one single value (i.e. it is [x,x] for some + * real number x), the class ProbabilisticOperator should be used instead. + * + * + * Has one PCTL 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 PCTLStateFormula + * @see PCTLPathFormula + * @see ProbabilisticOperator + * @see PCTLFormula + */ +template +class ProbabilisticIntervalOperator : public PCTLStateFormula { + +public: + /*! + * Empty constructor + */ + ProbabilisticIntervalOperator() { + upper = mrmc::utility::constGetZero(upper); + lower = mrmc::utility::constGetZero(lower); + pathFormula = NULL; + } + + /*! + * Constructor + * + * @param lowerBound The lower bound for the probability + * @param upperBound The upper bound for the probability + * @param pathFormula The child node + */ + ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula& pathFormula) { + this->lower = lowerBound; + this->upper = upperBound; + this->pathFormula = &pathFormula; + } + + /*! + * Destructor + * + * The subtree is deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~ProbabilisticIntervalOperator() { + if (pathFormula != NULL) { + delete pathFormula; + } + } + + /*! + * @returns the child node (representation of a PCTL path formula) + */ + const PCTLPathFormula& getPathFormula () const { + return *pathFormula; + } + + /*! + * @returns the lower bound for the probability + */ + const T& getLowerBound() const { + return lower; + } + + /*! + * @returns the upper bound for the probability + */ + const T& getUpperBound() const { + return upper; + } + + /*! + * Sets the child node + * + * @param pathFormula the path formula that becomes the new child node + */ + void setPathFormula(PCTLPathFormula* pathFormula) { + this->pathFormula = pathFormula; + } + + /*! + * Sets the interval in which the probability that the path formula holds may lie in. + * + * @param lowerBound The lower bound for the probability + * @param upperBound The upper bound for the probability + */ + void setInterval(T lowerBound, T upperBound) { + this->lower = lowerBound; + this->upper = upperBound; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() const { + std::string result = "("; + result += " P["; + result += lower; + result += ";"; + result += upper; + result += "] "; + result += pathFormula->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() const { + ProbabilisticIntervalOperator* result = new ProbabilisticIntervalOperator(); + result->setInterval(lower, upper); + if (pathFormula != NULL) { + result->setPathFormula(pathFormula->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 mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + return modelChecker.checkProbabilisticIntervalOperator(this); + } + +private: + T lower; + T upper; + PCTLPathFormula* pathFormula; +}; + +} //namespace formula + +} //namespace mrmc + +#endif /* PROBABILISTICINTERVALOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 49e6530de..0e3876237 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -1,7 +1,7 @@ /* * ProbabilisticOperator.h * - * Created on: 19.10.2012 + * Created on: 07.12.2012 * Author: Thomas Heinemann */ @@ -9,53 +9,54 @@ #define PROBABILISTICOPERATOR_H_ #include "PCTLStateFormula.h" -#include "PCTLPathFormula.h" -#include "utility/const_templates.h" namespace mrmc { - namespace formula { /*! * @brief - * Class for a PCTL formula tree with a P (probablistic) operator node as root. + * Class for a PCTL formula tree with a P (probablistic) operator node over a single real valued + * probability as root. + * + * If the probability interval consist just of one single value (i.e. it is [x,x] for some + * real number x), the class ProbabilisticOperator should be used instead. + * * * Has one PCTL 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 formula holds iff the probability that the path formula holds is equal to the probablility + * 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 PCTLStateFormula * @see PCTLPathFormula + * @see ProbabilisticOperator * @see PCTLFormula */ template -class ProbabilisticOperator : public PCTLStateFormula { - +class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula { public: /*! * Empty constructor */ ProbabilisticOperator() { - upper = mrmc::utility::constGetZero(upper); - lower = mrmc::utility::constGetZero(lower); - pathFormula = NULL; + // TODO Auto-generated constructor stub + } /*! * Constructor * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability - * @param pathFormula The child node (can be omitted, is then set to NULL) + * @param bound The expected value for path formulas + * @param pathFormula The child node */ - ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) { - this->lower = lowerBound; - this->upper = upperBound; - this->pathFormula = pathFormula; + ProbabilisticOperator(T bound, PCTLPathFormula& pathFormula) { + this->bound = bound; + this->pathFormula = &pathFormula; } /*! @@ -65,9 +66,7 @@ public: * (this behavior can be prevented by setting them to NULL before deletion) */ virtual ~ProbabilisticOperator() { - if (pathFormula != NULL) { - delete pathFormula; - } + // TODO Auto-generated destructor stub } /*! @@ -81,14 +80,7 @@ public: * @returns the lower bound for the probability */ const T& getLowerBound() const { - return lower; - } - - /*! - * @returns the upper bound for the probability - */ - const T& getUpperBound() const { - return upper; + return bound; } /*! @@ -101,29 +93,12 @@ public: } /*! - * Sets the interval in which the probability that the path formula holds may lie. + * Sets the expected probability that the path formula holds. * - * @param lowerBound The lower bound for the probability - * @param upperBound The upper bound for the probability + * @param bound The bound for the probability */ - void setInterval(T lowerBound, T upperBound) { - this->lower = lowerBound; - this->upper = upperBound; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() const { - std::string result = "("; - result += " P["; - result += lower; - result += ";"; - result += upper; - result += "] "; - result += pathFormula->toString(); - result += ")"; - return result; + void setInterval(T bound) { + this->bound = bound; } /*! @@ -131,11 +106,11 @@ public: * * 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. + * @returns a new ProbabilisticOperator-object that is identical to the called object. */ virtual PCTLStateFormula* clone() const { ProbabilisticOperator* result = new ProbabilisticOperator(); - result->setInterval(lower, upper); + result->setBound(bound); if (pathFormula != NULL) { result->setPathFormula(pathFormula->clone()); } @@ -146,23 +121,22 @@ public: * 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 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. + * @returns A bit vector indicating all states that satisfy the formula represented by the + * called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual mrmc::storage::BitVector *check( + const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkProbabilisticOperator(this); } private: - T lower; - T upper; + T bound; PCTLPathFormula* pathFormula; }; -} //namespace formula - -} //namespace mrmc - +} /* namespace formula */ +} /* namespace mrmc */ #endif /* PROBABILISTICOPERATOR_H_ */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index fcfb83cce..ba1b098c0 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -26,14 +26,7 @@ class DtmcPrctlModelChecker; #include "src/formula/PCTLPathFormula.h" #include "src/formula/PCTLStateFormula.h" -#include "src/formula/And.h" -#include "src/formula/AP.h" -#include "src/formula/BoundedUntil.h" -#include "src/formula/Next.h" -#include "src/formula/Not.h" -#include "src/formula/Or.h" -#include "src/formula/ProbabilisticOperator.h" -#include "src/formula/Until.h" +#include "src/formula/Formulas.h" #include "src/models/Dtmc.h" #include "src/storage/BitVector.h" @@ -163,12 +156,24 @@ public: } /*! - * The check method for a state formula with a probabilistic operator node as root in its formula tree + * The check method for a state formula with a probabilistic operator node as root in its + * formula tree * * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const = 0; + virtual mrmc::storage::BitVector* checkProbabilisticOperator( + const mrmc::formula::ProbabilisticOperator& formula) const = 0; + + /*! + * The check method for a state formula with a probabilistic interval operator node as root in + * its formula tree + * + * @param formula The state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector* checkProbabilisticIntervalOperator( + const mrmc::formula::ProbabilisticIntervalOperator& formula) const = 0; /*! * The check method for a path formula; Will infer the actual type of formula and delegate it diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 696a86c1e..9192b7886 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -37,7 +37,7 @@ public: virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator& formula) const { + virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticIntervalOperator& formula) const { std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates());