From adf16e5f9e286590e21648bf3024321a1cd2d418 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 16 Apr 2013 11:41:41 +0200 Subject: [PATCH] Added abstract reward formulas --- src/formula/abstract/CumulativeReward.h | 101 ++++++++++++++++++++ src/formula/abstract/InstantaneousReward.h | 102 +++++++++++++++++++++ src/formula/abstract/SteadyStateReward.h | 63 +++++++++++++ 3 files changed, 266 insertions(+) create mode 100644 src/formula/abstract/CumulativeReward.h create mode 100644 src/formula/abstract/InstantaneousReward.h create mode 100644 src/formula/abstract/SteadyStateReward.h diff --git a/src/formula/abstract/CumulativeReward.h b/src/formula/abstract/CumulativeReward.h new file mode 100644 index 000000000..8e8c3532c --- /dev/null +++ b/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 + +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 CumulativeReward : public AbstractFormula { + +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& checker) const { + return true; + } + +private: + T bound; +}; + +} //namespace abstract +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */ diff --git a/src/formula/abstract/InstantaneousReward.h b/src/formula/abstract/InstantaneousReward.h new file mode 100644 index 000000000..627e9f503 --- /dev/null +++ b/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 + +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 InstantaneousReward : public AbstractFormula { + +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& checker) const { + return true; + } + +private: + uint_fast64_t bound; +}; + +} //namespace abstract +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */ diff --git a/src/formula/abstract/SteadyStateReward.h b/src/formula/abstract/SteadyStateReward.h new file mode 100644 index 000000000..120f08410 --- /dev/null +++ b/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 + +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 SteadyStateReward: public AbstractFormula { +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& checker) const { + return true; + } +}; + +} //namespace abstract +} //namespace formula +} //namespace storm +#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_ */