Added time bounded operators for CSL.

src/formula/Formulas.h

@@ -35,6 +35,9 @@
 #include "SteadyStateNoBoundOperator.h"
 #include "SteadyStateBoundOperator.h"
 
+#include "TimeBoundedUntil.h"
+#include "TimeBoundedEventually.h"
+
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"

src/formula/TimeBoundedEventually.h

@@ -0,0 +1,133 @@
+/*
+ * TimeBoundedEventually.h
+ *
+ *  Created on: 10.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_
+#define STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_
+
+#include "TimeBoundedOperator.h"
+#include "AbstractStateFormula.h"
+
+namespace storm {
+namespace formula {
+
+template<class T> class TimeBoundedEventually;
+
+/*!
+ *  @brief Interface class for model checkers that support TimeBoundedEventually.
+ *
+ *  All model checkers that support the formula class BoundedEventually must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class ITimeBoundedEventuallyModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates TimeBoundedUntil formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkTimeBoundedEventually(const TimeBoundedEventually<T>& obj, bool qualitative) const = 0;
+};
+
+
+template<class T>
+class TimeBoundedEventually: public storm::formula::TimeBoundedOperator<T> {
+public:
+	/**
+	 * Simple constructor: Only sets the bounds
+	 *
+	 * @param lowerBound
+	 * @param upperBound
+	 */
+	TimeBoundedEventually(T lowerBound, T upperBound) : TimeBoundedOperator<T>(lowerBound, upperBound) {
+		child = nullptr;
+	}
+
+	TimeBoundedEventually(T lowerBound, T upperBound, AbstractStateFormula<T>* child) :
+		TimeBoundedOperator<T>(lowerBound, upperBound) {
+		this->child = child;
+	}
+
+	virtual ~TimeBoundedEventually() {
+		if (child != nullptr) {
+			delete child;
+		}
+	}
+
+
+	/*!
+	 * @returns the child node
+	 */
+	const AbstractStateFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "F";
+		result += TimeBoundedOperator<T>::toString();
+		result += " ";
+		result += child->toString();
+		return result;
+	}
+
+	/*!
+	 * 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 AbstractPathFormula<T>* clone() const {
+		TimeBoundedEventually<T>* result = new TimeBoundedEventually<T>(this->getLowerBound(), this->getUpperBound());
+		if (child != nullptr) {
+			result->setChild(child->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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*this, qualitative);
+	}
+
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
+
+private:
+	AbstractStateFormula<T>* child;
+};
+
+} /* namespace formula */
+} /* namespace storm */
+#endif /* STORM_FORMULA_TIMEBOUNDEDEVENTUALLY_H_ */

src/formula/TimeBoundedOperator.h

@@ -0,0 +1,101 @@
+/*
+ * TimeBoundedOperator.h
+ *
+ *  Created on: 10.04.2013
+ *      Author: thomas
+ */
+
+#ifndef TIMEBOUNDEDOPERATOR_H_
+#define TIMEBOUNDEDOPERATOR_H_
+
+#include "AbstractPathFormula.h"
+#include "exceptions/InvalidArgumentException.h"
+
+namespace storm {
+namespace formula {
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a operator node as root that uses a time interval
+ * (with upper and lower bound)
+ *
+ * This class does not provide support for sub formulas; this has to be done in concretizations of this abstract class.
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template<class T>
+class TimeBoundedOperator: public storm::formula::AbstractPathFormula<T> {
+public:
+	/**
+	 * Constructor
+	 *
+	 * @param lowerBound The lower bound
+	 * @param upperBound The upper bound
+	 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
+	 */
+	TimeBoundedOperator(T lowerBound, T upperBound) {
+		setInterval(lowerBound, upperBound);
+	}
+
+	/**
+	 * Destructor
+	 */
+	virtual ~TimeBoundedOperator() {
+		// Intentionally left empty
+	}
+
+	/**
+	 * Getter for lowerBound attribute
+	 *
+	 * @return lower bound of the operator.
+	 */
+	T getLowerBound() const {
+		return lowerBound;
+	}
+
+	/**
+	 * Getter for upperBound attribute
+	 * @return upper bound of the operator.
+	 */
+	T getUpperBound() const {
+		return upperBound;
+	}
+
+	/**
+	 * Set the time interval for the time bounded operator
+	 *
+	 * @param lowerBound
+	 * @param upperBound
+	 * @throw InvalidArgumentException if the lower bound is larger than the upper bound.
+	 */
+	void setInterval(T lowerBound, T upperBound) {
+		if (lowerBound > upperBound) {
+			throw new storm::exceptions::InvalidArgumentException("Lower bound is larger than upper bound");
+		}
+		this->lowerBound = lowerBound;
+		this->upperBound = upperBound;
+	}
+
+
+	/*!
+	 * @returns a string representation of the Interval of the formula
+	 * 			May be used in subclasses to simplify string output.
+	 */
+	virtual std::string toString() const {
+		std::string result = "[";
+		result += std::to_string(lowerBound);
+		result += ";";
+		result += "]";
+		return result;
+	}
+
+private:
+	T lowerBound, upperBound;
+};
+
+} /* namespace formula */
+} /* namespace storm */
+#endif /* TIMEBOUNDEDOPERATOR_H_ */

