From f5d220535202569793eef39f01c550b22521fe35 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 3 Dec 2012 08:51:56 +0100 Subject: [PATCH] - 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 {