Added abstract reward formulas

src/formula/abstract/CumulativeReward.h

@@ -0,0 +1,101 @@
+/*
+ * InstantaneousReward.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_ABSTRACT_CUMULATIVEREWARD_H_
+#define STORM_FORMULA_ABSTRACT_CUMULATIVEREWARD_H_
+
+#include "AbstractFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include <string>
+
+namespace storm {
+namespace formula {
+namespace abstract {
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Cumulative Reward node as root.
+ *
+ * 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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class CumulativeReward : public AbstractFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	CumulativeReward() {
+		bound = 0;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param bound The time bound of the reward formula
+	 */
+	CumulativeReward(T bound) {
+		this->bound = bound;
+	}
+
+	/*!
+	 * Empty destructor.
+	 */
+	virtual ~CumulativeReward() {
+		// Intentionally left empty.
+	}
+
+	/*!
+	 * @returns the time instance for the instantaneous reward operator
+	 */
+	T getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the the time instance for the instantaneous reward operator
+	 *
+	 * @param bound the new bound.
+	 */
+	void setBound(T bound) {
+		this->bound = bound;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "C <= ";
+		result += std::to_string(bound);
+		return result;
+	}
+	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *  
+     *  As CumulativeReward objects have no subformulas, we return true here.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true
+     */	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return true;
+	}
+
+private:
+	T bound;
+};
+
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */

src/formula/abstract/InstantaneousReward.h

@@ -0,0 +1,102 @@
+/*
+ * InstantaneousReward.h
+ *
+ *  Created on: 26.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_
+#define STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_
+
+#include "AbstractFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "boost/integer/integer_mask.hpp"
+#include <string>
+
+namespace storm {
+namespace formula {
+namespace abstract {
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Instantaneous Reward node as root.
+ *
+ * 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 AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class InstantaneousReward : public AbstractFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	InstantaneousReward() {
+		bound = 0;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param bound The time instance of the reward formula
+	 */
+	InstantaneousReward(uint_fast64_t bound) {
+		this->bound = bound;
+	}
+
+	/*!
+	 * Empty destructor.
+	 */
+	virtual ~InstantaneousReward() {
+		// Intentionally left empty.
+	}
+
+	/*!
+	 * @returns the time instance for the instantaneous reward operator
+	 */
+	uint_fast64_t getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the the time instance for the instantaneous reward 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() const {
+		std::string result = "I=";
+		result += std::to_string(bound);
+		return result;
+	}
+	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *  
+     *  As InstantaneousReward formulas have no subformulas, we return true here.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return true;
+	}
+
+private:
+	uint_fast64_t bound;
+};
+
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */

src/formula/abstract/SteadyStateReward.h

@@ -0,0 +1,63 @@
+/*
+ * SteadyStateReward.h
+ *
+ *  Created on: 08.04.2013
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_
+#define STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_
+
+#include "AbstractFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include <string>
+
+namespace storm {
+namespace formula {
+namespace abstract {
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a Steady State Reward node as root.
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class SteadyStateReward: public AbstractFormula<T> {
+public:
+	/*!
+	 * Empty constructor
+	 */
+	SteadyStateReward() {
+		// Intentionally left empty
+
+	}
+	virtual ~SteadyStateReward() {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		return "S";
+	}
+
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  As SteadyStateReward objects have no subformulas, we return true here.
+     *
+     *  @param checker Formula checker object.
+     *  @return true
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return true;
+	}
+};
+
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_ */