src/formula/TimeBoundedUntil.h

@@ -0,0 +1,168 @@
+/*
+ * TimeBoundedUntil.h
+ *
+ *  Created on: 10.04.2013
+ *      Author: thomas
+ */
+
+#ifndef STORM_FORMULA_TIMEBOUNDEDUNTIL_H_
+#define STORM_FORMULA_TIMEBOUNDEDUNTIL_H_
+
+#include "TimeBoundedOperator.h"
+
+namespace storm {
+namespace formula {
+
+template <class T> class TimeBoundedUntil;
+
+/*!
+ *  @brief Interface class for model checkers that support TimeBoundedUntil.
+ *
+ *  All model checkers that support the formula class BoundedEventually must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class ITimeBoundedUntilModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates TimeBoundedUntil formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual std::vector<T>* checkTimeBoundedUntil(const TimeBoundedUntil<T>& obj, bool qualitative) const = 0;
+};
+
+template <class T>
+class TimeBoundedUntil: public storm::formula::TimeBoundedOperator<T> {
+public:
+	/**
+	 * Constructor providing bounds only;
+	 * Sub formulas are set to null.
+	 *
+	 * @param lowerBound
+	 * @param upperBound
+	 */
+	TimeBoundedUntil(T lowerBound, T upperBound) :
+		TimeBoundedOperator<T>(lowerBound, upperBound) {
+		this->left = nullptr;
+		this->right = nullptr;
+	}
+
+
+	/**
+	 * Full constructor
+	 * @param lowerBound
+	 * @param upperBound
+	 * @param left
+	 * @param right
+	 */
+	TimeBoundedUntil(T lowerBound, T upperBound, AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) :
+		TimeBoundedOperator<T>(lowerBound, upperBound) {
+		this->left = left;
+		this->right = right;
+	}
+
+	virtual ~TimeBoundedUntil() {
+	   if (left != nullptr) {
+	   	delete left;
+	   }
+	   if (right != nullptr) {
+	   	delete right;
+	   }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(AbstractStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(AbstractStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractStateFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractStateFormula<T>& getRight() const {
+		return *right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = left->toString();
+		result += " U";
+		result += TimeBoundedOperator<T>::toString();
+		result += " ";
+		result += right->toString();
+		return result;
+	}
+
+	/*!
+	 * 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 AbstractPathFormula<T>* clone() const {
+		TimeBoundedUntil<T>* result = new TimeBoundedUntil<T>(this->getLowerBound(), this->getUpperBound());
+		if (left != nullptr) {
+			result->setLeft(left->clone());
+		}
+		if (right != nullptr) {
+			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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+		return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*this, qualitative);
+	}
+
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->left) && checker.conforms(this->right);
+	}
+
+private:
+	AbstractStateFormula<T>* left;
+	AbstractStateFormula<T>* right;
+};
+
+} /* namespace formula */
+} /* namespace storm */
+#endif /* STORM_FORMULA_TIMEBOUNDEDUNTIL_H_ */