From f5d220535202569793eef39f01c550b22521fe35 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 08:51:56 +0100 Subject: [PATCH 1/7] - Removed enum to infer the correct formula (sub-)class, instead used "check" which calls the correct check function in the model checker. - The dot output was modified to work with the refactored names - Also, it uses now filestreams instead of C style output - and the iterators from the matrix class - Included new (stub) test case for output (and general parsing) --- src/formula/AP.h | 62 ++++++++++- src/formula/And.h | 110 ++++++++++++++++-- src/formula/BoundedUntil.h | 124 ++++++++++++++++++--- src/formula/Next.h | 85 ++++++++++++-- src/formula/Not.h | 82 ++++++++++++-- src/formula/Or.h | 109 ++++++++++++++++-- src/formula/PCTLPathFormula.h | 42 ++++++- src/formula/PCTLStateFormula.h | 43 ++++++- src/formula/PCTLformula.h | 17 +++ src/formula/ProbabilisticOperator.h | 106 ++++++++++++++++-- src/formula/Until.h | 108 ++++++++++++++++-- src/formula/formulaTypes.h | 27 ----- src/modelChecker/DtmcPrctlModelChecker.cpp | 4 +- src/modelChecker/DtmcPrctlModelChecker.h | 65 +++++------ src/models/AtomicPropositionsLabeling.h | 20 ++++ src/models/Dtmc.h | 7 ++ src/parser/parser.cpp | 4 +- src/parser/readPrctlFile.cpp | 4 +- src/parser/readPrctlFile.h | 2 +- src/utility/utility.cpp | 79 ++++++------- src/utility/utility.h | 2 +- test/parser/parse_dtmc_test.cpp | 24 ++++ test/parser/read_tra_file_test.cpp | 4 +- 23 files changed, 922 insertions(+), 208 deletions(-) delete mode 100644 src/formula/formulaTypes.h create mode 100644 test/parser/parse_dtmc_test.cpp diff --git a/src/formula/AP.h b/src/formula/AP.h index 6305dfebf..9113c5bbd 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -14,28 +14,82 @@ namespace mrmc { namespace formula { -class AP : public PCTLStateFormula { +/*! + * Class for a PCTL formula tree with atomic proposition as root. + * This class represents the leaves in the formula tree. + * + * @see PCTLStateFormula + * @see PCTLFormula + */ +template +class AP : public PCTLStateFormula { private: std::string ap; public: + /*! + * Constructor + * + * Creates a new atomic proposition leaf, with the label AP + * + * @param ap The string representing the atomic proposition + */ AP(std::string ap) { this->ap = ap; } + /*! + * Constructor + * + * Creates a new atomic proposition leaf, with the label AP + * + * @param ap The string representing the atomic proposition + */ AP(char* ap) { + //TODO: Does that really work? this->ap = ap; } + /*! + * Destructor. + * At this time, empty... + */ + virtual ~AP() { } + + /*! + * @returns the name of the atomic proposition + */ std::string getAP() { return ap; } - std::string toString() { + /*! + * @returns a string representation of the leaf. + * + */ + virtual std::string toString() { return getAP(); } - virtual enum stateFormulaTypes type() { - return stateFormulaTypes::AP; + /*! + * Clones the called object. + * + * @returns a new AP-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() { + return new AP(ap); + } + + /*! + * 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkAP(this); } }; diff --git a/src/formula/And.h b/src/formula/And.h index 9d09c526e..025ac2f6e 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -15,37 +15,97 @@ namespace mrmc { namespace formula { -class And : public PCTLStateFormula { +/*! + * Class for a PCTL formula tree with AND node as root. + * Has two PCTL 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 PCTLStateFormula + * @see PCTLFormula + */ +template +class And : public PCTLStateFormula { private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PCTLStateFormula* left; + PCTLStateFormula* right; public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ And() { left = NULL; right = NULL; } - And(PCTLStateFormula* left, PCTLStateFormula* right) { + + /*! + * Constructor. + * Creates an AND note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + And(PCTLStateFormula* left, PCTLStateFormula* right) { this->left = left; this->right = right; } - void setLeft(PCTLStateFormula* newLeft) { + /*! + * Destructor. + * + * The subtrees are deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~And() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { left = newLeft; } - void setRight(PCTLStateFormula* newRight) { + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { right = newRight; } - PCTLStateFormula* getLeft() { + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { return left; } - PCTLStateFormula* getRight() { + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { return right; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "("; result += left->toString(); result += " && "; @@ -54,9 +114,37 @@ class And : public PCTLStateFormula { return result; } - virtual enum stateFormulaTypes type() { - return AND; + /*! + * 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() { + And* result = new And(); + if (this->left != NULL) { + result->setLeft(left->clone()); + } + if (this->right != NULL) { + result->setRight(right->clone()); + } + return result; } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkAnd(this); + } + }; } //namespace formula diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 425e5afaf..dc7640e95 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -11,68 +11,164 @@ #include "PCTLPathFormula.h" #include "PCTLStateFormula.h" #include "boost/integer/integer_mask.hpp" +#include "boost/lexical_cast.hpp" +#include namespace mrmc { namespace formula { -class BoundedUntil : public PCTLPathFormula { - PCTLStateFormula* left; - PCTLStateFormula* right; +/*! + * Class for a PCTL (path) formula tree with a BoundedUntil node as root. + * Has two PCTL state formulas as sub formulas/trees. + * + * \par Semantics + * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before, + * \e left holds. + * + * The subtrees are seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see PCTLPathFormula + * @see PCTLFormula + */ +template +class BoundedUntil : public PCTLPathFormula { + PCTLStateFormula* left; + PCTLStateFormula* right; uint_fast64_t bound; public: + /*! + * Empty constructor + */ BoundedUntil() { this->left = NULL; this->right = NULL; bound = 0; } - BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right, + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + * @param bound The maximal number of steps + */ + BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right, uint_fast64_t bound) { this->left = left; - this->right = right; + this->right = right;; this->bound = bound; } - virtual ~BoundedUntil(); + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~BoundedUntil() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } - void setLeft(PCTLStateFormula* newLeft) { + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { left = newLeft; } - void setRight(PCTLStateFormula* newRight) { + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { right = newRight; } - PCTLStateFormula* getLeft() { + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { return left; } - PCTLStateFormula* getRight() { + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { return right; } + /*! + * @returns the maximally allowed number of steps for the bounded until operator + */ uint_fast64_t getBound() { return bound; } + /*! + * Sets the maximally allowed number of steps for the bounded until operator + * + * @param bound the new bound. + */ void setBound(uint_fast64_t bound) { this->bound = bound; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "("; result += left->toString(); result += " U<="; - result += std::to_string(bound); + result += boost::lexical_cast(bound); result += " "; result += right->toString(); result += ")"; return result; } - virtual enum pathFormulaTypes type() { - return BOUNDED_UNTIL; + /*! + * 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 PCTLPathFormula* clone() { + BoundedUntil* result = new BoundedUntil(); + result->setBound(bound); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkBoundedUntil(this); } }; diff --git a/src/formula/Next.h b/src/formula/Next.h index 2fa5e1d02..5a243b5f1 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -15,28 +15,71 @@ namespace mrmc { namespace formula { - -class Next : public PCTLPathFormula { +/*! + * Class for a PCTL (path) formula tree with a Next node as root. + * Has two PCTL 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 PCTLPathFormula + * @see PCTLFormula + */ +template +class Next : public PCTLPathFormula { private: - PCTLStateFormula* child; + PCTLStateFormula* child; public: + /*! + * Empty constructor + */ Next() { this->child = NULL; } - Next(PCTLStateFormula* child) { + /*! + * Constructor + * + * @param child The child node + */ + Next(PCTLStateFormula* child) { this->child = child; } - PCTLStateFormula* getChild() { + /*! + * Constructor. + * + * Also deletes the subtree. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Next() { + if (child != NULL) { + delete child; + } + } + + /*! + * @returns the child node + */ + PCTLStateFormula* getChild() { return child; } - void setChild(PCTLStateFormula* child) { + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(PCTLStateFormula* child) { this->child = child; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "("; result += " X "; result += child->toString(); @@ -44,8 +87,32 @@ class Next : public PCTLPathFormula { return result; } - virtual enum pathFormulaTypes type() { - return NEXT; + /*! + * 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 PCTLPathFormula* clone() { + Next* result = new Next(); + if (child != NULL) { + result->setChild(child); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkNext(this); } }; diff --git a/src/formula/Not.h b/src/formula/Not.h index 36993c18a..52a9311aa 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -8,44 +8,104 @@ #ifndef NOT_H_ #define NOT_H_ +#include "PCTLStateFormula.h" + namespace mrmc { namespace formula { -#include "PCTLStateFormula.h" - -class Not : public PCTLStateFormula { +/*! + * Class for a PCTL formula tree with NOT node as root. + * Has one PCTL state formula as sub formula/tree. + * + * The subtree is seen as part of the object and deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + * + * @see PCTLStateFormula + * @see PCTLFormula + */ +template +class Not : public PCTLStateFormula { private: - PCTLStateFormula* child; + PCTLStateFormula* child; public: + /*! + * Empty constructor + */ Not() { this->child = NULL; } - Not(PCTLStateFormula* child) { + /*! + * Constructor + * @param child The child node + */ + Not(PCTLStateFormula* child) { this->child = child; } + /*! + * Destructor + * + * Also deletes the subtree + * (this behavior can be prevented by setting them to NULL before deletion) + */ virtual ~Not() { - + if (child != NULL) { + delete child; + } } - PCTLStateFormula* getChild() { + /*! + * @returns The child node + */ + PCTLStateFormula* getChild() { return child; } - void setChild(PCTLStateFormula* child) { + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(PCTLStateFormula* child) { this->child = child; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "!"; result += child->toString(); return result; } - virtual enum stateFormulaTypes type() { - return NOT; + /*! + * 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() { + Not* result = new Not(); + if (child != NULL) { + result->setChild(child); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkNot(this); } }; diff --git a/src/formula/Or.h b/src/formula/Or.h index 6559d36aa..94c01ba29 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -14,37 +14,97 @@ namespace mrmc { namespace formula { -class Or : public PCTLStateFormula { +/*! + * Class for a PCTL formula tree with OR node as root. + * Has two PCTL 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 PCTLStateFormula + * @see PCTLFormula + */ +template +class Or : public PCTLStateFormula { private: - PCTLStateFormula* left; - PCTLStateFormula* right; + PCTLStateFormula* left; + PCTLStateFormula* right; public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ Or() { left = NULL; right = NULL; } - Or(PCTLStateFormula* left, PCTLStateFormula* right) { + + /*! + * Constructor. + * Creates an AND note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + Or(PCTLStateFormula* left, PCTLStateFormula* right) { this->left = left; this->right = right; } - void setLeft(PCTLStateFormula* newLeft) { + /*! + * Destructor. + * + * The subtrees are deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Or() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { left = newLeft; } - void setRight(PCTLStateFormula* newRight) { + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { right = newRight; } - PCTLStateFormula* getLeft() { + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { return left; } - PCTLStateFormula* getRight() { + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { return right; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "("; result += left->toString(); result += " || "; @@ -53,8 +113,35 @@ class Or : public PCTLStateFormula { return result; } - virtual enum stateFormulaTypes type() { - return OR; + /*! + * 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() { + Or* result = new Or(); + if (this->left != NULL) { + result->setLeft(left->clone()); + } + if (this->right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkOr(this); } }; diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h index 7114caca9..cebc3d15f 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PCTLPathFormula.h @@ -9,16 +9,50 @@ #define PCTLPATHFORMULA_H_ #include "PCTLformula.h" -#include "formulaTypes.h" +#include "modelChecker/DtmcPrctlModelChecker.h" +#include namespace mrmc { namespace formula { -//abstract -class PCTLPathFormula : public PCTLFormula { +/*! + * Abstract base class for PCTL path formulas. + * @attention This class is abstract. + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method + * clone(). + */ +template +class PCTLPathFormula : public PCTLFormula { public: - virtual enum pathFormulaTypes type() = 0; + /*! + * empty destructor + */ + virtual ~PCTLPathFormula() { } + + /*! + * 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 PCTLPathFormula* clone() = 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; }; } //namespace formula diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h index 3361a11a4..67ed9a899 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PCTLStateFormula.h @@ -9,17 +9,50 @@ #define PCTLSTATEFORMULA_H_ #include "PCTLformula.h" -#include "formulaTypes.h" +#include "storage/BitVector.h" +#include "modelChecker/DtmcPrctlModelChecker.h" namespace mrmc { namespace formula { -//abstract -class PCTLStateFormula : public PCTLFormula { +/*! + * Abstract base class for PCTL state formulas. + * @attention This class is abstract. + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method + * clone(). + */ +template +class PCTLStateFormula : public PCTLFormula { public: - virtual enum stateFormulaTypes type() = 0; - + /*! + * empty destructor + */ + virtual ~PCTLStateFormula() { } + + /*! + * 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 PCTLStateFormula* clone() = 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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; }; } //namespace formula diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h index 996416a2c..60f361f25 100644 --- a/src/formula/PCTLformula.h +++ b/src/formula/PCTLformula.h @@ -16,8 +16,25 @@ namespace formula { //abstract +/*! + * Abstract base class for PCTL formulas in general. + * @attention This class is abstract. + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes + * PCTLPathFormula and PCTLStateFormula offer the method clone(). + */ +template class PCTLFormula { public: + /*! + * virtual destructor + */ + virtual ~PCTLFormula() { } + + /*! + * @note This function is not implemented in this class. + * @returns a string representation of the formula + */ virtual std::string toString() = 0; }; diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index bd83a1431..4d71e0be6 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -9,49 +9,112 @@ #define PROBABILISTICOPERATOR_H_ #include "PCTLStateFormula.h" +#include "PCTLPathFormula.h" +#include "misc/const_templates.h" namespace mrmc { namespace formula { +/*! + * Class for a PCTL formula tree with a P (probablistic) operator node as root. + * 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 PCTLFormula + */ template -class ProbabilisticOperator : public PCTLStateFormula { +class ProbabilisticOperator : public PCTLStateFormula { T lower; T upper; - PCTLPathFormula* pathFormula; + PCTLPathFormula* pathFormula; public: - ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) { + /*! + * Empty constructor + */ + ProbabilisticOperator() { + upper = mrmc::misc::constGetZero(&upper); + lower = mrmc::misc::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 (can be omitted, is then set to NULL) + */ + ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) { 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 ~ProbabilisticOperator() { - delete pathFormula; + if (pathFormula != NULL) { + delete pathFormula; + } } - PCTLPathFormula* getPathFormula () { + /*! + * @returns the child node (representation of a PCTL path formula) + */ + PCTLPathFormula* getPathFormula () { return pathFormula; } + /*! + * @returns the lower bound for the probability + */ T getLowerBound() { return lower; } + /*! + * @returns the upper bound for the probability + */ T getUpperBound() { return upper; } - void setPathFormula(PCTLPathFormula* pathFormula) { + /*! + * 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. + * + * @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; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "("; result += " P["; result += lower; @@ -63,8 +126,33 @@ class ProbabilisticOperator : public PCTLStateFormula { return result; } - virtual enum stateFormulaTypes type() { - return PROBABILISTIC; + /*! + * 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() { + ProbabilisticOperator* result = new ProbabilisticOperator(); + 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkProbabilisticOperator(this); } }; diff --git a/src/formula/Until.h b/src/formula/Until.h index d12f6ed78..8da6d0928 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -15,38 +15,95 @@ namespace mrmc { namespace formula { -class Until : public PCTLPathFormula { - PCTLStateFormula* left; - PCTLStateFormula* right; +/*! + * Class for a PCTL (path) formula tree with a BoundedUntil node as root. + * Has two PCTL 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 PCTLPathFormula + * @see PCTLFormula + */ +template +class Until : public PCTLPathFormula { + PCTLStateFormula* left; + PCTLStateFormula* right; public: + /*! + * Empty constructor + */ Until() { this->left = NULL; this->right = NULL; } - Until(PCTLStateFormula* left, PCTLStateFormula* right) { + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + */ + Until(PCTLStateFormula* left, PCTLStateFormula* right) { this->left = left; this->right = right; } - virtual ~Until(); - void setLeft(PCTLStateFormula* newLeft) { + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Until() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { left = newLeft; } - void setRight(PCTLStateFormula* newRight) { + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { right = newRight; } - PCTLStateFormula* getLeft() { + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { return left; } - PCTLStateFormula* getRight() { + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { return right; } - std::string toString() { + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { std::string result = "("; result += left->toString(); result += " U "; @@ -55,8 +112,35 @@ class Until : public PCTLPathFormula { return result; } - virtual enum pathFormulaTypes type() { - return UNTIL; + /*! + * 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 PCTLPathFormula* clone() { + Until* result = new Until(); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkUntil(this); } }; diff --git a/src/formula/formulaTypes.h b/src/formula/formulaTypes.h deleted file mode 100644 index 41f245fa3..000000000 --- a/src/formula/formulaTypes.h +++ /dev/null @@ -1,27 +0,0 @@ -/* - * formulaTypes.h - * - * Created on: 21.10.2012 - * Author: Thomas Heinemann - */ - -#ifndef FORMULATYPES_H_ -#define FORMULATYPES_H_ - -enum stateFormulaTypes { - AND, - AP, - NOT, - OR, - PROBABILISTIC -}; - -enum pathFormulaTypes { - NEXT, - UNTIL, - BOUNDED_UNTIL, - EVENTUALLY, - ALWAYS -}; - -#endif /* FORMULATYPES_H_ */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp index d308005cf..2af9ee50d 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.cpp +++ b/src/modelChecker/DtmcPrctlModelChecker.cpp @@ -12,8 +12,8 @@ namespace mrmc { namespace modelChecker { template -DtmcPrctlModelChecker::DtmcPrctlModelChecker(mrmc::models::Dtmc* DTMC) { - this->DTMC = DTMC; +DtmcPrctlModelChecker::DtmcPrctlModelChecker(mrmc::models::Dtmc* dtmc) { + this->dtmc = dtmc; } template diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 9a7a7be01..ddb4b1f9b 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -8,6 +8,24 @@ #ifndef DTMCPRCTLMODELCHECKER_H_ #define DTMCPRCTLMODELCHECKER_H_ +namespace mrmc { + +namespace modelChecker { + +/* The formula classes need to reference a model checker for the check function, + * which is used to infer the correct type of formula, + * so the model checker class is declared here already. + * + */ +template +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" @@ -37,53 +55,30 @@ class DtmcPrctlModelChecker { public: explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* DTMC); - ~DtmcPrctlModelChecker(); + virtual ~DtmcPrctlModelChecker(); virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0; virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0; virtual std::vector multiplyMatrixVector(std::vector*) = 0; - virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) { - if (formula->type() == AND) { - return checkAnd(static_cast(formula)); - } - if (formula->type() == stateFormulaTypes::AP) { - return checkAP(static_cast(formula)); - } - if (formula->type() == NOT) { - return checkNot(static_cast(formula)); - } - if (formula->type() == OR) { - return checkOr(static_cast(formula)); - } - if (formula->type() == PROBABILISTIC) { - return checkProbabilisticOperator( - static_cast*>(formula)); - } + virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) { + return formula->check(this); } - virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And*) = 0; - virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0; - virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0; - virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0; + virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And*) = 0; + virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0; + virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0; + virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0; virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator*) = 0; - virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula* formula) { - if (formula->type() == NEXT) { - return checkNext(static_cast(formula)); - } - if (formula->type() == UNTIL) { - return checkUntil(static_cast(formula)); - } - if (formula->type() == BOUNDED_UNTIL) { - return checkBoundedUntil(static_cast(formula)); - } + virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula* formula) { + return formula->check(this); } - virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0; - virtual std::vector checkNext(mrmc::formula::Next*) = 0; - virtual std::vector checkUntil(mrmc::formula::Until*) = 0; + virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0; + virtual std::vector checkNext(mrmc::formula::Next*) = 0; + virtual std::vector checkUntil(mrmc::formula::Until*) = 0; }; } //namespace modelChecker diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 2f051cf9b..0ed215a86 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -133,6 +133,26 @@ public: this->singleLabelings[nameToLabelingMap[ap]]->set(state, true); } + /*! + * Creates a list of atomic propositions for a given state + * @param state The index of a state + * @returns The list of propositions for the given state + */ + std::set getPropositionsForState(uint_fast32_t state) { + if (state >= stateCount) { + throw std::out_of_range("State index out of range."); + } + std::set result; + for (auto it = nameToLabelingMap.begin(); + it != nameToLabelingMap.end(); + it++) { + if (stateHasAtomicProposition(it->first, state)) { + result.insert(it->first); + } + } + return result; + } + /*! * Checks whether a given state is labeled with the given atomic proposition. * @param ap The name of the atomic proposition. diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 6edd0272e..80c1eb18f 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -106,6 +106,13 @@ public: return this->probabilityMatrix; } + /*! + * + */ + std::set getPropositionsForState(uint_fast32_t state) { + return stateLabeling->getPropositionsForState(state - 1); + } + /*! * Retrieves a reference to the backwards transition relation. * @return A reference to the backwards transition relation. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5c776a316..403ff6fd9 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -7,9 +7,9 @@ #include #include -#if defined MACOSX +//#if defined MACOSX #include -#endif +//#endif #include #include #include diff --git a/src/parser/readPrctlFile.cpp b/src/parser/readPrctlFile.cpp index 40aa6deb4..8e7d216b9 100644 --- a/src/parser/readPrctlFile.cpp +++ b/src/parser/readPrctlFile.cpp @@ -61,7 +61,7 @@ namespace /*! * @brief Resulting formula. */ - mrmc::formula::PCTLFormula* result; + mrmc::formula::PCTLFormula* result; struct dump { @@ -106,7 +106,7 @@ namespace }; } -mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename) +mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename) { PRCTLParser p; mrmc::parser::MappedFile file(filename); diff --git a/src/parser/readPrctlFile.h b/src/parser/readPrctlFile.h index 80393482d..7a4bc1a5b 100644 --- a/src/parser/readPrctlFile.h +++ b/src/parser/readPrctlFile.h @@ -9,7 +9,7 @@ namespace parser { /*! * @brief Load PRCTL file */ -mrmc::formula::PCTLFormula* readPrctlFile(const char * filename); +mrmc::formula::PCTLFormula* readPrctlFile(const char * filename); } // namespace parser } // namespace mrmc diff --git a/src/utility/utility.cpp b/src/utility/utility.cpp index 783ee9120..515fe925e 100644 --- a/src/utility/utility.cpp +++ b/src/utility/utility.cpp @@ -9,70 +9,57 @@ #include "src/parser/readTraFile.h" #include "src/parser/readLabFile.h" +#include + namespace mrmc { namespace utility { -void dtmcToDot(mrmc::models::Dtmc* dtmc, const char* filename) { - //FIXME: adapt this to the refactored names - //FIXME: use C++-style for file output here, as performance is not critical here -/* FILE *P; - mrmc::sparse::StaticSparseMatrix* matrix = dtmc->getTransitions(); - mrmc::dtmc::Labeling* labels = dtmc->getLabels(); - - uint_fast64_t* row_indications = matrix->getRowIndications(); - uint_fast64_t* column_indications = matrix->getColumnIndications(); - double* value_storage = matrix->getStoragePointer(); - double* diagonal_storage = matrix->getDiagonalStorage(); +void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { + mrmc::storage::SquareSparseMatrix* matrix = dtmc->getTransitionProbabilityMatrix(); + double* diagonal_storage = matrix->getDiagonalStoragePointer(); - P = fopen(filename, "w"); + std::ofstream file; + file.open(filename); - if (P == NULL) { - pantheios::log_ERROR("File could not be opened."); - throw mrmc::exceptions::file_IO_exception(); - } - - fprintf(P, "digraph dtmc {\n"); + file << "digraph dtmc {\n"; //Specify the nodes and their labels - for (uint_fast64_t i = 1; i <= dtmc->getNodeCount(); i++) { - fprintf(P, "\t%Lu[label=\"%Lu\\n{", i, i); + for (uint_fast64_t i = 1; i <= dtmc->getNumberOfStates(); i++) { + file << "\t" << i << "[label=\"" << i << "\\n{"; char komma=' '; - for(auto it = labels->getPropositionMap()->begin(); - it != labels->getPropositionMap()->end(); + std::set propositions = dtmc->getPropositionsForState(i); + for(auto it = propositions.begin(); + it != propositions.end(); it++) { - if(labels->nodeHasProposition(it->first, i)) { - fprintf(P, "%c%s", komma, (it->first).c_str()); - } - char komma=','; + file << komma << *it; + komma=','; } - fprintf(P, " }\"];\n"); - } + file << " }\"];\n"; - uint_fast64_t row = 0; - - for (uint_fast64_t i = 0; i < matrix->getNonZeroEntryCount(); i++ ) { - //Check whether we have to switch to the new row - while (row_indications[row] <= i) { - ++row; - //write diagonal entry/self loop first - if (diagonal_storage[row] != 0) { - fprintf(P, "\t%Lu -> %Lu [label=%f]\n", - row, row, diagonal_storage[row]); - } - } - fprintf(P, "\t%Lu -> %Lu [label=%f]\n", - row, column_indications[i], value_storage[i]); } + for (uint_fast64_t row = 0; row < dtmc->getNumberOfStates(); row++ ) { + //write diagonal entry/self loop first + if (diagonal_storage[row] != 0) { + file << "\t" << row << " -> " << row << " [label=" << diagonal_storage[row] <<"]\n"; + } + //Then, iterate through the row and write each non-diagonal value into the file + for ( auto it = matrix->beginConstColumnNoDiagIterator(row); + it != matrix->endConstColumnNoDiagIterator(row); + it++) { + double value = 0; + matrix->getValue(row,*it,&value); + file << "\t" << row << " -> " << *it << " [label=" << value << "]\n"; + } + } - - fprintf(P, "}\n"); - - fclose(P); */ + file << "}\n"; + file.close(); } +//TODO: Should this stay here or be integrated in the new parser structure? mrmc::models::Dtmc* parseDTMC(const char* tra_file, const char* lab_file) { mrmc::parser::TraParser tp(tra_file); uint_fast64_t node_count = tp.getMatrix()->getRowCount(); diff --git a/src/utility/utility.h b/src/utility/utility.h index 65eb9113f..ebfa964b7 100644 --- a/src/utility/utility.h +++ b/src/utility/utility.h @@ -25,7 +25,7 @@ namespace utility { it will be overwritten. */ -void dtmcToDot(mrmc::models::Dtmc* dtmc, const char* filename); +void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename); /*! Parses a transition file and a labeling file and produces a DTMC out of them. diff --git a/test/parser/parse_dtmc_test.cpp b/test/parser/parse_dtmc_test.cpp new file mode 100644 index 000000000..e89ec331e --- /dev/null +++ b/test/parser/parse_dtmc_test.cpp @@ -0,0 +1,24 @@ +/* + * parse_dtmc_test.cpp + * + * Created on: 03.12.2012 + * Author: Thomas Heinemann + */ + + +#include "gtest/gtest.h" +#include "mrmc-config.h" +#include "src/utility/utility.h" + +TEST(ParseDtmcTest, parseAndOutput) { + mrmc::models::Dtmc* myDtmc; + ASSERT_NO_THROW(myDtmc = mrmc::utility::parseDTMC( + MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra", + MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); + + ASSERT_NO_THROW(mrmc::utility::dtmcToDot(myDtmc, MRMC_CPP_TESTS_BASE_PATH "/parser/output.dot")); + + delete myDtmc; +} + + diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp index 9aad2b927..d8cf64c8e 100644 --- a/test/parser/read_tra_file_test.cpp +++ b/test/parser/read_tra_file_test.cpp @@ -12,6 +12,8 @@ #include "src/exceptions/file_IO_exception.h" #include "src/exceptions/wrong_file_format.h" +#include "src/utility/utility.h" + TEST(ReadTraFileTest, NonExistingFileTest) { //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-) ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception); @@ -61,8 +63,6 @@ TEST(ReadTraFileTest, ParseFileTest1) { ASSERT_TRUE(result->getValue(4,4,&val)); ASSERT_EQ(val,0); - // FIXME: adapt this test case to the new dot-output routines - /* result->toDOTFile("output.dot"); */ delete result; delete parser; } else { From a1854b26a5befcd1b3894728becee4cbd0188881 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 10:18:39 +0100 Subject: [PATCH 2/7] Documentation of ModelChecker (new) and improved doc of formula classes --- src/formula/AP.h | 2 + src/formula/And.h | 2 + src/formula/BoundedUntil.h | 4 +- src/formula/Next.h | 4 +- src/formula/Not.h | 2 + src/formula/Or.h | 2 + src/formula/PCTLPathFormula.h | 4 +- src/formula/PCTLStateFormula.h | 2 + src/formula/PCTLformula.h | 2 + src/formula/ProbabilisticOperator.h | 4 +- src/formula/Until.h | 6 +- src/modelChecker/DtmcPrctlModelChecker.h | 118 +++++++++++++++++++++-- 12 files changed, 140 insertions(+), 12 deletions(-) diff --git a/src/formula/AP.h b/src/formula/AP.h index 9113c5bbd..00a3e8734 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -15,7 +15,9 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL formula tree with atomic proposition as root. + * * This class represents the leaves in the formula tree. * * @see PCTLStateFormula diff --git a/src/formula/And.h b/src/formula/And.h index 025ac2f6e..8a1cd9696 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -16,7 +16,9 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL formula tree with AND node as root. + * * Has two PCTL state formulas as sub formulas/trees. * * As AND is commutative, the order is \e theoretically not important, but will influence the order in which diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index dc7640e95..3e48dc132 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -19,10 +19,12 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL (path) formula tree with a BoundedUntil node as root. + * * Has two PCTL state formulas as sub formulas/trees. * - * \par Semantics + * @par Semantics * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before, * \e left holds. * diff --git a/src/formula/Next.h b/src/formula/Next.h index 5a243b5f1..6000366ff 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -16,10 +16,12 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL (path) formula tree with a Next node as root. + * * Has two PCTL state formulas as sub formulas/trees. * - * \par Semantics + * @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 diff --git a/src/formula/Not.h b/src/formula/Not.h index 52a9311aa..59f100f70 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -15,7 +15,9 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL formula tree with NOT node as root. + * * Has one PCTL state formula as sub formula/tree. * * The subtree is seen as part of the object and deleted with the object diff --git a/src/formula/Or.h b/src/formula/Or.h index 94c01ba29..a5cdbc659 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -15,7 +15,9 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL formula tree with OR node as root. + * * Has two PCTL state formulas as sub formulas/trees. * * As OR is commutative, the order is \e theoretically not important, but will influence the order in which diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h index cebc3d15f..70255f8b3 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PCTLPathFormula.h @@ -17,9 +17,11 @@ namespace mrmc { namespace formula { /*! + * @brief * Abstract base class for PCTL path formulas. + * * @attention This class is abstract. - * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method * clone(). */ diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h index 67ed9a899..de8d0e117 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PCTLStateFormula.h @@ -17,7 +17,9 @@ namespace mrmc { namespace formula { /*! + * @brief * Abstract base class for PCTL state formulas. + * * @attention This class is abstract. * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h index 60f361f25..12f51a4ce 100644 --- a/src/formula/PCTLformula.h +++ b/src/formula/PCTLformula.h @@ -17,7 +17,9 @@ namespace formula { //abstract /*! + * @brief * Abstract base class for PCTL formulas in general. + * * @attention This class is abstract. * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so * the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 4d71e0be6..89978f30f 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -17,10 +17,12 @@ namespace mrmc { namespace formula { /*! + * @brief * Class for a PCTL formula tree with a P (probablistic) operator node as root. + * * Has one PCTL path formula as sub formula/tree. * - * \par Semantics + * @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 diff --git a/src/formula/Until.h b/src/formula/Until.h index 8da6d0928..39f361e11 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -16,10 +16,12 @@ namespace mrmc { namespace formula { /*! - * Class for a PCTL (path) formula tree with a BoundedUntil node as root. + * @brief + * Class for a PCTL (path) formula tree with an Until node as root. + * * Has two PCTL state formulas as sub formulas/trees. * - * \par Semantics + * @par Semantics * The formula holds iff eventually, formula \e right (the right subtree) holds, and before, * \e left holds always. * diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index ddb4b1f9b..7c6932ccb 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -43,41 +43,147 @@ namespace mrmc { namespace modelChecker { +/*! + * @brief + * Interface for model checker classes. + * + * This class provides basic functions that are the same for all subclasses, but mainly only declares + * abstract methods that are to be implemented in concrete instances. + * + * @attention This class is abstract. + */ template class DtmcPrctlModelChecker { private: mrmc::models::Dtmc* dtmc; protected: + /*! + * @returns A reference to the dtmc of the model checker. + */ mrmc::models::Dtmc* getDtmc() const { return this->dtmc; } public: + /*! + * Constructor + */ explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* DTMC); - virtual ~DtmcPrctlModelChecker(); - virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0; - virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0; - virtual std::vector multiplyMatrixVector(std::vector*) = 0; + /*! + * Destructor + */ + virtual ~DtmcPrctlModelChecker(); + /*! + * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all + * other edges from these states) + * + * @param states A bit vector representing a set of states that should become absorbing. + */ + virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0; + + /*! + * Returns all states that are labeled with a given atomic proposition. + * + * @param ap A string representing an atomic proposition. + * @returns The set of states labeled with the atomic proposition ap. + */ + virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0; + + /*! + * Multiplies the matrix with a given vector; the result again is a vector. + * + * @param vector The vector to multiply the matrix with. + * @returns The result of multiplying the transition probability matrix with vector. + */ + virtual std::vector multiplyMatrixVector(std::vector* vector) = 0; + + /*! + * The check method for a state formula; Will infer the actual type of formula and delegate it + * to the specialized method + * + * @param formula The state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) { return formula->check(this); } - - virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And*) = 0; + /*! + * The check method for a state formula with an And node as root in its formula tree + * + * @param formula The And formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And* formula) = 0; + + /*! + * The check method for a formula with an AP node as root in its formula tree + * + * @param formula The AP state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0; + + /*! + * The check method for a formula with a Not node as root in its formula tree + * + * @param formula The Not state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0; + + /*! + * The check method for a state formula with an Or node as root in its formula tree + * + * @param formula The Or state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0; + + /*! + * 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(mrmc::formula::ProbabilisticOperator*) = 0; + /*! + * The check method for a path formula; Will infer the actual type of formula and delegate it + * to the specialized method + * + * @param formula The path formula to check + * @returns for each state the probability that the path formula holds. + */ virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula* formula) { return formula->check(this); } + /*! + * The check method for a path formula with a Bounded Until operator node as root in its formula tree + * + * @param formula The Bounded Until path formula to check + * @returns for each state the probability that the path formula holds. + */ virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0; + + /*! + * The check method for a path formula with a Next operator node as root in its formula tree + * + * @param formula The Next path formula to check + * @returns for each state the probability that the path formula holds. + */ virtual std::vector checkNext(mrmc::formula::Next*) = 0; + + /*! + * The check method for a path formula with an Until operator node as root in its formula tree + * + * @param formula The Until path formula to check + * @returns for each state the probability that the path formula holds. + */ virtual std::vector checkUntil(mrmc::formula::Until*) = 0; }; From b726a07b3f30e8865fced488e0b7bfae78379b81 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 10:51:03 +0100 Subject: [PATCH 4/7] Small bugfix for the dot output --- src/models/Dtmc.h | 2 +- src/utility/utility.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 80c1eb18f..8ac46ffee 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -110,7 +110,7 @@ public: * */ std::set getPropositionsForState(uint_fast32_t state) { - return stateLabeling->getPropositionsForState(state - 1); + return stateLabeling->getPropositionsForState(state); } /*! diff --git a/src/utility/utility.cpp b/src/utility/utility.cpp index 515fe925e..e2ef43833 100644 --- a/src/utility/utility.cpp +++ b/src/utility/utility.cpp @@ -25,7 +25,7 @@ void dtmcToDot(mrmc::models::Dtmc* dtmc, std::string filename) { file << "digraph dtmc {\n"; //Specify the nodes and their labels - for (uint_fast64_t i = 1; i <= dtmc->getNumberOfStates(); i++) { + for (uint_fast64_t i = 1; i < dtmc->getNumberOfStates(); i++) { file << "\t" << i << "[label=\"" << i << "\\n{"; char komma=' '; std::set propositions = dtmc->getPropositionsForState(i); From 79761d049256986ac9e8d84df6c67d9e5ff7b283 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 11:18:10 +0100 Subject: [PATCH 5/7] Added copy constructor to model checker --- src/modelChecker/DtmcPrctlModelChecker.cpp | 5 ++++ src/modelChecker/DtmcPrctlModelChecker.h | 30 ++++++++++++++-------- 2 files changed, 24 insertions(+), 11 deletions(-) diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp index 2af9ee50d..f5a884921 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.cpp +++ b/src/modelChecker/DtmcPrctlModelChecker.cpp @@ -21,6 +21,11 @@ DtmcPrctlModelChecker::~DtmcPrctlModelChecker() { delete this->dtmc; } +template +DtmcPrctlModelChecker::DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + this->dtmc = new mrmc::models::Dtmc(modelChecker->getDtmc()); +} + } //namespace modelChecker diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 7c6932ccb..979d8d93d 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -54,28 +54,33 @@ namespace modelChecker { */ template class DtmcPrctlModelChecker { - private: - mrmc::models::Dtmc* dtmc; - - protected: + public: /*! - * @returns A reference to the dtmc of the model checker. + * Constructor + * + * @parameter Dtmc The dtmc model which is checked. */ - mrmc::models::Dtmc* getDtmc() const { - return this->dtmc; - } + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* Dtmc); - public: /*! - * Constructor + * Copy constructor + * + * @parameter modelChecker The model checker that is copied. */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* DTMC); + explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker); /*! * Destructor */ virtual ~DtmcPrctlModelChecker(); + /*! + * @returns A reference to the dtmc of the model checker. + */ + mrmc::models::Dtmc* getDtmc() const { + return this->dtmc; + } + /*! * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all * other edges from these states) @@ -185,6 +190,9 @@ class DtmcPrctlModelChecker { * @returns for each state the probability that the path formula holds. */ virtual std::vector checkUntil(mrmc::formula::Until*) = 0; + + private: + mrmc::models::Dtmc* dtmc; }; } //namespace modelChecker From 350f1a0990bceca198af51a30ddae5ba4b5bb088 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 11:40:54 +0100 Subject: [PATCH 6/7] Code style for formula classes --- src/formula/AP.h | 138 +++++++------- src/formula/And.h | 229 +++++++++++------------ src/formula/BoundedUntil.h | 275 ++++++++++++++-------------- src/formula/Next.h | 170 ++++++++--------- src/formula/Not.h | 164 +++++++++-------- src/formula/Or.h | 230 +++++++++++------------ src/formula/PCTLPathFormula.h | 53 +++--- src/formula/PCTLStateFormula.h | 53 +++--- src/formula/PCTLformula.h | 23 +-- src/formula/ProbabilisticOperator.h | 247 +++++++++++++------------ src/formula/Until.h | 225 ++++++++++++----------- 11 files changed, 914 insertions(+), 893 deletions(-) diff --git a/src/formula/AP.h b/src/formula/AP.h index 00a3e8734..8bda0df06 100644 --- a/src/formula/AP.h +++ b/src/formula/AP.h @@ -25,74 +25,76 @@ namespace formula { */ template class AP : public PCTLStateFormula { - private: - std::string ap; - public: - /*! - * Constructor - * - * Creates a new atomic proposition leaf, with the label AP - * - * @param ap The string representing the atomic proposition - */ - AP(std::string ap) { - this->ap = ap; - } - - /*! - * Constructor - * - * Creates a new atomic proposition leaf, with the label AP - * - * @param ap The string representing the atomic proposition - */ - AP(char* ap) { - //TODO: Does that really work? - this->ap = ap; - } - - /*! - * Destructor. - * At this time, empty... - */ - virtual ~AP() { } - - /*! - * @returns the name of the atomic proposition - */ - std::string getAP() { - return ap; - } - - /*! - * @returns a string representation of the leaf. - * - */ - virtual std::string toString() { - return getAP(); - } - - /*! - * Clones the called object. - * - * @returns a new AP-object that is identical the called object. - */ - virtual PCTLStateFormula* clone() { - return new AP(ap); - } - - /*! - * 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkAP(this); - } + +public: + /*! + * Constructor + * + * Creates a new atomic proposition leaf, with the label AP + * + * @param ap The string representing the atomic proposition + */ + AP(std::string ap) { + this->ap = ap; + } + + /*! + * Constructor + * + * Creates a new atomic proposition leaf, with the label AP + * + * @param ap The string representing the atomic proposition + */ + AP(char* ap) { + //TODO: Does that really work? + this->ap = ap; + } + + /*! + * Destructor. + * At this time, empty... + */ + virtual ~AP() { } + + /*! + * @returns the name of the atomic proposition + */ + std::string getAP() { + return ap; + } + + /*! + * @returns a string representation of the leaf. + * + */ + virtual std::string toString() { + return getAP(); + } + + /*! + * Clones the called object. + * + * @returns a new AP-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() { + return new AP(ap); + } + + /*! + * 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkAP(this); + } + +private: + std::string ap; }; } //namespace formula diff --git a/src/formula/And.h b/src/formula/And.h index 8a1cd9696..16f0b6d8e 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -32,121 +32,122 @@ namespace formula { */ template class And : public PCTLStateFormula { - private: - PCTLStateFormula* left; - PCTLStateFormula* right; - public: - /*! - * Empty constructor. - * Will create an AND-node without subnotes. Will not represent a complete formula! - */ - And() { - left = NULL; - right = NULL; - } - - /*! - * Constructor. - * Creates an AND note with the parameters as subtrees. - * - * @param left The left sub formula - * @param right The right sub formula - */ - And(PCTLStateFormula* left, PCTLStateFormula* right) { - this->left = left; - this->right = right; - } - - /*! - * Destructor. - * - * The subtrees are deleted with the object - * (this behavior can be prevented by setting them to NULL before deletion) - */ - virtual ~And() { - if (left != NULL) { - delete left; - } - if (right != NULL) { - delete right; - } - } - - /*! - * Sets the left child node. - * - * @param newLeft the new left child. - */ - void setLeft(PCTLStateFormula* newLeft) { - left = newLeft; - } - - /*! - * Sets the right child node. - * - * @param newRight the new right child. - */ - void setRight(PCTLStateFormula* newRight) { - right = newRight; - } - - /*! - * @returns a pointer to the left child node - */ - PCTLStateFormula* getLeft() { - return left; - } - - /*! - * @returns a pointer to the right child node - */ - PCTLStateFormula* getRight() { - return right; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() { - std::string result = "("; - result += left->toString(); - result += " && "; - result += right->toString(); - result += ")"; - return result; - } - - /*! - * Clones the called object. - * - * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones - * - * @returns a new AND-object that is identical the called object. - */ - virtual PCTLStateFormula* clone() { - And* result = new And(); - if (this->left != NULL) { - result->setLeft(left->clone()); - } - if (this->right != NULL) { - result->setRight(right->clone()); - } - return result; - } - - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A bit vector indicating all states that satisfy the formula represented by the called object. - */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkAnd(this); - } +public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ + And() { + left = NULL; + right = NULL; + } + + /*! + * Constructor. + * Creates an AND note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + And(PCTLStateFormula* left, PCTLStateFormula* right) { + this->left = left; + this->right = right; + } + + /*! + * Destructor. + * + * The subtrees are deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~And() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { + return left; + } + + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { + return right; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { + std::string result = "("; + result += left->toString(); + result += " && "; + result += right->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() { + And* result = new And(); + if (this->left != NULL) { + result->setLeft(left->clone()); + } + if (this->right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkAnd(this); + } + +private: + PCTLStateFormula* left; + PCTLStateFormula* right; }; } //namespace formula diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 3e48dc132..c0061691c 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -36,142 +36,145 @@ namespace formula { */ template class BoundedUntil : public PCTLPathFormula { - PCTLStateFormula* left; - PCTLStateFormula* right; - uint_fast64_t bound; - public: - /*! - * Empty constructor - */ - BoundedUntil() { - this->left = NULL; - this->right = NULL; - bound = 0; - } - - /*! - * Constructor - * - * @param left The left formula subtree - * @param right The left formula subtree - * @param bound The maximal number of steps - */ - BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right, - uint_fast64_t bound) { - this->left = left; - this->right = right;; - this->bound = bound; - } - - /*! - * Destructor. - * - * Also deletes the subtrees. - * (this behaviour can be prevented by setting the subtrees to NULL before deletion) - */ - virtual ~BoundedUntil() { - if (left != NULL) { - delete left; - } - if (right != NULL) { - delete right; - } - } - - /*! - * Sets the left child node. - * - * @param newLeft the new left child. - */ - void setLeft(PCTLStateFormula* newLeft) { - left = newLeft; - } - - /*! - * Sets the right child node. - * - * @param newRight the new right child. - */ - void setRight(PCTLStateFormula* newRight) { - right = newRight; - } - - /*! - * @returns a pointer to the left child node - */ - PCTLStateFormula* getLeft() { - return left; - } - - /*! - * @returns a pointer to the right child node - */ - PCTLStateFormula* getRight() { - return right; - } - - /*! - * @returns the maximally allowed number of steps for the bounded until operator - */ - uint_fast64_t getBound() { - return bound; - } - - /*! - * Sets the maximally allowed number of steps for the bounded until operator - * - * @param bound the new bound. - */ - void setBound(uint_fast64_t bound) { - this->bound = bound; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() { - std::string result = "("; - result += left->toString(); - result += " U<="; - result += boost::lexical_cast(bound); - result += " "; - result += right->toString(); - result += ")"; - return result; - } - - /*! - * Clones the called object. - * - * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones - * - * @returns a new BoundedUntil-object that is identical the called object. - */ - virtual PCTLPathFormula* clone() { - BoundedUntil* result = new BoundedUntil(); - result->setBound(bound); - if (left != NULL) { - result->setLeft(left->clone()); - } - if (right != NULL) { - result->setRight(right->clone()); - } - return result; - } - - - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A vector indicating the probability that the formula holds for each state. - */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkBoundedUntil(this); - } + +public: + /*! + * Empty constructor + */ + BoundedUntil() { + this->left = NULL; + this->right = NULL; + bound = 0; + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + * @param bound The maximal number of steps + */ + BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right, + uint_fast64_t bound) { + this->left = left; + this->right = right;; + this->bound = bound; + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~BoundedUntil() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { + return left; + } + + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { + return right; + } + + /*! + * @returns the maximally allowed number of steps for the bounded until operator + */ + uint_fast64_t getBound() { + return bound; + } + + /*! + * Sets the maximally allowed number of steps for the bounded until operator + * + * @param bound the new bound. + */ + void setBound(uint_fast64_t bound) { + this->bound = bound; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { + std::string result = "("; + result += left->toString(); + result += " U<="; + result += boost::lexical_cast(bound); + result += " "; + result += right->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual PCTLPathFormula* clone() { + BoundedUntil* result = new BoundedUntil(); + result->setBound(bound); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkBoundedUntil(this); + } + +private: + PCTLStateFormula* left; + PCTLStateFormula* right; + uint_fast64_t bound; }; } //namespace formula diff --git a/src/formula/Next.h b/src/formula/Next.h index 6000366ff..4ec120b80 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -32,90 +32,92 @@ namespace formula { */ template class Next : public PCTLPathFormula { - private: - PCTLStateFormula* child; - public: - /*! - * Empty constructor - */ - Next() { - this->child = NULL; - } - - /*! - * Constructor - * - * @param child The child node - */ - Next(PCTLStateFormula* child) { - this->child = child; - } - - /*! - * Constructor. - * - * Also deletes the subtree. - * (this behaviour can be prevented by setting the subtrees to NULL before deletion) - */ - virtual ~Next() { - if (child != NULL) { - delete child; - } - } - - /*! - * @returns the child node - */ - PCTLStateFormula* getChild() { - return child; - } - - /*! - * Sets the subtree - * @param child the new child node - */ - void setChild(PCTLStateFormula* child) { - this->child = child; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() { - std::string result = "("; - result += " X "; - result += child->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 BoundedUntil-object that is identical the called object. - */ - virtual PCTLPathFormula* clone() { - Next* result = new Next(); - if (child != NULL) { - result->setChild(child); - } - return result; - } - - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A vector indicating the probability that the formula holds for each state. - */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkNext(this); - } + +public: + /*! + * Empty constructor + */ + Next() { + this->child = NULL; + } + + /*! + * Constructor + * + * @param child The child node + */ + Next(PCTLStateFormula* child) { + this->child = child; + } + + /*! + * Constructor. + * + * Also deletes the subtree. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Next() { + if (child != NULL) { + delete child; + } + } + + /*! + * @returns the child node + */ + PCTLStateFormula* getChild() { + return child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(PCTLStateFormula* child) { + this->child = child; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { + std::string result = "("; + result += " X "; + result += child->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 BoundedUntil-object that is identical the called object. + */ + virtual PCTLPathFormula* clone() { + Next* result = new Next(); + if (child != NULL) { + result->setChild(child); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkNext(this); + } + +private: + PCTLStateFormula* child; }; } //namespace formula diff --git a/src/formula/Not.h b/src/formula/Not.h index 59f100f70..dfcb7c100 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -28,87 +28,89 @@ namespace formula { */ template class Not : public PCTLStateFormula { - private: - PCTLStateFormula* child; - public: - /*! - * Empty constructor - */ - Not() { - this->child = NULL; - } - - /*! - * Constructor - * @param child The child node - */ - Not(PCTLStateFormula* child) { - this->child = child; - } - - /*! - * Destructor - * - * Also deletes the subtree - * (this behavior can be prevented by setting them to NULL before deletion) - */ - virtual ~Not() { - if (child != NULL) { - delete child; - } - } - - /*! - * @returns The child node - */ - PCTLStateFormula* getChild() { - return child; - } - - /*! - * Sets the subtree - * @param child the new child node - */ - void setChild(PCTLStateFormula* child) { - this->child = child; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() { - std::string result = "!"; - result += child->toString(); - return result; - } - - /*! - * Clones the called object. - * - * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones - * - * @returns a new AND-object that is identical the called object. - */ - virtual PCTLStateFormula* clone() { - Not* result = new Not(); - if (child != NULL) { - result->setChild(child); - } - return result; - } - - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A bit vector indicating all states that satisfy the formula represented by the called object. - */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkNot(this); - } + +public: + /*! + * Empty constructor + */ + Not() { + this->child = NULL; + } + + /*! + * Constructor + * @param child The child node + */ + Not(PCTLStateFormula* child) { + this->child = child; + } + + /*! + * Destructor + * + * Also deletes the subtree + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Not() { + if (child != NULL) { + delete child; + } + } + + /*! + * @returns The child node + */ + PCTLStateFormula* getChild() { + return child; + } + + /*! + * Sets the subtree + * @param child the new child node + */ + void setChild(PCTLStateFormula* child) { + this->child = child; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { + std::string result = "!"; + result += child->toString(); + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() { + Not* result = new Not(); + if (child != NULL) { + result->setChild(child); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkNot(this); + } + +private: + PCTLStateFormula* child; }; } //namespace formula diff --git a/src/formula/Or.h b/src/formula/Or.h index a5cdbc659..51a2f88fd 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -31,120 +31,122 @@ namespace formula { */ template class Or : public PCTLStateFormula { - private: - PCTLStateFormula* left; - PCTLStateFormula* right; - public: - /*! - * Empty constructor. - * Will create an AND-node without subnotes. Will not represent a complete formula! - */ - Or() { - left = NULL; - right = NULL; - } - - /*! - * Constructor. - * Creates an AND note with the parameters as subtrees. - * - * @param left The left sub formula - * @param right The right sub formula - */ - Or(PCTLStateFormula* left, PCTLStateFormula* right) { - this->left = left; - this->right = right; - } - - /*! - * Destructor. - * - * The subtrees are deleted with the object - * (this behavior can be prevented by setting them to NULL before deletion) - */ - virtual ~Or() { - if (left != NULL) { - delete left; - } - if (right != NULL) { - delete right; - } - } - - /*! - * Sets the left child node. - * - * @param newLeft the new left child. - */ - void setLeft(PCTLStateFormula* newLeft) { - left = newLeft; - } - - /*! - * Sets the right child node. - * - * @param newRight the new right child. - */ - void setRight(PCTLStateFormula* newRight) { - right = newRight; - } - - /*! - * @returns a pointer to the left child node - */ - PCTLStateFormula* getLeft() { - return left; - } - - /*! - * @returns a pointer to the right child node - */ - PCTLStateFormula* getRight() { - return right; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() { - std::string result = "("; - result += left->toString(); - result += " || "; - result += right->toString(); - result += ")"; - return result; - } - - /*! - * Clones the called object. - * - * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones - * - * @returns a new AND-object that is identical the called object. - */ - virtual PCTLStateFormula* clone() { - Or* result = new Or(); - if (this->left != NULL) { - result->setLeft(left->clone()); - } - if (this->right != NULL) { - result->setRight(right->clone()); - } - return result; - } - - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A bit vector indicating all states that satisfy the formula represented by the called object. - */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkOr(this); - } + +public: + /*! + * Empty constructor. + * Will create an AND-node without subnotes. Will not represent a complete formula! + */ + Or() { + left = NULL; + right = NULL; + } + + /*! + * Constructor. + * Creates an AND note with the parameters as subtrees. + * + * @param left The left sub formula + * @param right The right sub formula + */ + Or(PCTLStateFormula* left, PCTLStateFormula* right) { + this->left = left; + this->right = right; + } + + /*! + * Destructor. + * + * The subtrees are deleted with the object + * (this behavior can be prevented by setting them to NULL before deletion) + */ + virtual ~Or() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { + return left; + } + + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { + return right; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { + std::string result = "("; + result += left->toString(); + result += " || "; + result += right->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new AND-object that is identical the called object. + */ + virtual PCTLStateFormula* clone() { + Or* result = new Or(); + if (this->left != NULL) { + result->setLeft(left->clone()); + } + if (this->right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkOr(this); + } + +private: + PCTLStateFormula* left; + PCTLStateFormula* right; }; } //namespace formula diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h index 70255f8b3..b795244e3 100644 --- a/src/formula/PCTLPathFormula.h +++ b/src/formula/PCTLPathFormula.h @@ -27,34 +27,35 @@ namespace formula { */ template class PCTLPathFormula : public PCTLFormula { - public: - /*! - * empty destructor - */ - virtual ~PCTLPathFormula() { } - /*! - * 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 PCTLPathFormula* clone() = 0; +public: + /*! + * empty destructor + */ + virtual ~PCTLPathFormula() { } - /*! - * 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; + /*! + * 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 PCTLPathFormula* clone() = 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; }; } //namespace formula diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h index de8d0e117..daf369510 100644 --- a/src/formula/PCTLStateFormula.h +++ b/src/formula/PCTLStateFormula.h @@ -27,34 +27,35 @@ namespace formula { */ template class PCTLStateFormula : public PCTLFormula { - public: - /*! - * empty destructor - */ - virtual ~PCTLStateFormula() { } - /*! - * 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 PCTLStateFormula* clone() = 0; +public: + /*! + * empty destructor + */ + virtual ~PCTLStateFormula() { } - /*! - * 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 bit vector indicating all states that satisfy the formula represented by the called object. - */ - virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; + /*! + * 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 PCTLStateFormula* clone() = 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 bit vector indicating all states that satisfy the formula represented by the called object. + */ + virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) = 0; }; } //namespace formula diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h index 12f51a4ce..b1e7bf0b9 100644 --- a/src/formula/PCTLformula.h +++ b/src/formula/PCTLformula.h @@ -27,17 +27,18 @@ namespace formula { */ template class PCTLFormula { - public: - /*! - * virtual destructor - */ - virtual ~PCTLFormula() { } - - /*! - * @note This function is not implemented in this class. - * @returns a string representation of the formula - */ - virtual std::string toString() = 0; + +public: + /*! + * virtual destructor + */ + virtual ~PCTLFormula() { } + + /*! + * @note This function is not implemented in this class. + * @returns a string representation of the formula + */ + virtual std::string toString() = 0; }; } //namespace formula diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 89978f30f..b0585fd58 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -34,128 +34,131 @@ namespace formula { */ template class ProbabilisticOperator : public PCTLStateFormula { - T lower; - T upper; - PCTLPathFormula* pathFormula; - public: - /*! - * Empty constructor - */ - ProbabilisticOperator() { - upper = mrmc::misc::constGetZero(&upper); - lower = mrmc::misc::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 (can be omitted, is then set to NULL) - */ - ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) { - 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 ~ProbabilisticOperator() { - if (pathFormula != NULL) { - delete pathFormula; - } - } - - /*! - * @returns the child node (representation of a PCTL path formula) - */ - PCTLPathFormula* getPathFormula () { - return pathFormula; - } - - /*! - * @returns the lower bound for the probability - */ - T getLowerBound() { - return lower; - } - - /*! - * @returns the upper bound for the probability - */ - T getUpperBound() { - 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. - * - * @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() { - 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() { - ProbabilisticOperator* result = new ProbabilisticOperator(); - 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkProbabilisticOperator(this); - } + +public: + /*! + * Empty constructor + */ + ProbabilisticOperator() { + upper = mrmc::misc::constGetZero(&upper); + lower = mrmc::misc::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 (can be omitted, is then set to NULL) + */ + ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) { + 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 ~ProbabilisticOperator() { + if (pathFormula != NULL) { + delete pathFormula; + } + } + + /*! + * @returns the child node (representation of a PCTL path formula) + */ + PCTLPathFormula* getPathFormula () { + return pathFormula; + } + + /*! + * @returns the lower bound for the probability + */ + T getLowerBound() { + return lower; + } + + /*! + * @returns the upper bound for the probability + */ + T getUpperBound() { + 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. + * + * @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() { + 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() { + ProbabilisticOperator* result = new ProbabilisticOperator(); + 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(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkProbabilisticOperator(this); + } + +private: + T lower; + T upper; + PCTLPathFormula* pathFormula; }; } //namespace formula diff --git a/src/formula/Until.h b/src/formula/Until.h index 39f361e11..df80ee0e0 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -33,117 +33,120 @@ namespace formula { */ template class Until : public PCTLPathFormula { - PCTLStateFormula* left; - PCTLStateFormula* right; - public: - /*! - * Empty constructor - */ - Until() { - this->left = NULL; - this->right = NULL; - } - - /*! - * Constructor - * - * @param left The left formula subtree - * @param right The left formula subtree - */ - Until(PCTLStateFormula* left, PCTLStateFormula* right) { - this->left = left; - this->right = right; - } - - /*! - * Destructor. - * - * Also deletes the subtrees. - * (this behaviour can be prevented by setting the subtrees to NULL before deletion) - */ - virtual ~Until() { - if (left != NULL) { - delete left; - } - if (right != NULL) { - delete right; - } - } - - /*! - * Sets the left child node. - * - * @param newLeft the new left child. - */ - void setLeft(PCTLStateFormula* newLeft) { - left = newLeft; - } - - /*! - * Sets the right child node. - * - * @param newRight the new right child. - */ - void setRight(PCTLStateFormula* newRight) { - right = newRight; - } - - /*! - * @returns a pointer to the left child node - */ - PCTLStateFormula* getLeft() { - return left; - } - - /*! - * @returns a pointer to the right child node - */ - PCTLStateFormula* getRight() { - return right; - } - - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() { - std::string result = "("; - result += left->toString(); - result += " U "; - result += right->toString(); - result += ")"; - return result; - } - - /*! - * Clones the called object. - * - * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones - * - * @returns a new BoundedUntil-object that is identical the called object. - */ - virtual PCTLPathFormula* clone() { - Until* result = new Until(); - if (left != NULL) { - result->setLeft(left->clone()); - } - if (right != NULL) { - result->setRight(right->clone()); - } - return result; - } - - /*! - * Calls the model checker to check this formula. - * Needed to infer the correct type of formula class. - * - * @note This function should only be called in a generic check function of a model checker class. For other uses, - * the methods of the model checker should be used. - * - * @returns A vector indicating the probability that the formula holds for each state. - */ - virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - return modelChecker->checkUntil(this); - } + +public: + /*! + * Empty constructor + */ + Until() { + this->left = NULL; + this->right = NULL; + } + + /*! + * Constructor + * + * @param left The left formula subtree + * @param right The left formula subtree + */ + Until(PCTLStateFormula* left, PCTLStateFormula* right) { + this->left = left; + this->right = right; + } + + /*! + * Destructor. + * + * Also deletes the subtrees. + * (this behaviour can be prevented by setting the subtrees to NULL before deletion) + */ + virtual ~Until() { + if (left != NULL) { + delete left; + } + if (right != NULL) { + delete right; + } + } + + /*! + * Sets the left child node. + * + * @param newLeft the new left child. + */ + void setLeft(PCTLStateFormula* newLeft) { + left = newLeft; + } + + /*! + * Sets the right child node. + * + * @param newRight the new right child. + */ + void setRight(PCTLStateFormula* newRight) { + right = newRight; + } + + /*! + * @returns a pointer to the left child node + */ + PCTLStateFormula* getLeft() { + return left; + } + + /*! + * @returns a pointer to the right child node + */ + PCTLStateFormula* getRight() { + return right; + } + + /*! + * @returns a string representation of the formula + */ + virtual std::string toString() { + std::string result = "("; + result += left->toString(); + result += " U "; + result += right->toString(); + result += ")"; + return result; + } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @returns a new BoundedUntil-object that is identical the called object. + */ + virtual PCTLPathFormula* clone() { + Until* result = new Until(); + if (left != NULL) { + result->setLeft(left->clone()); + } + if (right != NULL) { + result->setRight(right->clone()); + } + return result; + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector *check(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { + return modelChecker->checkUntil(this); + } + +private: + PCTLStateFormula* left; + PCTLStateFormula* right; }; } //namespace formula From cdc0332fd7a17ece0f6b3cf10021d4a6fed31d53 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 11:43:02 +0100 Subject: [PATCH 7/7] Code style and fixing errors in doxygen code for model checker class --- src/modelChecker/DtmcPrctlModelChecker.h | 278 +++++++++++------------ 1 file changed, 139 insertions(+), 139 deletions(-) diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 979d8d93d..3061dc75b 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -54,145 +54,145 @@ namespace modelChecker { */ template class DtmcPrctlModelChecker { - public: - /*! - * Constructor - * - * @parameter Dtmc The dtmc model which is checked. - */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* Dtmc); - - /*! - * Copy constructor - * - * @parameter modelChecker The model checker that is copied. - */ - explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker); - - /*! - * Destructor - */ - virtual ~DtmcPrctlModelChecker(); - - /*! - * @returns A reference to the dtmc of the model checker. - */ - mrmc::models::Dtmc* getDtmc() const { - return this->dtmc; - } - - /*! - * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all - * other edges from these states) - * - * @param states A bit vector representing a set of states that should become absorbing. - */ - virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0; - - /*! - * Returns all states that are labeled with a given atomic proposition. - * - * @param ap A string representing an atomic proposition. - * @returns The set of states labeled with the atomic proposition ap. - */ - virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0; - - /*! - * Multiplies the matrix with a given vector; the result again is a vector. - * - * @param vector The vector to multiply the matrix with. - * @returns The result of multiplying the transition probability matrix with vector. - */ - virtual std::vector multiplyMatrixVector(std::vector* vector) = 0; - - /*! - * The check method for a state formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @param formula The state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) { - return formula->check(this); - } - - /*! - * The check method for a state formula with an And node as root in its formula tree - * - * @param formula The And formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And* formula) = 0; - - /*! - * The check method for a formula with an AP node as root in its formula tree - * - * @param formula The AP state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0; - - /*! - * The check method for a formula with a Not node as root in its formula tree - * - * @param formula The Not state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0; - - /*! - * The check method for a state formula with an Or node as root in its formula tree - * - * @param formula The Or state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0; - - /*! - * 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(mrmc::formula::ProbabilisticOperator*) = 0; - - /*! - * The check method for a path formula; Will infer the actual type of formula and delegate it - * to the specialized method - * - * @param formula The path formula to check - * @returns for each state the probability that the path formula holds. - */ - virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula* formula) { - return formula->check(this); - } - - /*! - * The check method for a path formula with a Bounded Until operator node as root in its formula tree - * - * @param formula The Bounded Until path formula to check - * @returns for each state the probability that the path formula holds. - */ - virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0; - - /*! - * The check method for a path formula with a Next operator node as root in its formula tree - * - * @param formula The Next path formula to check - * @returns for each state the probability that the path formula holds. - */ - virtual std::vector checkNext(mrmc::formula::Next*) = 0; - - /*! - * The check method for a path formula with an Until operator node as root in its formula tree - * - * @param formula The Until path formula to check - * @returns for each state the probability that the path formula holds. - */ - virtual std::vector checkUntil(mrmc::formula::Until*) = 0; - - private: - mrmc::models::Dtmc* dtmc; +public: + /*! + * Constructor + * + * @param Dtmc The dtmc model which is checked. + */ + explicit DtmcPrctlModelChecker(mrmc::models::Dtmc* Dtmc); + + /*! + * Copy constructor + * + * @param modelChecker The model checker that is copied. + */ + explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker); + + /*! + * Destructor + */ + virtual ~DtmcPrctlModelChecker(); + + /*! + * @returns A reference to the dtmc of the model checker. + */ + mrmc::models::Dtmc* getDtmc() const { + return this->dtmc; + } + + /*! + * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all + * other edges from these states) + * + * @param states A bit vector representing a set of states that should become absorbing. + */ + virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0; + + /*! + * Returns all states that are labeled with a given atomic proposition. + * + * @param ap A string representing an atomic proposition. + * @returns The set of states labeled with the atomic proposition ap. + */ + virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0; + + /*! + * Multiplies the matrix with a given vector; the result again is a vector. + * + * @param vector The vector to multiply the matrix with. + * @returns The result of multiplying the transition probability matrix with vector. + */ + virtual std::vector multiplyMatrixVector(std::vector* vector) = 0; + + /*! + * The check method for a state formula; Will infer the actual type of formula and delegate it + * to the specialized method + * + * @param formula The state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) { + return formula->check(this); + } + + /*! + * The check method for a state formula with an And node as root in its formula tree + * + * @param formula The And formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And* formula) = 0; + + /*! + * The check method for a formula with an AP node as root in its formula tree + * + * @param formula The AP state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP* formula) = 0; + + /*! + * The check method for a formula with a Not node as root in its formula tree + * + * @param formula The Not state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not* formula) = 0; + + /*! + * The check method for a state formula with an Or node as root in its formula tree + * + * @param formula The Or state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or* formula) = 0; + + /*! + * 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(mrmc::formula::ProbabilisticOperator* formula) = 0; + + /*! + * The check method for a path formula; Will infer the actual type of formula and delegate it + * to the specialized method + * + * @param formula The path formula to check + * @returns for each state the probability that the path formula holds. + */ + virtual std::vector checkPathFormula(mrmc::formula::PCTLPathFormula* formula) { + return formula->check(this); + } + + /*! + * The check method for a path formula with a Bounded Until operator node as root in its formula tree + * + * @param formula The Bounded Until path formula to check + * @returns for each state the probability that the path formula holds. + */ + virtual std::vector checkBoundedUntil(mrmc::formula::BoundedUntil* formula) = 0; + + /*! + * The check method for a path formula with a Next operator node as root in its formula tree + * + * @param formula The Next path formula to check + * @returns for each state the probability that the path formula holds. + */ + virtual std::vector checkNext(mrmc::formula::Next* formula) = 0; + + /*! + * The check method for a path formula with an Until operator node as root in its formula tree + * + * @param formula The Until path formula to check + * @returns for each state the probability that the path formula holds. + */ + virtual std::vector checkUntil(mrmc::formula::Until* formula) = 0; + +private: + mrmc::models::Dtmc* dtmc; }; } //namespace modelChecker