tempest/src/properties/ltl/Until.h

#ifndef STORM_PROPERTIES_LTL_UNTIL_H_
#define STORM_PROPERTIES_LTL_UNTIL_H_

#include "AbstractLtlFormula.h"

namespace storm {
	namespace properties {
		namespace ltl {

			// Forward declaration for the interface class.
			template <class T> class Until;

			/*!
			 * Interface class for model checkers that support Until.
			 *
			 * All model checkers that support the formula class Until must inherit
			 * this pure virtual class.
			 */
			template <class T>
			class IUntilModelChecker {
				public:

					/*!
					 * Empty virtual destructor.
					 */
					virtual ~IUntilModelChecker() {
						// Intentionally left empty
					}

					/*!
					 * Evaluates an Until formula within a model checker.
					 *
					 * @param obj Formula object with subformulas.
					 * @return The modelchecking result of the formula for every state.
					 */
					virtual std::vector<T> checkUntil(Until<T> const & obj) const = 0;
			};

			/*!
			 * Class for an Ltl formula tree with an Until node as root.
			 *
			 * Has two Ltl formulas as sub formulas/trees.
			 *
			 * @par Semantics
			 * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
			 * \e left holds always.
			 *
			 * The object has shared ownership of its subtrees. If this object is deleted and no other object has a shared
			 * ownership of the subtrees they will be deleted as well.
			 *
			 * @see AbstractLtlFormula
			 */
			template <class T>
			class Until : public AbstractLtlFormula<T> {

			public:

				/*!
				 * Creates an Until node without subnodes.
				 * The resulting object will not represent a complete formula!
				 */
				Until() : left(nullptr), right(nullptr) {
					// Intentionally left empty.
				}

				/*!
				 * Creates an Until node using the given parameters.
				 *
				 * @param left The left formula subtree.
				 * @param right The right formula subtree.
				 */
				Until(std::shared_ptr<AbstractLtlFormula<T>> const & left, std::shared_ptr<AbstractLtlFormula<T>> const & right) : left(left), right(right) {
					// Intentionally left empty.
				}

				/*!
				 * Empty virtual destructor.
				 */
				virtual ~Until() {
					// Intentionally left empty.
				}

				/*!
				 * Clones the called object.
				 *
				 * Performs a "deep copy", i.e. the subnodes of the new object are clones of the original ones.
				 *
				 * @returns A new Until object that is a deep copy of the called object.
				 */
				virtual std::shared_ptr<AbstractLtlFormula<T>> clone() const override {
					auto result = std::make_shared<Until<T>>();
					if (this->isLeftSet()) {
					  result->setLeft(left->clone());
					}
					if (this->isRightSet()) {
					  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(storm::modelchecker::ltl::AbstractModelChecker<T> const & modelChecker) const {
					return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
				}

				/*!
				 * Returns a textual representation of the formula tree with this node as root.
				 *
				 * @returns A string representing the formula tree.
				 */
				virtual std::string toString() const {
					std::string result = "(" + left->toString();
					result += " U ";
					result += right->toString() + ")";
					return result;
				}

				/*!
				 * Gets the left child node.
				 *
				 * @returns The left child node.
				 */
				std::shared_ptr<AbstractLtlFormula<T>> const & getLeft() const {
					return left;
				}

				/*!
				 * Gets the right child node.
				 *
				 * @returns The right child node.
				 */
				std::shared_ptr<AbstractLtlFormula<T>> const & getRight() const {
					return right;
				}

				/*!
				 * Sets the left child node.
				 *
				 * @param newLeft The new left child.
				 */
				void setLeft(std::shared_ptr<AbstractLtlFormula<T>> const & newLeft) {
					left = newLeft;
				}

				/*!
				 * Sets the right child node.
				 *
				 * @param newRight The new right child.
				 */
				void setRight(std::shared_ptr<AbstractLtlFormula<T>> const & newRight) {
					right = newRight;
				}

				/*!
				 * Checks if the left child is set, i.e. it does not point to null.
				 *
				 * @return True iff the left child is set.
				 */
				bool isLeftSet() const {
					return left.get() != nullptr;
				}

				/*!
				 * Checks if the right child is set, i.e. it does not point to null.
				 *
				 * @return True iff the right child is set.
				 */
				bool isRightSet() const {
					return right.get() != nullptr;
				}

			private:

				// The left child node.
				std::shared_ptr<AbstractLtlFormula<T>> left;

				// The right child node.
				std::shared_ptr<AbstractLtlFormula<T>> right;
			};

		} // namespace ltl
	} // namespace properties
} // namespace storm

#endif /* STORM_PROPERTIES_LTL_UNTIL_H_ */