- 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

@@ -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 T>
+class AP : public PCTLStateFormula<T> {
    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<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);
       }
 };
 

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 T>
+class And : public PCTLStateFormula<T> {
    private:
-      PCTLStateFormula* left;
+      PCTLStateFormula<T>* left;
-      PCTLStateFormula* right;
+      PCTLStateFormula<T>* 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<T>* left, PCTLStateFormula<T>* 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<T>* newLeft) {
          left = newLeft;
       }
 
-      void setRight(PCTLStateFormula* newRight) {
+      /*!
+       * Sets the right child node.
+       *
+       * @param newRight the new right child.
+       */
+      void setRight(PCTLStateFormula<T>* newRight) {
          right = newRight;
       }
 
-      PCTLStateFormula* getLeft() {
+      /*!
+       * @returns a pointer to the left child node
+       */
+      PCTLStateFormula<T>* getLeft() {
          return left;
       }
 
-      PCTLStateFormula* getRight() {
+      /*!
+       * @returns a pointer to the right child node
+       */
+      PCTLStateFormula<T>* 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<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);
       }
+
 };
 
 } //namespace formula

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 <string>
 
 namespace mrmc {
 
 namespace formula {
 
-class BoundedUntil : public PCTLPathFormula {
+/*!
-      PCTLStateFormula* left;
+ * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
-      PCTLStateFormula* right;
+ * 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 T>
+class BoundedUntil : public PCTLPathFormula<T> {
+      PCTLStateFormula<T>* left;
+      PCTLStateFormula<T>* 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<T>* left, PCTLStateFormula<T>* 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<T>* newLeft) {
          left = newLeft;
       }
 
-      void setRight(PCTLStateFormula* newRight) {
+      /*!
+       * Sets the right child node.
+       *
+       * @param newRight the new right child.
+       */
+      void setRight(PCTLStateFormula<T>* newRight) {
          right = newRight;
       }
 
-      PCTLStateFormula* getLeft() {
+      /*!
+       * @returns a pointer to the left child node
+       */
+      PCTLStateFormula<T>* getLeft() {
          return left;
       }
 
-      PCTLStateFormula* getRight() {
+      /*!
+       * @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;
       }
 
-      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<std::string>(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<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);
       }
 };
 

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 T>
+class Next : public PCTLPathFormula<T> {
    private:
-      PCTLStateFormula* child;
+      PCTLStateFormula<T>* child;
    public:
+      /*!
+       * Empty constructor
+       */
       Next() {
          this->child = NULL;
       }
 
-      Next(PCTLStateFormula* child) {
+      /*!
+       * Constructor
+       *
+       * @param child The child node
+       */
+      Next(PCTLStateFormula<T>* 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<T>* getChild() {
          return child;
       }
 
-      void setChild(PCTLStateFormula* child) {
+      /*!
+       * Sets the subtree
+       * @param child the new child node
+       */
+      void setChild(PCTLStateFormula<T>* 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<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);
       }
 };
 

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 for a PCTL formula tree with NOT node as root.
-class Not : public PCTLStateFormula {
+ * 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> {
    private:
-      PCTLStateFormula* child;
+      PCTLStateFormula<T>* child;
    public:
+      /*!
+       * Empty constructor
+       */
       Not() {
          this->child = NULL;
       }
 
-      Not(PCTLStateFormula* child) {
+      /*!
+       * Constructor
+       * @param child The child node
+       */
+      Not(PCTLStateFormula<T>* 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<T>* getChild() {
          return child;
       }
 
-      void setChild(PCTLStateFormula* child) {
+      /*!
+       * Sets the subtree
+       * @param child the new child node
+       */
+      void setChild(PCTLStateFormula<T>* 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<T>* clone() {
+      	Not<T>* result = new Not<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 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);
       }
 };
 

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 T>
+class Or : public PCTLStateFormula<T> {
    private:
-      PCTLStateFormula* left;
+      PCTLStateFormula<T>* left;
-      PCTLStateFormula* right;
+      PCTLStateFormula<T>* 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<T>* left, PCTLStateFormula<T>* 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<T>* newLeft) {
          left = newLeft;
       }
 
-      void setRight(PCTLStateFormula* newRight) {
+      /*!
+       * Sets the right child node.
+       *
+       * @param newRight the new right child.
+       */
+      void setRight(PCTLStateFormula<T>* newRight) {
          right = newRight;
       }
 
-      PCTLStateFormula* getLeft() {
+      /*!
+       * @returns a pointer to the left child node
+       */
+      PCTLStateFormula<T>* getLeft() {
          return left;
       }
 
-      PCTLStateFormula* getRight() {
+      /*!
+       * @returns a pointer to the right child node
+       */
+      PCTLStateFormula<T>* 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<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);
       }
 };
 

src/formula/PCTLPathFormula.h

@@ -9,16 +9,50 @@
 #define PCTLPATHFORMULA_H_
 
 #include "PCTLformula.h"
-#include "formulaTypes.h"
+#include "modelChecker/DtmcPrctlModelChecker.h"
+#include <vector>
 
 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 T>
+class PCTLPathFormula : public PCTLFormula<T> {
    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<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,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 T>
+class PCTLStateFormula : public PCTLFormula<T> {
    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<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,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 T>
 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;
 };
 

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 T>
-class ProbabilisticOperator : public PCTLStateFormula {
+class ProbabilisticOperator : public PCTLStateFormula<T> {
       T lower;
       T upper;
-      PCTLPathFormula* pathFormula;
+      PCTLPathFormula<T>* 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<T>* pathFormula=NULL) {
          this->lower = lowerBound;
          this->upper = upperBound;
          this->pathFormula = pathFormula;
       }
 
+      /*!
+       * Destructor
+       *
+       * The subtree is deleted with the object
+       * (this behavior can be prevented by setting them to NULL before deletion)
+       */
       virtual ~ProbabilisticOperator() {
+    	 if (pathFormula != NULL) {
     		 delete pathFormula;
     	 }
+      }
 
-      PCTLPathFormula* getPathFormula () {
+      /*!
+       * @returns the child node (representation of a PCTL path formula)
+       */
+      PCTLPathFormula<T>* 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<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;
       }
 
-      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<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);
       }
 };
 

src/formula/Until.h

@@ -15,38 +15,95 @@ namespace mrmc {
 
 namespace formula {
 
-class Until : public PCTLPathFormula {
+/*!
-      PCTLStateFormula* left;
+ * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
-      PCTLStateFormula* right;
+ * 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 T>
+class Until : public PCTLPathFormula<T> {
+      PCTLStateFormula<T>* left;
+      PCTLStateFormula<T>* 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<T>* left, PCTLStateFormula<T>* 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<T>* newLeft) {
          left = newLeft;
       }
 
-      void setRight(PCTLStateFormula* newRight) {
+      /*!
+       * Sets the right child node.
+       *
+       * @param newRight the new right child.
+       */
+      void setRight(PCTLStateFormula<T>* newRight) {
          right = newRight;
       }
 
-      PCTLStateFormula* getLeft() {
+      /*!
+       * @returns a pointer to the left child node
+       */
+      PCTLStateFormula<T>* getLeft() {
          return left;
       }
 
-      PCTLStateFormula* getRight() {
+      /*!
+       * @returns a pointer to the right child node
+       */
+      PCTLStateFormula<T>* 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<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);
       }
 };
 

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>

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"
@@ -37,53 +55,30 @@ class DtmcPrctlModelChecker {
 
    public:
       explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC);
-      ~DtmcPrctlModelChecker();
+      virtual ~DtmcPrctlModelChecker();
 
       virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0;
       virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0;
       virtual std::vector<T> multiplyMatrixVector(std::vector<T>*) = 0;
 
-      virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) {
+      virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula<T>* formula) {
-         if (formula->type() == AND) {
+         return formula->check(this);
-            return checkAnd(static_cast<mrmc::formula::And*>(formula));
-         }
-         if (formula->type() == stateFormulaTypes::AP) {
-            return checkAP(static_cast<mrmc::formula::AP*>(formula));
-         }
-         if (formula->type() == NOT) {
-            return checkNot(static_cast<mrmc::formula::Not*>(formula));
-         }
-         if (formula->type() == OR) {
-            return checkOr(static_cast<mrmc::formula::Or*>(formula));
-         }
-         if (formula->type() == PROBABILISTIC) {
-            return checkProbabilisticOperator(
-                  static_cast<mrmc::formula::ProbabilisticOperator<T>*>(formula));
-         }
       }
 
 
-      virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And*) = 0;
+      virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And<T>*) = 0;
-      virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0;
+      virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP<T>*) = 0;
-      virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0;
+      virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not<T>*) = 0;
-      virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0;
+      virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or<T>*) = 0;
       virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>*) = 0;
 
-      virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula* formula) {
+      virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula<T>* formula) {
-         if (formula->type() == NEXT) {
+         return formula->check(this);
-            return checkNext(static_cast<mrmc::formula::Next*>(formula));
-         }
-         if (formula->type() == UNTIL) {
-            return checkUntil(static_cast<mrmc::formula::Until*>(formula));
-         }
-         if (formula->type() == BOUNDED_UNTIL) {
-            return checkBoundedUntil(static_cast<mrmc::formula::BoundedUntil*>(formula));
-         }
       }
 
-      virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0;
+      virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil<T>*) = 0;
-      virtual std::vector<T> checkNext(mrmc::formula::Next*) = 0;
+      virtual std::vector<T> checkNext(mrmc::formula::Next<T>*) = 0;
-      virtual std::vector<T> checkUntil(mrmc::formula::Until*) = 0;
+      virtual std::vector<T> checkUntil(mrmc::formula::Until<T>*) = 0;
 };
 
 } //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 - 1);
+	}
+
 	/*!
 	 * 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");
 
-   if (P == NULL) {
+   std::ofstream file;
-      pantheios::log_ERROR("File could not be opened.");
+   file.open(filename);
-      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++) {
+   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++ ) {
+   for (uint_fast64_t row = 0; row < dtmc->getNumberOfStates(); row++ ) {
-      //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",
+   	            file << "\t" << row << " -> " << row << " [label=" << diagonal_storage[row] <<"]\n";
-                  row, row, diagonal_storage[row]);
    	         }
+   	//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, "\t%Lu -> %Lu [label=%f]\n",
-            row, column_indications[i], value_storage[i]);
    }
 
-
+   file << "}\n";
-
+   file.close();
-   fprintf(P, "}\n");
-
-   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 {