Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC

src/formula/AP.h

@@ -14,29 +14,87 @@ namespace mrmc {
 
 namespace formula {
 
-class AP : public PCTLStateFormula {
+/*!
-   private:
+ * @brief
-   std::string ap;
+ * Class for a PCTL formula tree with atomic proposition as root.
-   public:
+ *
-      AP(std::string ap) {
+ * This class represents the leaves in the formula tree.
-         this->ap = ap;
+ *
-      }
+ * @see PCTLStateFormula
-
+ * @see PCTLFormula
-      AP(char* ap) {
+ */
-         this->ap = ap;
+template <class T>
-      }
+class AP : public PCTLStateFormula<T> {
-
+public:
-      std::string getAP() {
+	/*!
-         return ap;
+	 * Constructor
-      }
+	 *
-
+	 * Creates a new atomic proposition leaf, with the label AP
-      std::string toString() {
+	 *
-         return getAP();
+	 * @param ap The string representing the atomic proposition
-      }
+	 */
-
+	AP(std::string ap) {
-      virtual enum stateFormulaTypes type() {
+		this->ap = ap;
-            return stateFormulaTypes::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<T>* 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<T>* modelChecker) {
+	  return modelChecker->checkAP(this);
+	}
+
+private:
+	std::string ap;
 };
 
 } //namespace formula

src/formula/And.h

@@ -15,48 +15,139 @@ namespace mrmc {
 
 namespace formula {
 
-class And : public PCTLStateFormula {
+/*!
-   private:
+ * @brief
-      PCTLStateFormula* left;
+ * Class for a PCTL formula tree with AND node as root.
-      PCTLStateFormula* right;
+ *
-   public:
+ * Has two PCTL state formulas as sub formulas/trees.
-      And() {
+ *
-         left = NULL;
+ * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
-         right = NULL;
+ * the model checker works.
-      }
+ *
-      And(PCTLStateFormula* left, PCTLStateFormula* right) {
+ * The subtrees are seen as part of the object and deleted with the object
-         this->left = left;
+ * (this behavior can be prevented by setting them to NULL before deletion)
-         this->right = right;
+ *
-      }
+ * @see PCTLStateFormula
-
+ * @see PCTLFormula
-      void setLeft(PCTLStateFormula* newLeft) {
+ */
-         left = newLeft;
+template <class T>
-      }
+class And : public PCTLStateFormula<T> {
-
+public:
-      void setRight(PCTLStateFormula* newRight) {
+	/*!
-         right = newRight;
+	 * Empty constructor.
-      }
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
-
+	 */
-      PCTLStateFormula* getLeft() {
+	And() {
-         return left;
+		left = NULL;
-      }
+		right = NULL;
-
+	}
-      PCTLStateFormula* getRight() {
+	/*!
-         return right;
+	 * Constructor.
-      }
+	 * Creates an AND note with the parameters as subtrees.
-
+	 *
-      std::string toString() {
+	 * @param left The left sub formula
-         std::string result = "(";
+	 * @param right The right sub formula
-         result += left->toString();
+	 */
-         result += " && ";
+	And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
-         result += right->toString();
+		this->left = left;
-         result += ")";
+		this->right = right;
-         return result;
+	}
-      }
+	/*!
-
+	 * Destructor.
-      virtual enum stateFormulaTypes type() {
+	 *
-            return AND;
+	 * 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<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* 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<T>* clone() {
+		And<T>* 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<T>* modelChecker) {
+		return modelChecker->checkAnd(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula

src/formula/BoundedUntil.h

@@ -11,69 +11,170 @@
 #include "PCTLPathFormula.h"
 #include "PCTLStateFormula.h"
 #include "boost/integer/integer_mask.hpp"
+#include "boost/lexical_cast.hpp"
+#include <string>
 
 namespace mrmc {
 
 namespace formula {
 
-class BoundedUntil : public PCTLPathFormula {
+/*!
-      PCTLStateFormula* left;
+ * @brief
-      PCTLStateFormula* right;
+ * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
-      uint_fast64_t bound;
+ *
-   public:
+ * Has two PCTL state formulas as sub formulas/trees.
-      BoundedUntil() {
+ *
-         this->left = NULL;
+ * @par Semantics
-         this->right = NULL;
+ * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
-         bound = 0;
+ * \e left holds.
-      }
+ *
-
+ * The subtrees are seen as part of the object and deleted with the object
-      BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right,
+ * (this behavior can be prevented by setting them to NULL before deletion)
-                   uint_fast64_t bound) {
+ *
-         this->left = left;
+ * @see PCTLPathFormula
-         this->right = right;
+ * @see PCTLFormula
-         this->bound = bound;
+ */
-      }
+template <class T>
-
+class BoundedUntil : public PCTLPathFormula<T> {
-      virtual ~BoundedUntil();
+public:
-
+	/*!
-      void setLeft(PCTLStateFormula* newLeft) {
+	 * Empty constructor
-         left = newLeft;
+	 */
-      }
+	BoundedUntil() {
-
+		this->left = NULL;
-      void setRight(PCTLStateFormula* newRight) {
+		this->right = NULL;
-         right = newRight;
+		bound = 0;
-      }
+	}
-
+	/*!
-      PCTLStateFormula* getLeft() {
+	 * Constructor
-         return left;
+	 *
-      }
+	 * @param left The left formula subtree
-
+	 * @param right The left formula subtree
-      PCTLStateFormula* getRight() {
+	 * @param bound The maximal number of steps
-         return right;
+	 */
-      }
+	BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
-
+					 uint_fast64_t bound) {
-      uint_fast64_t getBound() {
+		this->left = left;
-         return bound;
+		this->right = right;;
-      }
+		this->bound = bound;
-
+	}
-      void setBound(uint_fast64_t bound) {
+	/*!
-         this->bound = bound;
+	 * Destructor.
-      }
+	 *
-
+	 * Also deletes the subtrees.
-      std::string toString() {
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-         std::string result = "(";
+	 */
-         result += left->toString();
+	virtual ~BoundedUntil() {
-         result += " U<=";
+	  if (left != NULL) {
-         result +=  std::to_string(bound);
+		  delete left;
-         result += " ";
+	  }
-         result += right->toString();
+	  if (right != NULL) {
-         result += ")";
+		  delete right;
-         return result;
+	  }
-      }
+	}
-
+	/*!
-      virtual enum pathFormulaTypes type() {
+	 * Sets the left child node.
-            return BOUNDED_UNTIL;
+	 *
-      }
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* 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<std::string>(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<T>* clone() {
+		BoundedUntil<T>* 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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkBoundedUntil(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
+	uint_fast64_t bound;
 };
 
 } //namespace formula

src/formula/Next.h

@@ -15,38 +15,109 @@ 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
+ * 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 T>
+class Next : public PCTLPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Next() {
+		this->child = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Next(PCTLStateFormula<T>* 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<T>* getChild() {
+		return child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PCTLStateFormula<T>* 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<T>* clone() {
+		Next<T>* result = new Next<T>();
+		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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkNext(this);
+	}
 
-class Next : public PCTLPathFormula {
+private:
-   private:
+	PCTLStateFormula<T>* child;
-      PCTLStateFormula* child;
-   public:
-      Next() {
-         this->child = NULL;
-      }
-
-      Next(PCTLStateFormula* child) {
-         this->child = child;
-      }
-
-      PCTLStateFormula* getChild() {
-         return child;
-      }
-
-      void setChild(PCTLStateFormula* child) {
-         this->child = child;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += " X ";
-         result += child->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum pathFormulaTypes type() {
-            return NEXT;
-      }
 };
 
 } //namespace formula

src/formula/Not.h

@@ -8,45 +8,109 @@
 #ifndef NOT_H_
 #define NOT_H_
 
+#include "PCTLStateFormula.h"
+
 namespace mrmc {
 
 namespace formula {
 
-#include "PCTLStateFormula.h"
+/*!
+ * @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
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLStateFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class Not : public PCTLStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Not() {
+		this->child = NULL;
+	}
 
-class Not : public PCTLStateFormula {
+	/*!
-   private:
+	 * Constructor
-      PCTLStateFormula* child;
+	 * @param child The child node
-   public:
+	 */
-      Not() {
+	Not(PCTLStateFormula<T>* child) {
-         this->child = NULL;
+		this->child = child;
-      }
+	}
 
-      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;
+	  }
+	}
 
-      virtual ~Not() {
+	/*!
+	 * @returns The child node
+	 */
+	PCTLStateFormula<T>* getChild() {
+		return child;
+	}
 
-      }
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
 
-      PCTLStateFormula* getChild() {
+	/*!
-         return child;
+	 * @returns a string representation of the formula
-      }
+	 */
+	virtual std::string toString() {
+		std::string result = "!";
+		result += child->toString();
+		return result;
+	}
 
-      void setChild(PCTLStateFormula* child) {
+	/*!
-         this->child = child;
+	 * 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<T>* clone() {
+		Not<T>* result = new Not<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		return result;
+	}
 
-      std::string toString() {
+	/*!
-         std::string result = "!";
+	 * Calls the model checker to check this formula.
-         result += child->toString();
+	 * Needed to infer the correct type of formula class.
-         return result;
+	 *
-      }
+	 * @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<T>* modelChecker) {
+	  return modelChecker->checkNot(this);
+	}
 
-      virtual enum stateFormulaTypes type() {
+private:
-            return NOT;
+	PCTLStateFormula<T>* child;
-      }
 };
 
 } //namespace formula

src/formula/Or.h

@@ -14,48 +14,139 @@ namespace mrmc {
 
 namespace formula {
 
-class Or : public PCTLStateFormula {
+/*!
-   private:
+ * @brief
-      PCTLStateFormula* left;
+ * Class for a PCTL formula tree with OR node as root.
-      PCTLStateFormula* right;
+ *
-   public:
+ * Has two PCTL state formulas as sub formulas/trees.
-      Or() {
+ *
-         left = NULL;
+ * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
-         right = NULL;
+ * the model checker works.
-      }
+ *
-      Or(PCTLStateFormula* left, PCTLStateFormula* right) {
+ * The subtrees are seen as part of the object and deleted with the object
-         this->left = left;
+ * (this behavior can be prevented by setting them to NULL before deletion)
-         this->right = right;
+ *
-      }
+ * @see PCTLStateFormula
-
+ * @see PCTLFormula
-      void setLeft(PCTLStateFormula* newLeft) {
+ */
-         left = newLeft;
+template <class T>
-      }
+class Or : public PCTLStateFormula<T> {
-
+public:
-      void setRight(PCTLStateFormula* newRight) {
+	/*!
-         right = newRight;
+	 * Empty constructor.
-      }
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
-
+	 */
-      PCTLStateFormula* getLeft() {
+	Or() {
-         return left;
+		left = NULL;
-      }
+		right = NULL;
-
+	}
-      PCTLStateFormula* getRight() {
+	/*!
-         return right;
+	 * Constructor.
-      }
+	 * Creates an AND note with the parameters as subtrees.
-
+	 *
-      std::string toString() {
+	 * @param left The left sub formula
-         std::string result = "(";
+	 * @param right The right sub formula
-         result += left->toString();
+	 */
-         result += " || ";
+	Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
-         result += right->toString();
+		this->left = left;
-         result += ")";
+		this->right = right;
-         return result;
+	}
-      }
+	/*!
-
+	 * Destructor.
-      virtual enum stateFormulaTypes type() {
+	 *
-            return OR;
+	 * 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<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* 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<T>* clone() {
+		Or<T>* 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<T>* modelChecker) {
+	  return modelChecker->checkOr(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula

src/formula/PCTLPathFormula.h

@@ -9,16 +9,53 @@
 #define PCTLPATHFORMULA_H_
 
 #include "PCTLformula.h"
-#include "formulaTypes.h"
+#include "modelChecker/DtmcPrctlModelChecker.h"
+#include <vector>
 
 namespace mrmc {
 
 namespace formula {
 
-//abstract
+/*!
-class PCTLPathFormula : public PCTLFormula {
+ * @brief
-   public:
+ * Abstract base class for PCTL path formulas.
-      virtual enum pathFormulaTypes type() = 0;
+ *
+ * @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 T>
+class PCTLPathFormula : public PCTLFormula<T> {
+
+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<T>* 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<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
 };
 
 } //namespace formula

src/formula/PCTLStateFormula.h

@@ -9,17 +9,53 @@
 #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 {
+ * @brief
-   public:
+ * Abstract base class for PCTL state formulas.
-      virtual enum stateFormulaTypes type() = 0;
+ *
+ * @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 T>
+class PCTLStateFormula : public PCTLFormula<T> {
+
+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<T>* 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<T>* modelChecker) = 0;
 };
 
 } //namespace formula

src/formula/PCTLformula.h

@@ -16,9 +16,29 @@ 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
+ * 	   PCTLPathFormula and PCTLStateFormula offer the method clone().
+ */
+template <class T>
 class PCTLFormula {
-   public:
+public:
-      virtual std::string toString() = 0;
+	/*!
+	 * 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

src/formula/ProbabilisticOperator.h

@@ -9,63 +9,156 @@
 #define PROBABILISTICOPERATOR_H_
 
 #include "PCTLStateFormula.h"
+#include "PCTLPathFormula.h"
+#include "misc/const_templates.h"
 
 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
+ * 	  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 T>
-class ProbabilisticOperator : public PCTLStateFormula {
+class ProbabilisticOperator : public PCTLStateFormula<T> {
-      T lower;
+public:
-      T upper;
+	/*!
-      PCTLPathFormula* pathFormula;
+	 * Empty constructor
-   public:
+	 */
-      ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) {
+	ProbabilisticOperator() {
-         this->lower = lowerBound;
+		upper = mrmc::misc::constGetZero(&upper);
-         this->upper = upperBound;
+		lower = mrmc::misc::constGetZero(&lower);
-         this->pathFormula = pathFormula;
+		pathFormula = NULL;
-      }
+	}
-
+	/*!
-      virtual ~ProbabilisticOperator() {
+	 * Constructor
-         delete pathFormula;
+	 *
-      }
+	 * @param lowerBound The lower bound for the probability
-
+	 * @param upperBound The upper bound for the probability
-      PCTLPathFormula* getPathFormula () {
+	 * @param pathFormula The child node (can be omitted, is then set to NULL)
-         return pathFormula;
+	 */
-      }
+	ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
-
+		this->lower = lowerBound;
-      T getLowerBound() {
+		this->upper = upperBound;
-         return lower;
+		this->pathFormula = pathFormula;
-      }
+	}
-
+	/*!
-      T getUpperBound() {
+	 * Destructor
-         return upper;
+	 *
-      }
+	 * The subtree is deleted with the object
-
+	 * (this behavior can be prevented by setting them to NULL before deletion)
-      void setPathFormula(PCTLPathFormula* pathFormula) {
+	 */
-         this->pathFormula = pathFormula;
+	virtual ~ProbabilisticOperator() {
-      }
+	 if (pathFormula != NULL) {
-
+		 delete pathFormula;
-      void setInterval(T lowerBound, T upperBound) {
+	 }
-         this->lower = lowerBound;
+	}
-         this->upper = upperBound;
+	/*!
-      }
+	 * @returns the child node (representation of a PCTL path formula)
-
+	 */
-      std::string toString() {
+	PCTLPathFormula<T>* getPathFormula () {
-         std::string result = "(";
+		return pathFormula;
-         result += " P[";
+	}
-         result += lower;
+	/*!
-         result += ";";
+	 * @returns the lower bound for the probability
-         result += upper;
+	 */
-         result += "] ";
+	T getLowerBound() {
-         result += pathFormula->toString();
+		return lower;
-         result += ")";
+	}
-         return result;
+	/*!
-      }
+	 * @returns the upper bound for the probability
-
+	 */
-      virtual enum stateFormulaTypes type() {
+	T getUpperBound() {
-            return PROBABILISTIC;
+		return upper;
-      }
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(PCTLPathFormula<T>* 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<T>* clone() {
+		ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
+		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<T>* modelChecker) {
+	  return modelChecker->checkProbabilisticOperator(this);
+	}
+
+private:
+	T lower;
+	T upper;
+	PCTLPathFormula<T>* pathFormula;
 };
 
 } //namespace formula

src/formula/Until.h

@@ -15,49 +15,138 @@ namespace mrmc {
 
 namespace formula {
 
-class Until : public PCTLPathFormula {
+/*!
-      PCTLStateFormula* left;
+ * @brief
-      PCTLStateFormula* right;
+ * Class for a PCTL (path) formula tree with an Until node as root.
-   public:
+ *
-      Until() {
+ * Has two PCTL state formulas as sub formulas/trees.
-         this->left = NULL;
+ *
-         this->right = NULL;
+ * @par Semantics
-      }
+ * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
-
+ * \e left holds always.
-      Until(PCTLStateFormula* left, PCTLStateFormula* right) {
+ *
-         this->left = left;
+ * The subtrees are seen as part of the object and deleted with the object
-         this->right = right;
+ * (this behavior can be prevented by setting them to NULL before deletion)
-      }
+ *
-      virtual ~Until();
+ * @see PCTLPathFormula
-
+ * @see PCTLFormula
-      void setLeft(PCTLStateFormula* newLeft) {
+ */
-         left = newLeft;
+template <class T>
-      }
+class Until : public PCTLPathFormula<T> {
-
+public:
-      void setRight(PCTLStateFormula* newRight) {
+	/*!
-         right = newRight;
+	 * Empty constructor
-      }
+	 */
-
+	Until() {
-      PCTLStateFormula* getLeft() {
+		this->left = NULL;
-         return left;
+		this->right = NULL;
-      }
+	}
-
+	/*!
-      PCTLStateFormula* getRight() {
+	 * Constructor
-         return right;
+	 *
-      }
+	 * @param left The left formula subtree
-
+	 * @param right The left formula subtree
-      std::string toString() {
+	 */
-         std::string result = "(";
+	Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
-         result += left->toString();
+		this->left = left;
-         result += " U ";
+		this->right = right;
-         result += right->toString();
+	}
-         result += ")";
+	/*!
-         return result;
+	 * Destructor.
-      }
+	 *
-
+	 * Also deletes the subtrees.
-      virtual enum pathFormulaTypes type() {
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
-            return UNTIL;
+	 */
-      }
+	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<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* 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<T>* clone() {
+		Until<T>* 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<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkUntil(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula

src/formula/formulaTypes.h

@@ -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_ */

src/modelChecker/DtmcPrctlModelChecker.cpp

@@ -12,8 +12,8 @@ namespace mrmc {
 namespace modelChecker {
 
 template<class T>
-DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC) {
+DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* dtmc) {
-   this->DTMC = DTMC;
+   this->dtmc = dtmc;
 }
 
 template<class T>
@@ -21,6 +21,11 @@ DtmcPrctlModelChecker<T>::~DtmcPrctlModelChecker() {
    delete this->dtmc;
 }
 
+template<class T>
+DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	this->dtmc = new mrmc::models::Dtmc<T>(modelChecker->getDtmc());
+}
+
 
 } //namespace modelChecker
 

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 T>
+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"
@@ -25,65 +43,156 @@ 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 T>
 class DtmcPrctlModelChecker {
-   private:
+public:
-      mrmc::models::Dtmc<T>* dtmc;
+	/*!
-
+	 * Constructor
-   protected:
+	 *
-      mrmc::models::Dtmc<T>* getDtmc() const {
+	 * @param Dtmc The dtmc model which is checked.
-         return this->dtmc;
+	 */
-      }
+	explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* Dtmc);
-
+	/*!
-   public:
+	 * Copy constructor
-      explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC);
+	 *
-      ~DtmcPrctlModelChecker();
+	 * @param modelChecker The model checker that is copied.
-
+	 */
-      virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0;
+	explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker);
-      virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0;
+	/*!
-      virtual std::vector<T> multiplyMatrixVector(std::vector<T>*) = 0;
+	 * Destructor
-
+	 */
-      virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) {
+	virtual ~DtmcPrctlModelChecker();
-         if (formula->type() == AND) {
+	/*!
-            return checkAnd(static_cast<mrmc::formula::And*>(formula));
+	 * @returns A reference to the dtmc of the model checker.
-         }
+	 */
-         if (formula->type() == stateFormulaTypes::AP) {
+	mrmc::models::Dtmc<T>* getDtmc() const {
-            return checkAP(static_cast<mrmc::formula::AP*>(formula));
+		return this->dtmc;
-         }
+	}
-         if (formula->type() == NOT) {
+	/*!
-            return checkNot(static_cast<mrmc::formula::Not*>(formula));
+	 * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all
-         }
+	 * other edges from these states)
-         if (formula->type() == OR) {
+	 *
-            return checkOr(static_cast<mrmc::formula::Or*>(formula));
+	 * @param states A bit vector representing a set of states that should become absorbing.
-         }
+	 */
-         if (formula->type() == PROBABILISTIC) {
+	virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0;
-            return checkProbabilisticOperator(
+	/*!
-                  static_cast<mrmc::formula::ProbabilisticOperator<T>*>(formula));
+	 * 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 checkAnd(mrmc::formula::And*) = 0;
+	virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0;
-      virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0;
+	/*!
-      virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0;
+	 * Multiplies the matrix with a given vector; the result again is a vector.
-      virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0;
+	 *
-      virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>*) = 0;
+	 * @param vector The vector to multiply the matrix with.
-
+	 * @returns The result of multiplying the transition probability matrix with vector.
-      virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula* formula) {
+	 */
-         if (formula->type() == NEXT) {
+	virtual std::vector<T> multiplyMatrixVector(std::vector<T>* vector) = 0;
-            return checkNext(static_cast<mrmc::formula::Next*>(formula));
+	/*!
-         }
+	 * The check method for a state formula; Will infer the actual type of formula and delegate it
-         if (formula->type() == UNTIL) {
+	 * to the specialized method
-            return checkUntil(static_cast<mrmc::formula::Until*>(formula));
+	 *
-         }
+	 * @param formula The state formula to check
-         if (formula->type() == BOUNDED_UNTIL) {
+	 * @returns The set of states satisfying the formula, represented by a bit vector
-            return checkBoundedUntil(static_cast<mrmc::formula::BoundedUntil*>(formula));
+	 */
-         }
+	virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula<T>* formula) {
-      }
+		return formula->check(this);
-
+	}
-      virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0;
+	/*!
-      virtual std::vector<T> checkNext(mrmc::formula::Next*) = 0;
+	 * The check method for a state formula with an And node as root in its formula tree
-      virtual std::vector<T> checkUntil(mrmc::formula::Until*) = 0;
+	 *
+	 * @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<T>* 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<T>* 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<T>* 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<T>* 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<T>* 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<T> checkPathFormula(mrmc::formula::PCTLPathFormula<T>* 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<T> checkBoundedUntil(mrmc::formula::BoundedUntil<T>* 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<T> checkNext(mrmc::formula::Next<T>* 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<T> checkUntil(mrmc::formula::Until<T>* formula) = 0;
+
+private:
+	mrmc::models::Dtmc<T>* dtmc;
 };
 
 } //namespace modelChecker

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<std::string> getPropositionsForState(uint_fast32_t state) {
+		if (state >= stateCount) {
+			throw std::out_of_range("State index out of range.");
+		}
+		std::set<std::string> 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.

src/models/Dtmc.h

@@ -106,6 +106,13 @@ public:
 		return this->probabilityMatrix;
 	}
 
+	/*!
+	 *
+	 */
+	std::set<std::string> getPropositionsForState(uint_fast32_t state) {
+		return stateLabeling->getPropositionsForState(state);
+	}
+
 	/*!
 	 * Retrieves a reference to the backwards transition relation.
 	 * @return A reference to the backwards transition relation.

src/parser/parser.cpp

@@ -7,9 +7,9 @@
 
 #include <sys/stat.h>
 #include <fcntl.h>
-#if defined MACOSX
+//#if defined MACOSX
 	#include <unistd.h>
-#endif
+//#endif
 #include <errno.h>
 #include <iostream>
 #include <cstring>

src/parser/readPrctlFile.cpp

@@ -61,7 +61,7 @@ namespace
 		/*!
 		 *	@brief Resulting formula.
 		 */
-		mrmc::formula::PCTLFormula* result;
+		mrmc::formula::PCTLFormula<double>* result;
 		
 		struct dump
 		{
@@ -106,7 +106,7 @@ namespace
 	};
 }
 
-mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename)
+mrmc::formula::PCTLFormula<double>* mrmc::parser::readPrctlFile(const char* filename)
 {
 	PRCTLParser p;
 	mrmc::parser::MappedFile file(filename);

src/parser/readPrctlFile.h

@@ -9,7 +9,7 @@ namespace parser {
 /*!
  *	@brief Load PRCTL file
  */
-mrmc::formula::PCTLFormula* readPrctlFile(const char * filename);
+mrmc::formula::PCTLFormula<double>* readPrctlFile(const char * filename);
 
 } // namespace parser
 } // namespace mrmc

src/utility/utility.cpp

@@ -9,70 +9,57 @@
 #include "src/parser/readTraFile.h"
 #include "src/parser/readLabFile.h"
 
+#include <fstream>
+
 namespace mrmc {
 
 namespace utility {
 
-void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename) {
+void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename) {
-	//FIXME: adapt this to the refactored names
+   mrmc::storage::SquareSparseMatrix<double>* matrix = dtmc->getTransitionProbabilityMatrix();
-	//FIXME: use C++-style for file output here, as performance is not critical here
+   double* diagonal_storage = matrix->getDiagonalStoragePointer();
-/*   FILE *P;
-   mrmc::sparse::StaticSparseMatrix<double>* 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();
 
-   P = fopen(filename, "w");
+   std::ofstream file;
+   file.open(filename);
 
-   if (P == NULL) {
+   file << "digraph dtmc {\n";
-      pantheios::log_ERROR("File could not be opened.");
-      throw mrmc::exceptions::file_IO_exception();
-   }
-
-   fprintf(P, "digraph dtmc {\n");
 
    //Specify the nodes and their labels
-   for (uint_fast64_t i = 1; i <= dtmc->getNodeCount(); i++) {
+   for (uint_fast64_t i = 1; i < dtmc->getNumberOfStates(); i++) {
-      fprintf(P, "\t%Lu[label=\"%Lu\\n{", i, i);
+      file << "\t" << i << "[label=\"" << i << "\\n{";
       char komma=' ';
-      for(auto it = labels->getPropositionMap()->begin();
+      std::set<std::string> propositions = dtmc->getPropositionsForState(i);
-               it != labels->getPropositionMap()->end();
+      for(auto it = propositions.begin();
+               it != propositions.end();
                it++) {
-         if(labels->nodeHasProposition(it->first, i)) {
+      	file << komma << *it;
-            fprintf(P, "%c%s", komma, (it->first).c_str());
+         komma=',';
-         }
-         char 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";
+   	}
+   }
 
-
+   file << "}\n";
-   fprintf(P, "}\n");
+   file.close();
-
-   fclose(P); */
 }
 
+//TODO: Should this stay here or be integrated in the new parser structure?
 mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
 	mrmc::parser::TraParser tp(tra_file);
 	uint_fast64_t node_count = tp.getMatrix()->getRowCount();

src/utility/utility.h

@@ -25,7 +25,7 @@ namespace utility {
                      it will be overwritten.
 
  */
-void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename);
+void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename);
 
 /*!
     Parses a transition file and a labeling file and produces a DTMC out of them.

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<double>* 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;
+}
+
+

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 {