Added abstract reward operators.

src/formula/abstract/RewardBoundOperator.h

@@ -0,0 +1,82 @@
+/*
+ * RewardBoundOperator.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_
+
+#include "PathBoundOperator.h"
+#include "utility/ConstTemplates.h"
+
+namespace storm {
+namespace formula {
+namespace abstract {
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root.
+ *
+ * Has a reward path formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the reward of the reward path formula 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 AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see AbstractFormula
+ */
+template<class T, class FormulaType>
+class RewardBoundOperator : public PathBoundOperator<T, FormulaType> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	RewardBoundOperator() : PathBoundOperator<T>(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonRelation The relation to compare the actual value and the bound
+	 * @param bound The bound for the probability
+	 * @param pathFormula The child node
+	 */
+	RewardBoundOperator(
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula) :
+				PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+		// Intentionally left empty
+	}
+
+	RewardBoundOperator(
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula, bool minimumOperator)
+			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "R ";
+		result += PathBoundOperator<T>::toString();
+		return result;
+	}
+};
+
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_ */

src/formula/abstract/RewardNoBoundOperator.h

@@ -0,0 +1,90 @@
+/*
+ * RewardNoBoundOperator.h
+ *
+ *  Created on: 25.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_
+
+#include "AbstractFormula.h"
+#include "PathNoBoundOperator.h"
+
+namespace storm {
+namespace formula {
+namespace abstract {
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a R (reward) operator without declaration of reward values
+ * as root.
+ *
+ * Checking a formula with this operator as root returns the reward for the reward path formula for
+ * each state
+ *
+ * Has one Abstract 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 AbstractFormula.
+ *
+ * @note
+ * 	This class does not contain a check() method like the other formula classes.
+ * 	The check method should only be called by the model checker to infer the correct check function for sub
+ * 	formulas. As this operator can only appear at the root, the method is not useful here.
+ * 	Use the checkRewardNoBoundOperator method from the DtmcPrctlModelChecker class instead.
+ *
+ * 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 AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticIntervalOperator
+ * @see AbstractFormula
+ */
+template <class T, class FormulaType>
+class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	RewardNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param pathFormula The child node.
+	 */
+	RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "R";
+		result += PathNoBoundOperator<T>::toString();
+		return result;
+	}
+};
+
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_ */