diff --git a/src/formula/abstract/AbstractFormula.h b/src/formula/AbstractFormula.h
similarity index 91%
rename from src/formula/abstract/AbstractFormula.h
rename to src/formula/AbstractFormula.h
index ad8122b52..ebe6f6e73 100644
--- a/src/formula/abstract/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -5,25 +5,21 @@
* Author: Thomas Heinemann
*/
-#ifndef STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_
-#define STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_
+#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_
+#define STORM_FORMULA_ABSTRACTFORMULA_H_
#include <string>
namespace storm {
namespace property {
-namespace abstract {
template <class T> class AbstractFormula;
-} //namespace abstract
} //namespace property
} //namespace storm
-
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
namespace property {
-namespace abstract {
//abstract
/*!
@@ -58,7 +54,7 @@ public:
virtual ~AbstractFormula() {
// Intentionally left empty.
}
-
+
/*!
* @brief Return string representation of this formula.
*
@@ -67,7 +63,7 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const = 0;
-
+
/*!
* @brief Checks if all subtrees are valid in some logic.
*
@@ -85,8 +81,7 @@ public:
virtual bool validate(const AbstractFormulaChecker<T>& checker) const = 0;
};
-} // namespace abstract
} // namespace property
} // namespace storm
-#endif /* STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_ */
+#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */
diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index 92858bfac..0f83f3860 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -10,7 +10,7 @@ template <class T> class AbstractFormulaChecker;
} //namespace storm
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
namespace storm {
namespace property {
@@ -64,7 +64,7 @@ class AbstractFormulaChecker {
* @param formula A pointer to some formula object.
* @return true iff the formula is valid.
*/
- virtual bool validate(const storm::property::abstract::AbstractFormula<T>* formula) const = 0;
+ virtual bool validate(const AbstractFormula<T>* formula) const = 0;
};
} // namespace property
diff --git a/src/formula/abstract/IOptimizingOperator.h b/src/formula/IOptimizingOperator.h
similarity index 81%
rename from src/formula/abstract/IOptimizingOperator.h
rename to src/formula/IOptimizingOperator.h
index 53a5f8769..f89419d91 100644
--- a/src/formula/abstract/IOptimizingOperator.h
+++ b/src/formula/IOptimizingOperator.h
@@ -5,12 +5,11 @@
* Author: thomas
*/
-#ifndef STORM_FORMULA_ABSTRACT_IOPTIMIZINGOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_IOPTIMIZINGOPERATOR_H_
+#ifndef STORM_FORMULA_IOPTIMIZINGOPERATOR_H_
+#define STORM_FORMULA_IOPTIMIZINGOPERATOR_H_
namespace storm {
namespace property {
-namespace abstract {
/*!
* @brief Interface for optimizing operators
@@ -20,6 +19,10 @@ namespace abstract {
class IOptimizingOperator {
public:
+ virtual ~IOptimizingOperator() {
+ // Intentionally left empty
+ }
+
/*!
* Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
* @returns True if the operator is an optimizing operator.
@@ -35,7 +38,6 @@ public:
virtual bool isMinimumOperator() const = 0;
};
-} /* namespace abstract */
} /* namespace property */
} /* namespace storm */
-#endif /* IOPTIMIZINGOPERATOR_H_ */
+#endif /* STORM_FORMULA_IOPTIMIZINGOPERATOR_H_ */
diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h
index 65c31bdef..0f03ded32 100644
--- a/src/formula/Ltl/AbstractLtlFormula.h
+++ b/src/formula/Ltl/AbstractLtlFormula.h
@@ -10,7 +10,7 @@
#include <vector>
#include "src/modelchecker/ltl/ForwardDeclarations.h"
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
// Forward declaration for formula visitor
namespace storm {
@@ -35,7 +35,7 @@ namespace ltl {
* Interface class for all LTL root formulas.
*/
template <class T>
-class AbstractLtlFormula : public virtual storm::property::abstract::AbstractFormula<T> {
+class AbstractLtlFormula : public virtual storm::property::AbstractFormula<T> {
public:
/**
* Empty destructor
diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h
index f7c901de3..dee2706f6 100644
--- a/src/formula/Ltl/And.h
+++ b/src/formula/Ltl/And.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_LTL_AND_H_
#include "AbstractLtlFormula.h"
-#include "src/formula/abstract/And.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ltl/ForwardDeclarations.h"
#include <string>
@@ -71,27 +70,29 @@ class IAndVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class And : public storm::property::abstract::And<T, AbstractLtlFormula<T>>, public AbstractLtlFormula<T> {
+class And : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor.
* Will create an AND-node without subnotes. Will not represent a complete formula!
*/
And() {
- //intentionally left empty
+ left = NULL;
+ right = NULL;
}
/*!
* Constructor.
- * Creates an AND node with the parameters as subtrees.
+ * Creates an AND note with the parameters as subtrees.
*
* @param left The left sub formula
* @param right The right sub formula
*/
- And(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
- : storm::property::abstract::And<T, AbstractLtlFormula<T>>(left, right) {
- //intentionally left empty
+ And(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right) {
+ this->left = left;
+ this->right = right;
}
/*!
@@ -101,7 +102,12 @@ public:
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~And() {
- //intentionally left empty
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
}
/*!
@@ -139,6 +145,81 @@ public:
visitor.template as<IAndVisitor>()->visitAnd(*this);
}
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "(";
+ result += left->toString();
+ result += " & ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->left) && checker.validate(this->right);
+ }
+
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(AbstractLtlFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(AbstractLtlFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ const AbstractLtlFormula<T>& getLeft() const {
+ return *left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ const AbstractLtlFormula<T>& getRight() const {
+ return *right;
+ }
+
+ /*!
+ *
+ * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool leftIsSet() const {
+ return left != nullptr;
+ }
+
+ /*!
+ *
+ * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool rightIsSet() const {
+ return right != nullptr;
+ }
+
+private:
+ AbstractLtlFormula<T>* left;
+ AbstractLtlFormula<T>* right;
+
};
} //namespace ltl
diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h
index d5a0069f8..46a5376e1 100644
--- a/src/formula/Ltl/Ap.h
+++ b/src/formula/Ltl/Ap.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_LTL_AP_H_
#include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Ap.h"
namespace storm {
namespace property {
@@ -63,8 +62,7 @@ class IApVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Ap: public storm::property::abstract::Ap<T>,
- public storm::property::ltl::AbstractLtlFormula<T> {
+class Ap: public storm::property::ltl::AbstractLtlFormula<T> {
public:
/*!
* Empty constructor
@@ -80,13 +78,13 @@ public:
*
* @param ap The string representing the atomic proposition
*/
- Ap(std::string ap) :
- storm::property::abstract::Ap<T>(ap) {
- // Intentionally left empty
+ Ap(std::string ap) {
+ this->ap = ap;
}
/*!
* Destructor
+ * At this time, empty...
*/
virtual ~Ap() {
// Intentionally left empty
@@ -121,6 +119,36 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<IApVisitor>()->visitAp(*this);
}
+
+ /*!
+ * @returns a string representation of the leaf.
+ *
+ */
+ virtual std::string toString() const override {
+ return getAp();
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * As atomic propositions have no subformulas, we return true here.
+ *
+ * @param checker Formula checker object.
+ * @return true
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return true;
+ }
+
+ /*!
+ * @returns the name of the atomic proposition
+ */
+ const std::string& getAp() const {
+ return ap;
+ }
+
+private:
+ std::string ap;
};
} /* namespace ltl */
diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h
index 2cbbc4c4a..b37775a0c 100644
--- a/src/formula/Ltl/BoundedEventually.h
+++ b/src/formula/Ltl/BoundedEventually.h
@@ -8,7 +8,6 @@
#ifndef STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
#define STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
-#include "src/formula/abstract/BoundedEventually.h"
#include "AbstractLtlFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include <cstdint>
@@ -72,15 +71,16 @@ class IBoundedEventuallyVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class BoundedEventually : public storm::property::abstract::BoundedEventually<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class BoundedEventually : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
- BoundedEventually() {
- //intentionally left empty
+ BoundedEventually() {
+ this->child = nullptr;
+ bound = 0;
}
/*!
@@ -89,9 +89,9 @@ public:
* @param child The child formula subtree
* @param bound The maximal number of steps
*/
- BoundedEventually(AbstractLtlFormula<T>* child, uint_fast64_t bound) :
- storm::property::abstract::BoundedEventually<T, AbstractLtlFormula<T>>(child, bound){
- //intentionally left empty
+ BoundedEventually(AbstractLtlFormula<T>* child, uint_fast64_t bound) {
+ this->child = child;
+ this->bound = bound;
}
/*!
@@ -101,9 +101,12 @@ public:
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~BoundedEventually() {
- //intentionally left empty
+ if (child != nullptr) {
+ delete child;
+ }
}
+
/*!
* Clones the called object.
*
@@ -137,6 +140,72 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<IBoundedEventuallyVisitor>()->visitBoundedEventually(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "F<=";
+ result += std::to_string(bound);
+ result += " ";
+ result += child->toString();
+ return result;
+ }
+
+ /*!
+ * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->child);
+ }
+
+ /*!
+ * @returns the child node
+ */
+ const AbstractLtlFormula<T>& getChild() const {
+ return *child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(AbstractLtlFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ *
+ * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool childIsSet() const {
+ return child != nullptr;
+ }
+
+ /*!
+ * @returns the maximally allowed number of steps for the bounded until operator
+ */
+ uint_fast64_t getBound() const {
+ return bound;
+ }
+
+ /*!
+ * Sets the maximally allowed number of steps for the bounded until operator
+ *
+ * @param bound the new bound.
+ */
+ void setBound(uint_fast64_t bound) {
+ this->bound = bound;
+ }
+
+
+private:
+ AbstractLtlFormula<T>* child;
+ uint_fast64_t bound;
+
};
} //namespace ltl
diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h
index 8d6f2fcf3..5daf126b8 100644
--- a/src/formula/Ltl/BoundedUntil.h
+++ b/src/formula/Ltl/BoundedUntil.h
@@ -8,8 +8,7 @@
#ifndef STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
#define STORM_FORMULA_LTL_BOUNDEDUNTIL_H_
-#include "src/formula/abstract/BoundedUntil.h"
-#include "AbstractLtlFormula.h"
+#include "src/formula/Ltl/AbstractLtlFormula.h"
#include <cstdint>
#include <string>
#include "src/modelchecker/ltl/ForwardDeclarations.h"
@@ -72,15 +71,17 @@ class IBoundedUntilVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class BoundedUntil : public storm::property::abstract::BoundedUntil<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class BoundedUntil : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
BoundedUntil() {
- //Intentionally left empty
+ this->left = NULL;
+ this->right = NULL;
+ bound = 0;
}
/*!
@@ -91,9 +92,10 @@ public:
* @param bound The maximal number of steps
*/
BoundedUntil(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right,
- uint_fast64_t bound) :
- storm::property::abstract::BoundedUntil<T, AbstractLtlFormula<T>>(left,right,bound) {
- //intentionally left empty
+ uint_fast64_t bound) {
+ this->left = left;
+ this->right = right;
+ this->bound = bound;
}
/*!
@@ -103,19 +105,12 @@ public:
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~BoundedUntil() {
- //intentionally left empty
- }
-
- /*!
- * @brief Return string representation of this formula.
- *
- * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
- * root of a path formula); hence this function is overwritten in this class.
- *
- * @return A string representation of the formula.
- */
- virtual std::string toString() const {
- return "(" + storm::property::abstract::BoundedUntil<T, AbstractLtlFormula<T>>::toString() + ")";
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
}
/*!
@@ -154,6 +149,102 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<IBoundedUntilVisitor>()->visitBoundedUntil(*this);
}
+
+ /*!
+ * @brief Return string representation of this formula.
+ *
+ * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
+ * root of a path formula); hence this function is overwritten in this class.
+ *
+ * @return A string representation of the formula.
+ */
+ virtual std::string toString() const override {
+ std::string result = "(" + left->toString();
+ result += " U<=";
+ result += std::to_string(bound);
+ result += " ";
+ result += right->toString() + ")";
+ return result;
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->left) && checker.validate(this->right);
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(AbstractLtlFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(AbstractLtlFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ const AbstractLtlFormula<T>& getLeft() const {
+ return *left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ const AbstractLtlFormula<T>& getRight() const {
+ return *right;
+ }
+
+ /*!
+ *
+ * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool leftIsSet() const {
+ return left != nullptr;
+ }
+
+ /*!
+ *
+ * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool rightIsSet() const {
+ return right != nullptr;
+ }
+
+ /*!
+ * @returns the maximally allowed number of steps for the bounded until operator
+ */
+ uint_fast64_t getBound() const {
+ return bound;
+ }
+
+ /*!
+ * Sets the maximally allowed number of steps for the bounded until operator
+ *
+ * @param bound the new bound.
+ */
+ void setBound(uint_fast64_t bound) {
+ this->bound = bound;
+ }
+
+private:
+ AbstractLtlFormula<T>* left;
+ AbstractLtlFormula<T>* right;
+ uint_fast64_t bound;
};
} //namespace ltl
diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h
index 2ca73607c..2825292fe 100644
--- a/src/formula/Ltl/Eventually.h
+++ b/src/formula/Ltl/Eventually.h
@@ -8,8 +8,7 @@
#ifndef STORM_FORMULA_LTL_EVENTUALLY_H_
#define STORM_FORMULA_LTL_EVENTUALLY_H_
-#include "src/formula/abstract/Eventually.h"
-#include "AbstractLtlFormula.h"
+#include "src/formula/Ltl/AbstractLtlFormula.h"
#include "src/modelchecker/ltl/ForwardDeclarations.h"
namespace storm {
@@ -69,15 +68,15 @@ class IEventuallyVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Eventually : public storm::property::abstract::Eventually<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class Eventually : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
Eventually() {
- // Intentionally left empty
+ this->child = nullptr;
}
/*!
@@ -85,9 +84,8 @@ public:
*
* @param child The child node
*/
- Eventually(AbstractLtlFormula<T>* child)
- : storm::property::abstract::Eventually<T, AbstractLtlFormula<T>>(child) {
-
+ Eventually(AbstractLtlFormula<T>* child) {
+ this->child = child;
}
/*!
@@ -97,7 +95,9 @@ public:
* (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
*/
virtual ~Eventually() {
- //intentionally left empty
+ if (child != nullptr) {
+ delete child;
+ }
}
/*!
@@ -131,6 +131,51 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<IEventuallyVisitor>()->visitEventually(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "F ";
+ result += child->toString();
+ return result;
+ }
+
+ /*!
+ * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->child);
+ }
+
+ /*!
+ * @returns the child node
+ */
+ const AbstractLtlFormula<T>& getChild() const {
+ return *child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(AbstractLtlFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ *
+ * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool childIsSet() const {
+ return child != nullptr;
+ }
+
+private:
+ AbstractLtlFormula<T>* child;
};
} //namespace ltl
diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h
index 21bacaf14..e4000cc53 100644
--- a/src/formula/Ltl/Globally.h
+++ b/src/formula/Ltl/Globally.h
@@ -8,7 +8,6 @@
#ifndef STORM_FORMULA_LTL_GLOBALLY_H_
#define STORM_FORMULA_LTL_GLOBALLY_H_
-#include "src/formula/abstract/Globally.h"
#include "AbstractLtlFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/ltl/ForwardDeclarations.h"
@@ -70,15 +69,15 @@ class IGloballyVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Globally : public storm::property::abstract::Globally<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class Globally : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
Globally() {
- //intentionally left empty
+ this->child = nullptr;
}
/*!
@@ -86,9 +85,8 @@ public:
*
* @param child The child node
*/
- Globally(AbstractLtlFormula<T>* child)
- : storm::property::abstract::Globally<T, AbstractLtlFormula<T>>(child) {
- //intentionally left empty
+ Globally(AbstractLtlFormula<T>* child) {
+ this->child = child;
}
/*!
@@ -98,10 +96,11 @@ public:
* (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
*/
virtual ~Globally() {
- //intentionally left empty
+ if (child != nullptr) {
+ delete child;
+ }
}
-
/*!
* Clones the called object.
*
@@ -133,6 +132,51 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<IGloballyVisitor>()->visitGlobally(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "G ";
+ result += child->toString();
+ return result;
+ }
+
+ /*!
+ * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->child);
+ }
+
+ /*!
+ * @returns the child node
+ */
+ const AbstractLtlFormula<T>& getChild() const {
+ return *child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(AbstractLtlFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ *
+ * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool childIsSet() const {
+ return child != nullptr;
+ }
+
+ private:
+ AbstractLtlFormula<T>* child;
};
} //namespace ltl
diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h
index 44d98e12f..eb2d5334a 100644
--- a/src/formula/Ltl/Next.h
+++ b/src/formula/Ltl/Next.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_LTL_NEXT_H_
#include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Next.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -69,15 +68,15 @@ class INextVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Next : public storm::property::abstract::Next<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class Next : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
Next() {
- //intentionally left empty
+ this->child = NULL;
}
/*!
@@ -85,9 +84,8 @@ public:
*
* @param child The child node
*/
- Next(AbstractLtlFormula<T>* child)
- : storm::property::abstract::Next<T, AbstractLtlFormula<T>>(child) {
- //intentionally left empty
+ Next(AbstractLtlFormula<T>* child) {
+ this->child = child;
}
/*!
@@ -97,7 +95,9 @@ public:
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~Next() {
- //intentionally left empty
+ if (child != NULL) {
+ delete child;
+ }
}
/*!
@@ -131,6 +131,53 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<INextVisitor>()->visitNext(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "(";
+ result += " X ";
+ result += child->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->child);
+ }
+
+ /*!
+ * @returns the child node
+ */
+ const AbstractLtlFormula<T>& getChild() const {
+ return *child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(AbstractLtlFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ *
+ * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool childIsSet() const {
+ return child != nullptr;
+ }
+
+private:
+ AbstractLtlFormula<T>* child;
};
} //namespace ltl
diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h
index bcf510999..11cac3acf 100644
--- a/src/formula/Ltl/Not.h
+++ b/src/formula/Ltl/Not.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_LTL_NOT_H_
#include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Not.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -66,24 +65,23 @@ class INotVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Not : public storm::property::abstract::Not<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class Not : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
Not() {
- //intentionally left empty
+ this->child = NULL;
}
/*!
* Constructor
* @param child The child node
*/
- Not(AbstractLtlFormula<T>* child) :
- storm::property::abstract::Not<T, AbstractLtlFormula<T>>(child){
- //intentionally left empty
+ Not(AbstractLtlFormula<T>* child) {
+ this->child = child;
}
/*!
@@ -93,7 +91,9 @@ public:
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Not() {
- //intentionally left empty
+ if (child != NULL) {
+ delete child;
+ }
}
/*!
@@ -127,6 +127,51 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<INotVisitor>()->visitNot(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "!";
+ result += child->toString();
+ return result;
+ }
+
+ /*!
+ * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->child);
+ }
+
+ /*!
+ * @returns The child node
+ */
+ const AbstractLtlFormula<T>& getChild() const {
+ return *child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(AbstractLtlFormula<T>* child) {
+ this->child = child;
+ }
+
+ /*!
+ *
+ * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool childIsSet() const {
+ return child != nullptr;
+ }
+
+private:
+ AbstractLtlFormula<T>* child;
};
} //namespace ltl
diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h
index 511420d5d..a11e8fc71 100644
--- a/src/formula/Ltl/Or.h
+++ b/src/formula/Ltl/Or.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_LTL_OR_H_
#include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Or.h"
namespace storm {
namespace property {
@@ -68,34 +67,44 @@ class IOrVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Or: public storm::property::abstract::Or<T, AbstractLtlFormula<T>>,
- public storm::property::ltl::AbstractLtlFormula<T> {
+class Or: public storm::property::ltl::AbstractLtlFormula<T> {
+
public:
+
/*!
- * Empty constructor
+ * Empty constructor.
+ * Will create an AND-node without subnotes. Will not represent a complete formula!
*/
Or() {
- // Intentionally left empty
-
+ left = NULL;
+ right = NULL;
}
/*!
- * Constructor
- * Creates an OR node with the parameters as subtrees.
+ * Constructor.
+ * Creates an AND note with the parameters as subtrees.
*
- * @param left The left subformula
- * @param right The right subformula
+ * @param left The left sub formula
+ * @param right The right sub formula
*/
- Or(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
- : storm::property::abstract::Or<T,AbstractLtlFormula<T>>(left, right) {
- // Intentionally left empty
+ Or(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right) {
+ this->left = left;
+ this->right = right;
}
/*!
- * Destructor
+ * Destructor.
+ *
+ * The subtrees are deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Or() {
- // Intentionally left empty
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
}
/*!
@@ -133,6 +142,79 @@ public:
visitor.template as<IOrVisitor>()->visitOr(*this);
}
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "(";
+ result += left->toString();
+ result += " | ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->left) && checker.validate(this->right);
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(AbstractLtlFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(AbstractLtlFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ const AbstractLtlFormula<T>& getLeft() const {
+ return *left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ const AbstractLtlFormula<T>& getRight() const {
+ return *right;
+ }
+
+ /*!
+ *
+ * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool leftIsSet() const {
+ return left != nullptr;
+ }
+
+ /*!
+ *
+ * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool rightIsSet() const {
+ return right != nullptr;
+ }
+
+private:
+ AbstractLtlFormula<T>* left;
+ AbstractLtlFormula<T>* right;
};
} /* namespace ltl */
diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h
index 359e64a0a..596a654fe 100644
--- a/src/formula/Ltl/Until.h
+++ b/src/formula/Ltl/Until.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_LTL_UNTIL_H_
#include "AbstractLtlFormula.h"
-#include "src/formula/abstract/Until.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -70,15 +69,16 @@ class IUntilVisitor {
* @see AbstractLtlFormula
*/
template <class T>
-class Until : public storm::property::abstract::Until<T, AbstractLtlFormula<T>>,
- public AbstractLtlFormula<T> {
+class Until : public AbstractLtlFormula<T> {
public:
+
/*!
* Empty constructor
*/
Until() {
- // Intentionally left empty
+ this->left = NULL;
+ this->right = NULL;
}
/*!
@@ -87,9 +87,9 @@ public:
* @param left The left formula subtree
* @param right The left formula subtree
*/
- Until(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right)
- : storm::property::abstract::Until<T, AbstractLtlFormula<T>>(left, right) {
- // Intentionally left empty
+ Until(AbstractLtlFormula<T>* left, AbstractLtlFormula<T>* right) {
+ this->left = left;
+ this->right = right;
}
/*!
@@ -99,19 +99,12 @@ public:
* (this behaviour can be prevented by setting the subtrees to NULL before deletion)
*/
virtual ~Until() {
- // Intentionally left empty
- }
-
- /*!
- * @brief Return string representation of this formula.
- *
- * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
- * root of a path formula); hence this function is overwritten in this class.
- *
- * @return A string representation of the formula.
- */
- virtual std::string toString() const {
- return "(" + storm::property::abstract::Until<T, AbstractLtlFormula<T>>::toString() + ")";
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
}
/*!
@@ -148,6 +141,83 @@ public:
virtual void visit(visitor::AbstractLtlFormulaVisitor<T>& visitor) const override {
visitor.template as<IUntilVisitor>()->visitUntil(*this);
}
+
+ /*!
+ * @brief Return string representation of this formula.
+ *
+ * In LTL, brackets are needed around the until, as Until may appear nested (in other logics, Until always is the
+ * root of a path formula); hence this function is overwritten in this class.
+ *
+ * @return A string representation of the formula.
+ */
+ virtual std::string toString() const {
+ std::string result = "(" + left->toString();
+ result += " U ";
+ result += right->toString() + ")";
+ return result;
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->left) && checker.validate(this->right);
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(AbstractLtlFormula<T>* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(AbstractLtlFormula<T>* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ const AbstractLtlFormula<T>& getLeft() const {
+ return *left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ const AbstractLtlFormula<T>& getRight() const {
+ return *right;
+ }
+
+ /*!
+ *
+ * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool leftIsSet() const {
+ return left != nullptr;
+ }
+
+ /*!
+ *
+ * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool rightIsSet() const {
+ return right != nullptr;
+ }
+
+private:
+ AbstractLtlFormula<T>* left;
+ AbstractLtlFormula<T>* right;
};
} //namespace ltl
diff --git a/src/formula/Prctl/AbstractNoBoundOperator.h b/src/formula/Prctl/AbstractNoBoundOperator.h
index c73c4ed6f..4605a590d 100644
--- a/src/formula/Prctl/AbstractNoBoundOperator.h
+++ b/src/formula/Prctl/AbstractNoBoundOperator.h
@@ -8,7 +8,7 @@
#ifndef STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PRCTL_ABSTRACTNOBOUNDOPERATOR_H_
-#include "AbstractPrctlFormula.h"
+#include "src/formula/AbstractFormula.h"
#include "src/formula/abstract/IOptimizingOperator.h"
namespace storm {
@@ -42,8 +42,8 @@ public:
* Interface class for all PRCTL No bound operators
*/
template <class T>
-class AbstractNoBoundOperator: public AbstractPrctlFormula<T>,
- public virtual storm::property::abstract::IOptimizingOperator {
+class AbstractNoBoundOperator: public storm::property::AbstractFormula<T>,
+ public virtual storm::property::IOptimizingOperator {
public:
AbstractNoBoundOperator() {
// Intentionally left empty.
diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h
index c3c2cfc1b..c7e20b9c6 100644
--- a/src/formula/Prctl/AbstractPathFormula.h
+++ b/src/formula/Prctl/AbstractPathFormula.h
@@ -8,11 +8,7 @@
#ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
#define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
-namespace storm { namespace property { namespace prctl {
-template <class T> class AbstractPathFormula;
-}}}
-
-#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
#include "src/modelchecker/prctl/ForwardDeclarations.h"
#include <vector>
@@ -35,7 +31,7 @@ namespace prctl {
* @note This class is intentionally not derived from AbstractPrctlFormula, as path formulas are not complete PRCTL formulas.
*/
template <class T>
-class AbstractPathFormula : public virtual storm::property::abstract::AbstractFormula<T> {
+class AbstractPathFormula : public virtual storm::property::AbstractFormula<T> {
public:
/*!
diff --git a/src/formula/Prctl/AbstractPrctlFormula.h b/src/formula/Prctl/AbstractPrctlFormula.h
deleted file mode 100644
index 8855763a9..000000000
--- a/src/formula/Prctl/AbstractPrctlFormula.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
- * AbstractPrctlFormula.h
- *
- * Created on: 16.04.2013
- * Author: thomas
- */
-
-#ifndef STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_
-#define STORM_FORMULA_PRCTL_ABSTRACTPRCTLFORMULA_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-
-namespace storm {
-namespace property {
-namespace prctl {
-
-/*!
- * Interface class for all PRCTL root formulas.
- */
-template<class T>
-class AbstractPrctlFormula : public virtual storm::property::abstract::AbstractFormula<T> {
-public:
- virtual ~AbstractPrctlFormula() {
- // Intentionally left empty
- }
-};
-
-} /* namespace prctl */
-} /* namespace property */
-} /* namespace storm */
-#endif /* ABSTRACTPRCTLFORMULA_H_ */
diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h
index 0a313bfd1..1142d7754 100644
--- a/src/formula/Prctl/AbstractStateFormula.h
+++ b/src/formula/Prctl/AbstractStateFormula.h
@@ -8,11 +8,7 @@
#ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
#define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
-namespace storm { namespace property { namespace prctl {
-template <class T> class AbstractStateFormula;
-}}}
-
-#include "AbstractPrctlFormula.h"
+#include "src/formula/AbstractFormula.h"
#include "src/storage/BitVector.h"
#include "src/modelchecker/prctl/ForwardDeclarations.h"
@@ -30,7 +26,7 @@ namespace prctl {
* clone().
*/
template <class T>
-class AbstractStateFormula : public AbstractPrctlFormula<T> {
+class AbstractStateFormula : public virtual storm::property::AbstractFormula<T> {
public:
/*!
diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h
index eca17d73d..dcda9e802 100644
--- a/src/formula/Prctl/And.h
+++ b/src/formula/Prctl/And.h
@@ -8,8 +8,7 @@
#ifndef STORM_FORMULA_PRCTL_AND_H_
#define STORM_FORMULA_PRCTL_AND_H_
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/And.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/prctl/ForwardDeclarations.h"
#include <string>
@@ -54,15 +53,17 @@ class IAndModelChecker {
* @see AbstractPrctlFormula
*/
template <class T>
-class And : public storm::property::abstract::And<T, AbstractStateFormula<T>>, public AbstractStateFormula<T> {
+class And : public AbstractStateFormula<T> {
public:
+
/*!
* Empty constructor.
* Will create an AND-node without subnotes. Will not represent a complete formula!
*/
And() {
- //intentionally left empty
+ left = NULL;
+ right = NULL;
}
/*!
@@ -72,9 +73,9 @@ public:
* @param left The left sub formula
* @param right The right sub formula
*/
- And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
- : storm::property::abstract::And<T, AbstractStateFormula<T>>(left, right) {
- //intentionally left empty
+ And(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+ this->left = left;
+ this->right = right;
}
/*!
@@ -84,7 +85,12 @@ public:
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~And() {
- //intentionally left empty
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
}
/*!
@@ -118,6 +124,80 @@ public:
return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
}
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "(";
+ result += left->toString();
+ result += " & ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->left) && checker.validate(this->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;
+ }
+
+ /*!
+ *
+ * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool leftIsSet() const {
+ return left != nullptr;
+ }
+
+ /*!
+ *
+ * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool rightIsSet() const {
+ return right != nullptr;
+ }
+
+private:
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
+
};
} //namespace prctl
diff --git a/src/formula/Prctl/Ap.h b/src/formula/Prctl/Ap.h
index d2df03951..7e234d434 100644
--- a/src/formula/Prctl/Ap.h
+++ b/src/formula/Prctl/Ap.h
@@ -8,8 +8,7 @@
#ifndef STORM_FORMULA_PRCTL_AP_H_
#define STORM_FORMULA_PRCTL_AP_H_
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Ap.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/prctl/ForwardDeclarations.h"
@@ -47,10 +46,10 @@ class IApModelChecker {
* @see AbstractStateFormula
*/
template <class T>
-class Ap : public storm::property::abstract::Ap<T>,
- public AbstractStateFormula<T> {
+class Ap : public AbstractStateFormula<T> {
public:
+
/*!
* Constructor
*
@@ -58,9 +57,8 @@ public:
*
* @param ap The string representing the atomic proposition
*/
- Ap(std::string ap)
- : storm::property::abstract::Ap<T>(ap) {
- // Intentionally left empty
+ Ap(std::string ap) {
+ this->ap = ap;
}
/*!
@@ -95,6 +93,35 @@ public:
return modelChecker.template as<IApModelChecker>()->checkAp(*this);
}
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * As atomic propositions have no subformulas, we return true here.
+ *
+ * @param checker Formula checker object.
+ * @return true
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return true;
+ }
+
+ /*!
+ * @returns the name of the atomic proposition
+ */
+ const std::string& getAp() const {
+ return ap;
+ }
+
+ /*!
+ * @returns a string representation of the leaf.
+ *
+ */
+ virtual std::string toString() const override {
+ return getAp();
+ }
+
+private:
+ std::string ap;
};
} //namespace abstract
diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h
index 7f6a992ab..6859d97b1 100644
--- a/src/formula/Prctl/Not.h
+++ b/src/formula/Prctl/Not.h
@@ -9,7 +9,6 @@
#define STORM_FORMULA_PRCTL_NOT_H_
#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Not.h"
#include "src/formula/AbstractFormulaChecker.h"
#include "src/modelchecker/prctl/ForwardDeclarations.h"
@@ -50,24 +49,22 @@ class INotModelChecker {
* @see AbstractPrctlFormula
*/
template <class T>
-class Not : public storm::property::abstract::Not<T, AbstractStateFormula<T>>,
- public AbstractStateFormula<T> {
+class Not : public AbstractStateFormula<T> {
public:
/*!
* Empty constructor
*/
Not() {
- //intentionally left empty
+ this->child = NULL;
}
/*!
* Constructor
* @param child The child node
*/
- Not(AbstractStateFormula<T>* child) :
- storm::property::abstract::Not<T, AbstractStateFormula<T>>(child){
- //intentionally left empty
+ Not(AbstractStateFormula<T>* child) {
+ this->child = child;
}
/*!
@@ -77,7 +74,9 @@ public:
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Not() {
- //intentionally left empty
+ if (child != NULL) {
+ delete child;
+ }
}
/*!
@@ -107,6 +106,51 @@ public:
virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<INotModelChecker>()->checkNot(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "!";
+ result += child->toString();
+ return result;
+ }
+
+ /*!
+ * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->child);
+ }
+
+ /*!
+ * @returns The child node
+ */
+ const FormulaType& getChild() const {
+ return *child;
+ }
+
+ /*!
+ * Sets the subtree
+ * @param child the new child node
+ */
+ void setChild(FormulaType* child) {
+ this->child = child;
+ }
+
+ /*!
+ *
+ * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool childIsSet() const {
+ return child != nullptr;
+ }
+
+private:
+ AbstractStateFormula<T>* child;
};
} //namespace prctl
diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h
index a13c385e3..cbac0c655 100644
--- a/src/formula/Prctl/Or.h
+++ b/src/formula/Prctl/Or.h
@@ -8,8 +8,7 @@
#ifndef STORM_FORMULA_PRCTL_OR_H_
#define STORM_FORMULA_PRCTL_OR_H_
-#include "AbstractStateFormula.h"
-#include "src/formula/abstract/Or.h"
+#include "src/formula/Prctl/AbstractStateFormula.h"
#include "src/formula/AbstractFormulaChecker.h"
namespace storm {
@@ -52,28 +51,28 @@ class IOrModelChecker {
* @see AbstractPrctlFormula
*/
template <class T>
-class Or : public storm::property::abstract::Or<T, AbstractStateFormula<T>>,
- public AbstractStateFormula<T> {
+class Or : public AbstractStateFormula<T> {
public:
/*!
* Empty constructor.
- * Will create an OR-node without subnotes. The result does not represent a complete formula!
+ * Will create an AND-node without subnotes. Will not represent a complete formula!
*/
Or() {
- //intentionally left empty
+ left = NULL;
+ right = NULL;
}
/*!
* Constructor.
- * Creates an OR note with the parameters as subtrees.
+ * Creates an AND note with the parameters as subtrees.
*
* @param left The left sub formula
* @param right The right sub formula
*/
- Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) :
- storm::property::abstract::Or<T, AbstractStateFormula<T>>(left, right) {
- //intentionally left empty
+ Or(FormulaType* left, FormulaType* right) {
+ this->left = left;
+ this->right = right;
}
/*!
@@ -83,7 +82,12 @@ public:
* (this behavior can be prevented by setting them to NULL before deletion)
*/
virtual ~Or() {
- //intentionally left empty
+ if (left != NULL) {
+ delete left;
+ }
+ if (right != NULL) {
+ delete right;
+ }
}
/*!
@@ -116,6 +120,81 @@ public:
virtual storm::storage::BitVector check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const override {
return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
}
+
+ /*!
+ * @returns a string representation of the formula
+ */
+ virtual std::string toString() const override {
+ std::string result = "(";
+ result += left->toString();
+ result += " | ";
+ result += right->toString();
+ result += ")";
+ return result;
+ }
+
+ /*!
+ * @brief Checks if all subtrees conform to some logic.
+ *
+ * @param checker Formula checker object.
+ * @return true iff all subtrees conform to some logic.
+ */
+ virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
+ return checker.validate(this->left) && checker.validate(this->right);
+ }
+
+ /*!
+ * Sets the left child node.
+ *
+ * @param newLeft the new left child.
+ */
+ void setLeft(FormulaType* newLeft) {
+ left = newLeft;
+ }
+
+ /*!
+ * Sets the right child node.
+ *
+ * @param newRight the new right child.
+ */
+ void setRight(FormulaType* newRight) {
+ right = newRight;
+ }
+
+ /*!
+ * @returns a pointer to the left child node
+ */
+ const FormulaType& getLeft() const {
+ return *left;
+ }
+
+ /*!
+ * @returns a pointer to the right child node
+ */
+ const FormulaType& getRight() const {
+ return *right;
+ }
+
+ /*!
+ *
+ * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool leftIsSet() const {
+ return left != nullptr;
+ }
+
+ /*!
+ *
+ * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
+ */
+ bool rightIsSet() const {
+ return right != nullptr;
+ }
+
+private:
+ AbstractStateFormula<T>* left;
+ AbstractStateFormula<T>* right;
+
};
} //namespace prctl
diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h
index a2ea229aa..6e171a517 100644
--- a/src/formula/Prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticBoundOperator.h
@@ -10,7 +10,6 @@
#include "AbstractStateFormula.h"
#include "AbstractPathFormula.h"
-#include "src/formula/abstract/ProbabilisticBoundOperator.h"
#include "utility/constants.h"
namespace storm {
diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h
deleted file mode 100644
index c2739a9e4..000000000
--- a/src/formula/abstract/And.h
+++ /dev/null
@@ -1,164 +0,0 @@
-/*
- * And.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_AND_H_
-#define STORM_FORMULA_ABSTRACT_AND_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <string>
-#include <type_traits>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Logic-abstract Class for an abstract formula tree with AND node as root.
- *
- * Has two formulas as sub formulas/trees; the type is the template parameter FormulaType
- *
- * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
- * the model checker works.
- *
- * 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 AbstractFormula
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "validate" of the subformulas are needed.
- */
-template <class T, class FormulaType>
-class And : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::And<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
- */
- And() {
- left = NULL;
- right = NULL;
- }
-
- /*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
- *
- * @param left The left sub formula
- * @param right The right sub formula
- */
- And(FormulaType* left, FormulaType* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~And() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(FormulaType* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(FormulaType* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- const FormulaType& getLeft() const {
- return *left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- const FormulaType& getRight() const {
- return *right;
- }
-
- /*!
- *
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool leftIsSet() const {
- return left != nullptr;
- }
-
- /*!
- *
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool rightIsSet() const {
- return right != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "(";
- result += left->toString();
- result += " & ";
- result += right->toString();
- result += ")";
- return result;
- }
-
- /*!
- * @brief Checks if all subtrees conform to some logic.
- *
- * @param checker Formula checker object.
- * @return true iff all subtrees conform to some logic.
- */
- virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->left) && checker.validate(this->right);
- }
-
-
-private:
- FormulaType* left;
- FormulaType* right;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_AND_H_ */
diff --git a/src/formula/abstract/Ap.h b/src/formula/abstract/Ap.h
deleted file mode 100644
index dd0acce82..000000000
--- a/src/formula/abstract/Ap.h
+++ /dev/null
@@ -1,84 +0,0 @@
-/*
- * Ap.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_AP_H_
-#define STORM_FORMULA_ABSTRACT_AP_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Logic-abstract Class for an abstract formula tree with atomic proposition as root.
- *
- * This class represents the leaves in the formula tree.
- *
- * @see AbstractFormula
- */
-template <class T>
-class Ap : public virtual AbstractFormula<T> {
-
-public:
- /*!
- * Constructor
- *
- * Creates a new atomic proposition leaf, with the label Ap
- *
- * @param ap The string representing the atomic proposition
- */
- Ap(std::string ap) {
- this->ap = ap;
- }
-
- /*!
- * Destructor.
- * At this time, empty...
- */
- virtual ~Ap() { }
-
- /*!
- * @returns the name of the atomic proposition
- */
- const std::string& getAp() const {
- return ap;
- }
-
- /*!
- * @returns a string representation of the leaf.
- *
- */
- virtual std::string toString() const override {
- return getAp();
- }
-
- /*!
- * @brief Checks if all subtrees conform to some logic.
- *
- * As atomic propositions have no subformulas, we return true here.
- *
- * @param checker Formula checker object.
- * @return true
- */
- virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
- return true;
- }
-
-private:
- std::string ap;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_ABSTRCT_AP_H_ */
diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h
deleted file mode 100644
index 2970d09d3..000000000
--- a/src/formula/abstract/BoundedEventually.h
+++ /dev/null
@@ -1,151 +0,0 @@
-/*
- * BoundedUntil.h
- *
- * Created on: 27.11.2012
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include <cstdint>
-#include <string>
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedEventually node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff in at most \e bound steps, formula \e child holds.
- *
- * 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "validate" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class BoundedEventually : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::BoundedEventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- BoundedEventually() {
- this->child = nullptr;
- bound = 0;
- }
-
- /*!
- * Constructor
- *
- * @param child The child formula subtree
- * @param bound The maximal number of steps
- */
- BoundedEventually(FormulaType* child, uint_fast64_t bound) {
- this->child = child;
- this->bound = bound;
- }
-
- /*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~BoundedEventually() {
- if (child != nullptr) {
- delete child;
- }
- }
-
- /*!
- * @returns the child node
- */
- const FormulaType& getChild() const {
- return *child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- *
- * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool childIsSet() const {
- return child != nullptr;
- }
-
- /*!
- * @returns the maximally allowed number of steps for the bounded until operator
- */
- uint_fast64_t getBound() const {
- return bound;
- }
-
- /*!
- * Sets the maximally allowed number of steps for the bounded until 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 override {
- std::string result = "F<=";
- result += std::to_string(bound);
- result += " ";
- result += child->toString();
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->child);
- }
-
-
-private:
- FormulaType* child;
- uint_fast64_t bound;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_ */
diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h
deleted file mode 100644
index 749f2305f..000000000
--- a/src/formula/abstract/BoundedNaryUntil.h
+++ /dev/null
@@ -1,175 +0,0 @@
-/*
- * BoundedNaryUntil.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
-#define STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include <cstdint>
-#include <string>
-#include <vector>
-#include <tuple>
-#include <sstream>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedNaryUntil node as root.
- *
- * Has at least two formulas as sub formulas and an interval
- * associated with all but the first sub formula. We'll call the first one
- * \e left and all other one \e right.
- *
- * @par Semantics
- * The formula holds iff \e left holds until eventually any of the \e right
- * formulas holds after a number of steps contained in the interval
- * associated with this formula.
- *
- * 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class BoundedNaryUntil : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::BoundedNaryUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- BoundedNaryUntil() {
- this->left = nullptr;
- this->right = new std::vector<std::tuple<FormulaType*,T,T>>();
- }
-
- /*!
- * Constructor
- *
- * @param left The left formula subtree
- * @param right The left formula subtree
- */
- BoundedNaryUntil(FormulaType* left, std::vector<std::tuple<FormulaType*,T,T>>* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~BoundedNaryUntil() {
- if (left != nullptr) {
- delete left;
- }
- if (right != nullptr) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(FormulaType* newLeft) {
- left = newLeft;
- }
-
- void setRight(std::vector<std::tuple<FormulaType*,T,T>>* newRight) {
- right = newRight;
- }
-
- /*!
- *
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool leftIsSet() const {
- return left != nullptr;
- }
-
- /*!
- *
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool rightIsSet() const {
- return right != nullptr;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void addRight(FormulaType* newRight, T upperBound, T lowerBound) {
- this->right->push_back(std::tuple<FormulaType*,T,T>(newRight, upperBound, lowerBound));
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- const FormulaType& getLeft() const {
- return *left;
- }
-
- /*!
- * @returns a pointer to the right child nodes.
- */
- const std::vector<std::tuple<FormulaType*,T,T>>& getRight() const {
- return *right;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::stringstream result;
- result << "( " << left->toString();
- for (auto it = this->right->begin(); it != this->right->end(); ++it) {
- result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString();
- }
- result << ")";
- return result.str();
- }
-
- /*!
- * @brief Checks if all subtrees conform to some logic.
- *
- * @param checker Formula checker object.
- * @return true iff all subtrees conform to some logic.
- */
- virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
- bool res = checker.validate(this->left);
- for (auto it = this->right->begin(); it != this->right->end(); ++it) {
- res &= checker.validate(std::get<0>(*it));
- }
- return res;
- }
-
-
-private:
- FormulaType* left;
- std::vector<std::tuple<FormulaType*,T,T>>* right;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_ */
diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h
deleted file mode 100644
index 487fb0535..000000000
--- a/src/formula/abstract/BoundedUntil.h
+++ /dev/null
@@ -1,182 +0,0 @@
-/*
- * BoundedUntil.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
-#define STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include <cstdint>
-#include <string>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a BoundedUntil node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
- * \e left holds.
- *
- * 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class BoundedUntil : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::BoundedUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- BoundedUntil() {
- this->left = NULL;
- this->right = NULL;
- bound = 0;
- }
-
- /*!
- * Constructor
- *
- * @param left The left formula subtree
- * @param right The left formula subtree
- * @param bound The maximal number of steps
- */
- BoundedUntil(FormulaType* left, FormulaType* right,
- uint_fast64_t bound) {
- this->left = left;
- this->right = right;
- this->bound = bound;
- }
-
- /*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~BoundedUntil() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(FormulaType* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(FormulaType* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- const FormulaType& getLeft() const {
- return *left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- const FormulaType& getRight() const {
- return *right;
- }
-
- /*!
- *
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool leftIsSet() const {
- return left != nullptr;
- }
-
- /*!
- *
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool rightIsSet() const {
- return right != nullptr;
- }
-
- /*!
- * @returns the maximally allowed number of steps for the bounded until operator
- */
- uint_fast64_t getBound() const {
- return bound;
- }
-
- /*!
- * Sets the maximally allowed number of steps for the bounded until 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 override {
- std::string result = left->toString();
- result += " U<=";
- result += std::to_string(bound);
- result += " ";
- result += right->toString();
- return result;
- }
-
- /*!
- * @brief Checks if all subtrees conform to some logic.
- *
- * @param checker Formula checker object.
- * @return true iff all subtrees conform to some logic.
- */
- virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->left) && checker.validate(this->right);
- }
-
-private:
- FormulaType* left;
- FormulaType* right;
- uint_fast64_t bound;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_ */
diff --git a/src/formula/abstract/CumulativeReward.h b/src/formula/abstract/CumulativeReward.h
deleted file mode 100644
index f347ebd77..000000000
--- a/src/formula/abstract/CumulativeReward.h
+++ /dev/null
@@ -1,101 +0,0 @@
-/*
- * 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 property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an 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 virtual 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 override {
- 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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return true;
- }
-
-private:
- T bound;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */
diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h
deleted file mode 100644
index 3171c559a..000000000
--- a/src/formula/abstract/Eventually.h
+++ /dev/null
@@ -1,125 +0,0 @@
-/*
- * Next.h
- *
- * Created on: 26.12.2012
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
-#define STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with an Eventually node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff eventually \e child holds.
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Eventually : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::Eventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- Eventually() {
- this->child = nullptr;
- }
-
- /*!
- * Constructor
- *
- * @param child The child node
- */
- Eventually(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
- */
- virtual ~Eventually() {
- if (child != nullptr) {
- delete child;
- }
- }
-
- /*!
- * @returns the child node
- */
- const FormulaType& getChild() const {
- return *child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- *
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
- */
- bool childIsSet() const {
- return child != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "F ";
- result += child->toString();
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->child);
- }
-
-private:
- FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_EVENTUALLY_H_ */
diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h
deleted file mode 100644
index 77444c232..000000000
--- a/src/formula/abstract/Globally.h
+++ /dev/null
@@ -1,126 +0,0 @@
-/*
- * Next.h
- *
- * Created on: 26.12.2012
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_GLOBALLY_H_
-#define STORM_FORMULA_ABSTRACT_GLOBALLY_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a Globally node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff globally \e child holds.
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to nullptr before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Globally : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::Globally<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- Globally() {
- this->child = nullptr;
- }
-
- /*!
- * Constructor
- *
- * @param child The child node
- */
- Globally(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
- */
- virtual ~Globally() {
- if (child != nullptr) {
- delete child;
- }
- }
-
- /*!
- * @returns the child node
- */
- const FormulaType& getChild() const {
- return *child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- *
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
- */
- bool childIsSet() const {
- return child != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "G ";
- result += child->toString();
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->child);
- }
-
-private:
- FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_GLOBALLY_H_ */
diff --git a/src/formula/abstract/InstantaneousReward.h b/src/formula/abstract/InstantaneousReward.h
deleted file mode 100644
index 8e2674efb..000000000
--- a/src/formula/abstract/InstantaneousReward.h
+++ /dev/null
@@ -1,101 +0,0 @@
-/*
- * 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 <cstdint>
-#include <string>
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an 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 AbstractFormula
- */
-template <class T>
-class InstantaneousReward : public virtual 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 override {
- 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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return true;
- }
-
-private:
- uint_fast64_t bound;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_INSTANTANEOUSREWARD_H_ */
diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h
deleted file mode 100644
index d4fc9fe94..000000000
--- a/src/formula/abstract/Next.h
+++ /dev/null
@@ -1,128 +0,0 @@
-/*
- * Next.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_NEXT_H_
-#define STORM_FORMULA_ABSTRACT_NEXT_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a Next node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff in the next step, \e child holds
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Next : public virtual AbstractFormula<T> {
-
- // Throw a compiler error when FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::Next<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- Next() {
- this->child = NULL;
- }
-
- /*!
- * Constructor
- *
- * @param child The child node
- */
- Next(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- * Constructor.
- *
- * Also deletes the subtree.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~Next() {
- if (child != NULL) {
- delete child;
- }
- }
-
- /*!
- * @returns the child node
- */
- const FormulaType& getChild() const {
- return *child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- *
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
- */
- bool childIsSet() const {
- return child != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "(";
- result += " X ";
- result += child->toString();
- result += ")";
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->child);
- }
-
-private:
- FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_NEXT_H_ */
diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h
deleted file mode 100644
index bfa24059d..000000000
--- a/src/formula/abstract/Not.h
+++ /dev/null
@@ -1,122 +0,0 @@
-/*
- * Not.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_NOT_H_
-#define STORM_FORMULA_ABSTRACT_NOT_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with NOT node as root.
- *
- * Has one formula as sub formula/tree.
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Not : public virtual AbstractFormula<T> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::Not<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- Not() {
- this->child = NULL;
- }
-
- /*!
- * Constructor
- * @param child The child node
- */
- Not(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- * Destructor
- *
- * Also deletes the subtree
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~Not() {
- if (child != NULL) {
- delete child;
- }
- }
-
- /*!
- * @returns The child node
- */
- const FormulaType& getChild() const {
- return *child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- *
- * @return True if the child node is set, i.e. it does not point to nullptr; false otherwise
- */
- bool childIsSet() const {
- return child != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "!";
- result += child->toString();
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->child);
- }
-
-private:
- FormulaType* child;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_NOT_H_ */
diff --git a/src/formula/abstract/OptimizingOperator.h b/src/formula/abstract/OptimizingOperator.h
deleted file mode 100644
index 46d868a23..000000000
--- a/src/formula/abstract/OptimizingOperator.h
+++ /dev/null
@@ -1,72 +0,0 @@
-#ifndef STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
-
-#include "IOptimizingOperator.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- *
- */
-class OptimizingOperator : public virtual IOptimizingOperator {
-public:
- /*!
- * Empty constructor
- */
- OptimizingOperator() : optimalityOperator(false), minimumOperator(false) {
- }
-
- /*!
- * Constructor
- *
- * @param minimumOperator A flag indicating whether this operator is a minimizing or a maximizing operator.
- */
- OptimizingOperator(bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) {
- }
-
- /*!
- * Destructor
- */
- virtual ~OptimizingOperator() {
- // Intentionally left empty
- }
-
- /*!
- * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator.
- * @returns True if the operator is an optimizing operator.
- */
- virtual bool isOptimalityOperator() const {
- return optimalityOperator;
- }
-
- /*!
- * Retrieves whether the operator is a minimizing operator given that it is an optimality
- * operator.
- * @returns True if the operator is an optimizing operator and it is a minimizing operator and
- * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator.
- */
- virtual bool isMinimumOperator() const {
- return optimalityOperator && minimumOperator;
- }
-
-private:
- // A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
- // over a nondeterministic model.
- bool optimalityOperator;
-
- // In the case this operator is an optimizing operator, this flag indicates whether it is
- // looking for the minimum or the maximum value.
- bool minimumOperator;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_ */
diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h
deleted file mode 100644
index 67ed1e72d..000000000
--- a/src/formula/abstract/Or.h
+++ /dev/null
@@ -1,161 +0,0 @@
-/*
- * Or.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_OR_H_
-#define STORM_FORMULA_ABSTRACT_OR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with OR node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
- * the model checker works.
- *
- * 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Or : public virtual AbstractFormula<T> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::Or<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor.
- * Will create an AND-node without subnotes. Will not represent a complete formula!
- */
- Or() {
- left = NULL;
- right = NULL;
- }
-
- /*!
- * Constructor.
- * Creates an AND note with the parameters as subtrees.
- *
- * @param left The left sub formula
- * @param right The right sub formula
- */
- Or(FormulaType* left, FormulaType* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * The subtrees are deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~Or() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(FormulaType* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(FormulaType* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- const FormulaType& getLeft() const {
- return *left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- const FormulaType& getRight() const {
- return *right;
- }
-
- /*!
- *
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool leftIsSet() const {
- return left != nullptr;
- }
-
- /*!
- *
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool rightIsSet() const {
- return right != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "(";
- result += left->toString();
- result += " | ";
- result += right->toString();
- result += ")";
- return result;
- }
-
- /*!
- * @brief Checks if all subtrees conform to some logic.
- *
- * @param checker Formula checker object.
- * @return true iff all subtrees conform to some logic.
- */
- virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->left) && checker.validate(this->right);
- }
-
-private:
- FormulaType* left;
- FormulaType* right;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_OR_H_ */
diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h
deleted file mode 100644
index f6c1cd956..000000000
--- a/src/formula/abstract/PathBoundOperator.h
+++ /dev/null
@@ -1,194 +0,0 @@
-/*
- * PathBoundOperator.h
- *
- * Created on: 27.12.2012
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/ComparisonType.h"
-
-#include "src/formula/abstract/OptimizingOperator.h"
-
-#include "src/utility/constants.h"
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff the probability that the path formula holds 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathNoBoundOperator
- */
-template<class T, class FormulaType>
-class PathBoundOperator : public virtual AbstractFormula<T>, public OptimizingOperator {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::PathBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Constructor for non-optimizing operator.
- *
- * @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param pathFormula The child node
- */
- PathBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula)
- : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor for optimizing operator.
- *
- * @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param pathFormula The child node
- * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
- */
- PathBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* pathFormula, bool minimumOperator)
- : OptimizingOperator(minimumOperator), comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- *
- * The subtree is deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~PathBoundOperator() {
- if (pathFormula != nullptr) {
- delete pathFormula;
- }
- }
-
- /*!
- * @returns the child node (representation of a formula)
- */
- const FormulaType& getPathFormula () const {
- return *pathFormula;
- }
-
- /*!
- * Sets the child node
- *
- * @param pathFormula the path formula that becomes the new child node
- */
- void setPathFormula(FormulaType* pathFormula) {
- this->pathFormula = pathFormula;
- }
-
- /*!
- *
- * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
- */
- bool pathFormulaIsSet() const {
- return pathFormula != nullptr;
- }
-
- /*!
- * @returns the comparison relation
- */
- const storm::property::ComparisonType getComparisonOperator() const {
- return comparisonOperator;
- }
-
- void setComparisonOperator(storm::property::ComparisonType comparisonOperator) {
- this->comparisonOperator = comparisonOperator;
- }
-
- /*!
- * @returns the bound for the measure
- */
- const T& getBound() const {
- return bound;
- }
-
- /*!
- * Sets the interval in which the probability that the path formula holds may lie in.
- *
- * @param bound The bound for the measure
- */
- void setBound(T bound) {
- this->bound = bound;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "";
- switch (comparisonOperator) {
- case LESS: result += "<"; break;
- case LESS_EQUAL: result += "<="; break;
- case GREATER: result += ">"; break;
- case GREATER_EQUAL: result += ">="; break;
- }
- result += " ";
- result += std::to_string(bound);
- result += " [";
- result += pathFormula->toString();
- result += "]";
- return result;
- }
-
- bool meetsBound(T value) const {
- switch (comparisonOperator) {
- case LESS: return value < bound; break;
- case LESS_EQUAL: return value <= bound; break;
- case GREATER: return value > bound; break;
- case GREATER_EQUAL: return value >= bound; break;
- default: return false;
- }
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->pathFormula);
- }
-
-private:
- storm::property::ComparisonType comparisonOperator;
- T bound;
- FormulaType* pathFormula;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h
deleted file mode 100644
index 1b0af8d1e..000000000
--- a/src/formula/abstract/PathNoBoundOperator.h
+++ /dev/null
@@ -1,160 +0,0 @@
-/*
- * PathNoBoundOperator.h
- *
- * Created on: 27.12.2012
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/abstract/OptimizingOperator.h"
-
-
-namespace storm {
-
-namespace property {
-
-namespace abstract {
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator without declaration of probabilities
- * as root.
- *
- * Checking a formula with this operator as root returns the probabilities that the path formula holds
- * (for each state)
- *
- * Has one 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 checkProbabilisticNoBoundOperator 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathBoundOperator
- */
-template <class T, class FormulaType>
-class PathNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::PathNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-
-public:
- /*!
- * Empty constructor
- */
- PathNoBoundOperator() :
- OptimizingOperator(false) {
- this->pathFormula = nullptr;
- }
-
- /*!
- * Constructor
- *
- * @param pathFormula The child node.
- */
- PathNoBoundOperator(FormulaType* pathFormula) {
- this->pathFormula = pathFormula;
- }
-
- /*!
- * Constructor
- *
- * @param pathFormula The child node.
- * @param minimumOperator A flag indicating whether this operator is a minimizing or a
- * maximizing operator.
- */
- PathNoBoundOperator(FormulaType* pathFormula, bool minimumOperator)
- : OptimizingOperator(minimumOperator) {
- this->pathFormula = pathFormula;
- }
-
- /*!
- * Destructor
- */
- virtual ~PathNoBoundOperator() {
- if (pathFormula != NULL) {
- delete pathFormula;
- }
- }
-
- /*!
- * @returns the child node (representation of an abstract path formula)
- */
- const FormulaType& getPathFormula () const {
- return *pathFormula;
- }
-
- /*!
- * Sets the child node
- *
- * @param pathFormula the path formula that becomes the new child node
- */
- void setPathFormula(FormulaType* pathFormula) {
- this->pathFormula = pathFormula;
- }
-
- /*!
- *
- * @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
- */
- bool pathFormulaIsSet() const {
- return pathFormula != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result;
- if (this->isOptimalityOperator()) {
- if (this->isMinimumOperator()) {
- result += "min";
- } else {
- result += "max";
- }
- }
- result += " = ? [";
- result += this->getPathFormula().toString();
- result += "]";
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->pathFormula);
- }
-
-private:
- FormulaType* pathFormula;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h
deleted file mode 100644
index b326e1c05..000000000
--- a/src/formula/abstract/ProbabilisticBoundOperator.h
+++ /dev/null
@@ -1,114 +0,0 @@
-/*
- * ProbabilisticBoundOperator.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/PathBoundOperator.h"
-#include "src/formula/abstract/OptimizingOperator.h"
-#include "utility/constants.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one Abstract path formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff the probability that the path formula holds 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see AbstractFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
- */
-template<class T, class FormulaType>
-class ProbabilisticBoundOperator : public PathBoundOperator<T, FormulaType> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::ProbabilisticBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- ProbabilisticBoundOperator() : PathBoundOperator<T, FormulaType>
- (LESS_EQUAL, storm::utility::constantZero<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
- */
- ProbabilisticBoundOperator(
- storm::property::ComparisonType comparisonRelation,
- T bound,
- FormulaType* pathFormula)
- : PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- *
- * @param comparisonRelation
- * @param bound
- * @param pathFormula
- * @param minimumOperator
- */
- ProbabilisticBoundOperator(
- storm::property::ComparisonType comparisonRelation,
- T bound,
- FormulaType* pathFormula,
- bool minimumOperator)
- : PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula, minimumOperator){
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- */
- virtual ~ProbabilisticBoundOperator() {
- // Intentionally left empty
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "P ";
- result += PathBoundOperator<T, FormulaType>::toString();
- return result;
- }
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h
deleted file mode 100644
index 7bf01422e..000000000
--- a/src/formula/abstract/ProbabilisticNoBoundOperator.h
+++ /dev/null
@@ -1,104 +0,0 @@
-/*
- * ProbabilisticNoBoundOperator.h
- *
- * Created on: 12.12.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "PathNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator without declaration of probabilities
- * as root.
- *
- * Checking a formula with this operator as root returns the probabilities that the path formula holds
- * (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 checkProbabilisticNoBoundOperator 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathNoBoundOperator
- * @see ProbabilisticBoundOperator
- */
-template <class T, class FormulaType>
-class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::ProbabilisticNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- ProbabilisticNoBoundOperator() : PathNoBoundOperator<T, FormulaType>(nullptr) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- *
- * @param pathFormula The child node.
- */
- ProbabilisticNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T, FormulaType>(pathFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- */
- virtual ~ProbabilisticNoBoundOperator() {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- *
- * @param pathFormula The child node.
- */
- ProbabilisticNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T, FormulaType>(pathFormula, minimumOperator) {
- // Intentionally left empty
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "P";
- result += PathNoBoundOperator<T, FormulaType>::toString();
- return result;
- }
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/RewardBoundOperator.h b/src/formula/abstract/RewardBoundOperator.h
deleted file mode 100644
index 30d2f3221..000000000
--- a/src/formula/abstract/RewardBoundOperator.h
+++ /dev/null
@@ -1,106 +0,0 @@
-/*
- * 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/constants.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathBoundOperator
- * @see RewardNoBoundOperator
- */
-template<class T, class FormulaType>
-class RewardBoundOperator : public PathBoundOperator<T, FormulaType> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::RewardBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- RewardBoundOperator() : PathBoundOperator<T, FormulaType>(LESS_EQUAL, storm::utility::constantZero<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(
- storm::property::ComparisonType comparisonRelation,
- T bound,
- FormulaType* pathFormula) :
- PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- * @param comparisonRelation
- * @param bound
- * @param pathFormula
- * @param minimumOperator
- */
- RewardBoundOperator(
- storm::property::ComparisonType comparisonRelation,
- T bound,
- FormulaType* pathFormula,
- bool minimumOperator)
- : PathBoundOperator<T, FormulaType>(comparisonRelation, bound, pathFormula, minimumOperator) {
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- */
- virtual ~RewardBoundOperator() {
- // Intentionally left empty
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "R ";
- result += PathBoundOperator<T, FormulaType>::toString();
- return result;
- }
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_REWARDBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/RewardNoBoundOperator.h b/src/formula/abstract/RewardNoBoundOperator.h
deleted file mode 100644
index a147502d8..000000000
--- a/src/formula/abstract/RewardNoBoundOperator.h
+++ /dev/null
@@ -1,103 +0,0 @@
-/*
- * 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 property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an 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 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see PathNoBoundOperator
- * @see RewardBoundOperator
- */
-template <class T, class FormulaType>
-class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::RewardNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- RewardNoBoundOperator() : PathNoBoundOperator<T, FormulaType>(nullptr) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- *
- * @param pathFormula The child node.
- */
- RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T, FormulaType>(pathFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- *
- * @param pathFormula The child node.
- */
- RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T, FormulaType>(pathFormula, minimumOperator) {
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- */
- virtual ~RewardNoBoundOperator() {
- // Intentionally left empty
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "R";
- result += PathNoBoundOperator<T, FormulaType>::toString();
- return result;
- }
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_REWARDNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h
deleted file mode 100644
index c274bd2b3..000000000
--- a/src/formula/abstract/StateBoundOperator.h
+++ /dev/null
@@ -1,174 +0,0 @@
-/*
- * BoundOperator.h
- *
- * Created on: 27.12.2012
- * Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/ComparisonType.h"
-#include "src/utility/constants.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one formula as sub formula/tree.
- *
- * @par Semantics
- * The formula holds iff the probability that the state formula holds 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see StateNoBoundOperator
- */
-template<class T, class FormulaType>
-class StateBoundOperator : public virtual AbstractFormula<T> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::StateBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
-
- /*!
- * Constructor
- *
- * @param comparisonOperator The relation for the bound.
- * @param bound The bound for the probability
- * @param stateFormula The child node
- */
- StateBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, FormulaType* stateFormula)
- : comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- *
- * The subtree is deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- */
- virtual ~StateBoundOperator() {
- if (stateFormula != nullptr) {
- delete stateFormula;
- }
- }
-
- /*!
- * @returns the child node (representation of a formula)
- */
- const FormulaType& getStateFormula () const {
- return *stateFormula;
- }
-
- /*!
- * Sets the child node
- *
- * @param stateFormula the state formula that becomes the new child node
- */
- void setStateFormula(FormulaType* stateFormula) {
- this->stateFormula = stateFormula;
- }
-
- /*!
- *
- * @return True if the state formula is set, i.e. it does not point to nullptr; false otherwise
- */
- bool stateFormulaIsSet() const {
- return stateFormula != nullptr;
- }
-
- /*!
- * @returns the comparison relation
- */
- const ComparisonType getComparisonOperator() const {
- return comparisonOperator;
- }
-
- void setComparisonOperator(ComparisonType comparisonOperator) {
- this->comparisonOperator = comparisonOperator;
- }
-
- /*!
- * @returns the bound for the measure
- */
- const T& getBound() const {
- return bound;
- }
-
- /*!
- * Sets the interval in which the probability that the path formula holds may lie in.
- *
- * @param bound The bound for the measure
- */
- void setBound(T bound) {
- this->bound = bound;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = " ";
- switch (comparisonOperator) {
- case LESS: result += "< "; break;
- case LESS_EQUAL: result += "<= "; break;
- case GREATER: result += "> "; break;
- case GREATER_EQUAL: result += ">= "; break;
- }
- result += std::to_string(bound);
- result += " [";
- result += stateFormula->toString();
- result += "]";
- return result;
- }
-
- bool meetsBound(T value) const {
- switch (comparisonOperator) {
- case LESS: return value < bound; break;
- case LESS_EQUAL: return value <= bound; break;
- case GREATER: return value > bound; break;
- case GREATER_EQUAL: return value >= bound; break;
- default: return false;
- }
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->stateFormula);
- }
-
-private:
- ComparisonType comparisonOperator;
- T bound;
- FormulaType* stateFormula;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h
deleted file mode 100644
index 4780f2587..000000000
--- a/src/formula/abstract/StateNoBoundOperator.h
+++ /dev/null
@@ -1,126 +0,0 @@
-/*
- * StateNoBoundOperator.h
- *
- * Created on: 09.04.2013
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
-
-#include "AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with an operator without declaration of bounds.
- * as root.
- *
- * Checking a formula with this operator as root returns the probabilities that the path formula holds
- * (for each state)
- *
- * Has one 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 checkProbabilisticNoBoundOperator 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- * @see StateBoundOperator
- */
-template <class T, class FormulaType>
-class StateNoBoundOperator: public virtual AbstractFormula<T>, public OptimizingOperator {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::StateNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- StateNoBoundOperator() {
- stateFormula = nullptr;
- }
-
- /*!
- * Constructor
- */
- StateNoBoundOperator(FormulaType* stateFormula) {
- this->stateFormula = stateFormula;
- }
-
- /*!
- * Destructor
- *
- * Deletes the subtree
- */
- virtual ~StateNoBoundOperator() {
- if (stateFormula != nullptr) {
- delete stateFormula;
- }
- }
-
- const FormulaType& getStateFormula() const {
- return *(this->stateFormula);
- }
-
- void setStateFormula(FormulaType* stateFormula) {
- this->stateFormula = stateFormula;
- }
-
- /*!
- *
- * @return True if the state formula is set, i.e. it does not point to nullptr; false otherwise
- */
- bool stateFormulaIsSet() const {
- return stateFormula != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result;
- result += " = ? [";
- result += this->getStateFormula().toString();
- result += "]";
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->stateFormula);
- }
-
-private:
- FormulaType* stateFormula;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-#endif /* STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/SteadyStateBoundOperator.h b/src/formula/abstract/SteadyStateBoundOperator.h
deleted file mode 100644
index a25e7d280..000000000
--- a/src/formula/abstract/SteadyStateBoundOperator.h
+++ /dev/null
@@ -1,77 +0,0 @@
-/*
- * SteadyState.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_
-
-#include "StateBoundOperator.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an Abstract (path) formula tree with a SteadyStateOperator node as root.
- *
- * Has two formulas as sub formulas/trees.
- *
- * @par Semantics
- * The formula holds iff \e child holds SteadyStateOperator step, \e child holds
- *
- * The subtree is seen as part of the object and deleted with the object
- * (this behavior can be prevented by setting them to NULL before deletion)
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class SteadyStateBoundOperator : public StateBoundOperator<T, FormulaType> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::SteadyStateBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- SteadyStateBoundOperator() : StateBoundOperator<T, FormulaType>
- (LESS_EQUAL, storm::utility::constantZero<T>(), nullptr) {
- // Intentionally left empty
- }
-
- /*!
- * Constructor
- *
- * @param stateFormula The child node
- */
- SteadyStateBoundOperator(
- storm::property::ComparisonType comparisonRelation, T bound, FormulaType* stateFormula) :
- StateBoundOperator<T, FormulaType>(comparisonRelation, bound, stateFormula) {
- }
-
- /*!
- * Destructor
- */
- virtual ~SteadyStateBoundOperator() {
- // Intentionally left empty
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- return "S" + StateBoundOperator<T, FormulaType>::toString();
- }
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEOPERATOR_H_ */
diff --git a/src/formula/abstract/SteadyStateNoBoundOperator.h b/src/formula/abstract/SteadyStateNoBoundOperator.h
deleted file mode 100644
index 6e544d207..000000000
--- a/src/formula/abstract/SteadyStateNoBoundOperator.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/*
- * SteadyStateNoBoundOperator.h
- *
- * Created on: 09.04.2013
- * Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_
-
-#include "StateNoBoundOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract formula tree with a steady state operator as root, without explicit declaration of bounds.
- *
- * Checking a formula with this operator as root returns the exact bound parameter for the corresponding subformula.
- * (for each state)
- *
- * Has one formula as sub formula/tree.
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- */
-template <class T, class FormulaType>
-class SteadyStateNoBoundOperator: public StateNoBoundOperator<T, FormulaType> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::SteadyStateNoBoundOperator<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- SteadyStateNoBoundOperator() : StateNoBoundOperator<T, FormulaType>() {
- // Intentionally left empty
-
- }
-
- /*!
- * Constructor
- *
- * @param stateFormula The state formula that forms the subtree
- */
- SteadyStateNoBoundOperator(FormulaType* stateFormula)
- : StateNoBoundOperator<T, FormulaType>(stateFormula) {
- // Intentionally left empty
- }
-
- /*!
- * Destructor
- */
- virtual ~SteadyStateNoBoundOperator() {
- // Intentionally left empty
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- return "S" + StateNoBoundOperator<T, FormulaType>::toString();
- }
-
-};
-
-} /* namespace abstract */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATENOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/SteadyStateReward.h b/src/formula/abstract/SteadyStateReward.h
deleted file mode 100644
index d5f344752..000000000
--- a/src/formula/abstract/SteadyStateReward.h
+++ /dev/null
@@ -1,62 +0,0 @@
-/*
- * 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 property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with a Steady State Reward node as root.
- *
- * @see AbstractFormula
- */
-template <class T>
-class SteadyStateReward: public virtual 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 override {
- 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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return true;
- }
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-#endif /* STORM_FORMULA_ABSTRACT_STEADYSTATEREWARD_H_ */
diff --git a/src/formula/abstract/TimeBoundedEventually.h b/src/formula/abstract/TimeBoundedEventually.h
deleted file mode 100644
index eaecaa868..000000000
--- a/src/formula/abstract/TimeBoundedEventually.h
+++ /dev/null
@@ -1,107 +0,0 @@
-/*
- * TimeBoundedEventually.h
- *
- * Created on: 10.04.2013
- * Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_
-
-#include "TimeBoundedOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * Class for a formula tree with a time bounded eventually operator as root.
- *
- * Has two subformulas.
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- */
-template<class T, class FormulaType>
-class TimeBoundedEventually: public storm::property::abstract::TimeBoundedOperator<T> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::TimeBoundedEventually<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<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, FormulaType* child) :
- TimeBoundedOperator<T>(lowerBound, upperBound) {
- this->child = child;
- }
-
- virtual ~TimeBoundedEventually() {
- if (child != nullptr) {
- delete child;
- }
- }
-
- /*!
- * @returns the child node
- */
- const FormulaType& getChild() const {
- return *child;
- }
-
- /*!
- * Sets the subtree
- * @param child the new child node
- */
- void setChild(FormulaType* child) {
- this->child = child;
- }
-
- /*!
- *
- * @return True if the child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool childIsSet() const {
- return child != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = "F";
- result += TimeBoundedOperator<T>::toString();
- result += " ";
- result += child->toString();
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->child);
- }
-
-private:
- FormulaType* child;
-};
-
-} /* namespace abstract */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDEVENTUALLY_H_ */
diff --git a/src/formula/abstract/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h
deleted file mode 100644
index d26fea552..000000000
--- a/src/formula/abstract/TimeBoundedOperator.h
+++ /dev/null
@@ -1,112 +0,0 @@
-/*
- * TimeBoundedOperator.h
- *
- * Created on: 10.04.2013
- * Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
-#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
-
-#include <limits>
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "exceptions/InvalidArgumentException.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an 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 concrete subclasses of this abstract class.
- *
- *
- * @see AbstractFormula
- * @see AbstractFormula
- * @see AbstractFormula
- */
-template<class T>
-class TimeBoundedOperator: public virtual AbstractFormula<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 override {
- std::string result = "";
- if (upperBound == std::numeric_limits<double>::infinity()) {
- result = ">=" + std::to_string(lowerBound);
- } else {
- result = "[";
- result += std::to_string(lowerBound);
- result += ",";
- result += std::to_string(upperBound);
- result += "]";
- }
- return result;
- }
-
-private:
- T lowerBound, upperBound;
-};
-
-} //namespace abstract
-} //namespace property
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_ */
diff --git a/src/formula/abstract/TimeBoundedUntil.h b/src/formula/abstract/TimeBoundedUntil.h
deleted file mode 100644
index 936baeef4..000000000
--- a/src/formula/abstract/TimeBoundedUntil.h
+++ /dev/null
@@ -1,149 +0,0 @@
-/*
- * TimeBoundedUntil.h
- *
- * Created on: 10.04.2013
- * Author: thomas
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_
-#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_
-
-#include "TimeBoundedOperator.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-
-/**
- * @brief
- * Class for an abstract formula tree with an time bounded until operator as root.
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- */
-template <class T, class FormulaType>
-class TimeBoundedUntil: public TimeBoundedOperator<T> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::TimeBoundedUntil<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<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, FormulaType* left, FormulaType* 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(FormulaType* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(FormulaType* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- const FormulaType& getLeft() const {
- return *left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- const FormulaType& getRight() const {
- return *right;
- }
-
- /*!
- *
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool leftIsSet() const {
- return left != nullptr;
- }
-
- /*!
- *
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool rightIsSet() const {
- return right != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = left->toString();
- result += " U";
- result += TimeBoundedOperator<T>::toString();
- result += " ";
- result += right->toString();
- return result;
- }
-
- /*!
- * @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 validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->left) && checker.validate(this->right);
- }
-
-private:
- FormulaType* left;
- FormulaType* right;
-};
-
-} /* namespace abstract */
-} /* namespace property */
-} /* namespace storm */
-
-#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDUNTIL_H_ */
diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h
deleted file mode 100644
index dd093de88..000000000
--- a/src/formula/abstract/Until.h
+++ /dev/null
@@ -1,159 +0,0 @@
-/*
- * Until.h
- *
- * Created on: 19.10.2012
- * Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_ABSTRACT_UNTIL_H_
-#define STORM_FORMULA_ABSTRACT_UNTIL_H_
-
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/abstract/AbstractFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-namespace storm {
-namespace property {
-namespace abstract {
-
-/*!
- * @brief
- * Class for an abstract (path) formula tree with an Until node as root.
- *
- * Has two 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 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)
- *
- * @tparam FormulaType The type of the subformula.
- * The instantiation of FormulaType should be a subclass of AbstractFormula, as the functions
- * "toString" and "conforms" of the subformulas are needed.
- *
- * @see AbstractFormula
- */
-template <class T, class FormulaType>
-class Until : public virtual AbstractFormula<T> {
-
- // Throw a compiler error if FormulaType is not a subclass of AbstractFormula.
- static_assert(std::is_base_of<AbstractFormula<T>, FormulaType>::value,
- "Instantiaton of FormulaType for storm::property::abstract::Until<T,FormulaType> has to be a subtype of storm::property::abstract::AbstractFormula<T>");
-
-public:
- /*!
- * Empty constructor
- */
- Until() {
- this->left = NULL;
- this->right = NULL;
- }
-
- /*!
- * Constructor
- *
- * @param left The left formula subtree
- * @param right The left formula subtree
- */
- Until(FormulaType* left, FormulaType* right) {
- this->left = left;
- this->right = right;
- }
-
- /*!
- * Destructor.
- *
- * Also deletes the subtrees.
- * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
- */
- virtual ~Until() {
- if (left != NULL) {
- delete left;
- }
- if (right != NULL) {
- delete right;
- }
- }
-
- /*!
- * Sets the left child node.
- *
- * @param newLeft the new left child.
- */
- void setLeft(FormulaType* newLeft) {
- left = newLeft;
- }
-
- /*!
- * Sets the right child node.
- *
- * @param newRight the new right child.
- */
- void setRight(FormulaType* newRight) {
- right = newRight;
- }
-
- /*!
- * @returns a pointer to the left child node
- */
- const FormulaType& getLeft() const {
- return *left;
- }
-
- /*!
- * @returns a pointer to the right child node
- */
- const FormulaType& getRight() const {
- return *right;
- }
-
- /*!
- *
- * @return True if the left child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool leftIsSet() const {
- return left != nullptr;
- }
-
- /*!
- *
- * @return True if the right child is set, i.e. it does not point to nullptr; false otherwise
- */
- bool rightIsSet() const {
- return right != nullptr;
- }
-
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const override {
- std::string result = left->toString();
- result += " U ";
- result += right->toString();
- return result;
- }
-
- /*!
- * @brief Checks if all subtrees conform to some logic.
- *
- * @param checker Formula checker object.
- * @return true iff all subtrees conform to some logic.
- */
- virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
- return checker.validate(this->left) && checker.validate(this->right);
- }
-
-private:
- FormulaType* left;
- FormulaType* right;
-};
-
-} //namespace abstract
-
-} //namespace property
-
-} //namespace storm
-
-#endif /* STORM_FORMULA_ABSTRACT_UNTIL_H_ */