From be6223e4a7e5048e058a4ee8c0d2f9db712fe471 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Wed, 12 Dec 2012 16:12:43 +0100
Subject: [PATCH] Forgot the file for the probabilistic operator in the
 previous commit. Also, improved toString methods for other probabilistic
 operators

---
 src/formula/ProbabilisticIntervalOperator.h |   5 +-
 src/formula/ProbabilisticNoBoundsOperator.h | 100 ++++++++++++++++++++
 src/formula/ProbabilisticOperator.h         |   8 +-
 3 files changed, 108 insertions(+), 5 deletions(-)
 create mode 100644 src/formula/ProbabilisticNoBoundsOperator.h

diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h
index f61ec8af3..c7ffb9ba3 100644
--- a/src/formula/ProbabilisticIntervalOperator.h
+++ b/src/formula/ProbabilisticIntervalOperator.h
@@ -124,12 +124,11 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const {
-		std::string result = "(";
-		result += " P[";
+		std::string result = "P[";
 		result += std::to_string(lower);
 		result += ";";
 		result += std::to_string(upper);
-		result += "] ";
+		result += "] (";
 		result += pathFormula->toString();
 		result += ")";
 		return result;
diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/ProbabilisticNoBoundsOperator.h
new file mode 100644
index 000000000..09a2fc4c3
--- /dev/null
+++ b/src/formula/ProbabilisticNoBoundsOperator.h
@@ -0,0 +1,100 @@
+/*
+ * ProbabilisticNoBoundsOperator.h
+ *
+ *  Created on: 12.12.2012
+ *      Author: thomas
+ */
+
+#ifndef PROBABILISTICNOBOUNDSOPERATOR_H_
+#define PROBABILISTICNOBOUNDSOPERATOR_H_
+
+#include "PCTLformula.h"
+#include "PCTLPathFormula.h"
+
+namespace mrmc {
+namespace formula {
+
+/*!
+ * @brief
+ * Class for a PCTL formula tree with a P (probablistic) operator without declaration of probabilities
+ * as root.
+ *
+ * Checking a formula with this operator as root returns the probabilities that the path formula holds
+ * (for each state)
+ *
+ * Has one PCTL path formula as sub formula/tree.
+ *
+ * @note
+ * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
+ * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from PCTLformula.
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see PCTLStateFormula
+ * @see PCTLPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticIntervalOperator
+ * @see PCTLFormula
+ */
+template <class T>
+class ProbabilisticNoBoundsOperator: public mrmc::formula::PCTLFormula<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticNoBoundsOperator() {
+		// TODO Auto-generated constructor stub
+		this->pathFormula = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	ProbabilisticNoBoundsOperator(PCTLPathFormula<T> &pathFormula) {
+		this->pathFormula = &pathFormula;
+	}
+
+	/*!
+	 * Destructor
+	 */
+	virtual ~ProbabilisticNoBoundsOperator() {
+		// TODO Auto-generated destructor stub
+	}
+
+	/*!
+	 * @returns the child node (representation of a PCTL path formula)
+	 */
+	const PCTLPathFormula<T>& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = " P=? (";
+		result += pathFormula->toString();
+		result += ")";
+		return result;
+	}
+
+private:
+	PCTLPathFormula<T>* pathFormula;
+};
+
+} /* namespace formula */
+} /* namespace mrmc */
+#endif /* PROBABILISTICNOBOUNDSOPERATOR_H_ */
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index f1f6df24f..cbceee0d4 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -139,8 +139,12 @@ public:
 	 * @returns a string representation of this PCTLStateFormula
 	 */
 	virtual std::string toString() const {
-		// TODO
-		return "";
+		std::string result = " P=";
+		result += std::to_string(bound);
+		result += " (";
+		result += pathFormula->toString();
+		result += ")";
+		return result;
 	}
 private:
 	T bound;