diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
index c7801e0e2..5bd7185db 100644
--- a/src/formula/AbstractFormulaChecker.h
+++ b/src/formula/AbstractFormulaChecker.h
@@ -1,7 +1,7 @@
#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
-#include "src/formula/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
namespace storm {
namespace formula {
diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h
index 84e78e669..103c5e968 100644
--- a/src/formula/Prctl/And.h
+++ b/src/formula/Prctl/And.h
@@ -96,11 +96,11 @@ public:
*/
virtual AbstractStateFormula<T>* clone() const {
And<T>* result = new And();
- if (this->left != NULL) {
- result->setLeft(left->clone());
+ if (this->leftIsSet()) {
+ result->setLeft(this->getLeft().clone());
}
- if (this->right != NULL) {
- result->setRight(right->clone());
+ if (this->rightIsSet()) {
+ result->setRight(this->getRight().clone());
}
return result;
}
diff --git a/src/formula/Prctl/Ap.h b/src/formula/Prctl/Ap.h
index 3b187543a..c99dc4886 100644
--- a/src/formula/Prctl/Ap.h
+++ b/src/formula/Prctl/Ap.h
@@ -47,7 +47,7 @@ class IApModelChecker {
* @see AbstractFormula
*/
template <class T>
-class Ap : public storm::formula::abstract::Ap<T>, public AbstractFormula<T> {
+class Ap : public storm::formula::abstract::Ap<T>, public AbstractStateFormula<T> {
public:
/*!
@@ -78,7 +78,7 @@ public:
* @returns a new AND-object that is identical the called object.
*/
virtual AbstractStateFormula<T>* clone() const {
- return new Ap(getAp());
+ return new Ap(this->getAp());
}
/*!
diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h
index 03f31f634..f9f18b72e 100644
--- a/src/formula/Prctl/BoundedEventually.h
+++ b/src/formula/Prctl/BoundedEventually.h
@@ -97,9 +97,9 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
BoundedEventually<T>* result = new BoundedEventually<T>();
- result->setBound(bound);
- if (child != nullptr) {
- result->setChild(child->clone());
+ result->setBound(this->getBound());
+ if (this->childIsSet()) {
+ result->setChild(this->getChild().clone());
}
return result;
}
diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h
index 4dc17bec1..e3e7a63dd 100644
--- a/src/formula/Prctl/BoundedNaryUntil.h
+++ b/src/formula/Prctl/BoundedNaryUntil.h
@@ -105,10 +105,10 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>();
- if (left != NULL) {
- result->setLeft(left->clone());
+ if (this->leftIsSet()) {
+ result->setLeft(this->getLeft().clone());
}
- if (right != NULL) {
+ if (this->rightIsSet()) {
std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newright = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
for (auto it = this->right->begin(); it != this->right->end(); ++it) {
newright->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it)));
diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h
index 0664f4ce1..ae13597d4 100644
--- a/src/formula/Prctl/BoundedUntil.h
+++ b/src/formula/Prctl/BoundedUntil.h
@@ -56,7 +56,7 @@ class IBoundedUntilModelChecker {
* @see AbstractFormula
*/
template <class T>
-class BoundedUntil : public storm::formula::abstract::BoundedUntil<T, AbstractStateFormula>,
+class BoundedUntil : public storm::formula::abstract::BoundedUntil<T, AbstractStateFormula<T>>,
public AbstractPathFormula<T> {
public:
@@ -76,7 +76,7 @@ public:
*/
BoundedUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
uint_fast64_t bound) :
- storm::formula::abstract::BoundedUntil<T, AbstractStateFormula>(left,right,bound) {
+ storm::formula::abstract::BoundedUntil<T, AbstractStateFormula<T>>(left,right,bound) {
//intentionally left empty
}
@@ -99,12 +99,12 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
BoundedUntil<T>* result = new BoundedUntil<T>();
- result->setBound(bound);
- if (left != NULL) {
- result->setLeft(left->clone());
+ result->setBound(this->getBound());
+ if (this->leftIsSet()) {
+ result->setLeft(this->getLeft().clone());
}
- if (right != NULL) {
- result->setRight(right->clone());
+ if (this->rightIsSet()) {
+ result->setRight(this->getRight().clone());
}
return result;
}
diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h
index 75c4df2ac..6b15533ed 100644
--- a/src/formula/Prctl/Eventually.h
+++ b/src/formula/Prctl/Eventually.h
@@ -93,8 +93,8 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
Eventually<T>* result = new Eventually<T>();
- if (child != nullptr) {
- result->setChild(child);
+ if (this->childIsSet()) {
+ result->setChild(this->getChild().clone());
}
return result;
}
diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h
index 14cbdec41..65ef1004a 100644
--- a/src/formula/Prctl/Globally.h
+++ b/src/formula/Prctl/Globally.h
@@ -94,9 +94,9 @@ public:
* @returns a new Globally-object that is identical the called object.
*/
virtual AbstractPathFormula<T>* clone() const {
- Next<T>* result = new Next<T>();
- if (child != nullptr) {
- result->setChild(child);
+ Globally<T>* result = new Globally<T>();
+ if (this->childIsSet()) {
+ result->setChild(this->getChild().clone());
}
return result;
}
diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h
index c88534c10..c48789599 100644
--- a/src/formula/Prctl/InstantaneousReward.h
+++ b/src/formula/Prctl/InstantaneousReward.h
@@ -50,7 +50,7 @@ class IInstantaneousRewardModelChecker {
* @see AbstractFormula
*/
template <class T>
-class InstantaneousReward : public storm::formula::abstract::InstantaneousReward,
+class InstantaneousReward : public storm::formula::abstract::InstantaneousReward<T>,
public AbstractPathFormula<T> {
public:
@@ -86,7 +86,7 @@ public:
* @returns a new InstantaneousReward-object that is identical the called object.
*/
virtual AbstractPathFormula<T>* clone() const {
- return new InstantaneousReward(bound);
+ return new InstantaneousReward(this->getBound());
}
diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h
index e81be5887..19f2e95c2 100644
--- a/src/formula/Prctl/Next.h
+++ b/src/formula/Prctl/Next.h
@@ -93,8 +93,8 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
Next<T>* result = new Next<T>();
- if (child != NULL) {
- result->setChild(child);
+ if (this->childIsSet()) {
+ result->setChild(this->getChild().clone());
}
return result;
}
diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h
index 17bc27708..e2139f308 100644
--- a/src/formula/Prctl/Not.h
+++ b/src/formula/Prctl/Not.h
@@ -89,8 +89,8 @@ public:
*/
virtual AbstractStateFormula<T>* clone() const {
Not<T>* result = new Not<T>();
- if (child != NULL) {
- result->setChild(getChild().clone());
+ if (this->childIsSet()) {
+ result->setChild(this->getChild().clone());
}
return result;
}
diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h
index ecf1202f9..24c104407 100644
--- a/src/formula/Prctl/Or.h
+++ b/src/formula/Prctl/Or.h
@@ -95,11 +95,11 @@ public:
*/
virtual AbstractStateFormula<T>* clone() const {
Or<T>* result = new Or();
- if (this->left != NULL) {
- result->setLeft(getLeft().clone());
+ if (this->leftIsSet()) {
+ result->setLeft(this->getLeft().clone());
}
- if (this->right != NULL) {
- result->setRight(getLeft().clone());
+ if (this->rightIsSet()) {
+ result->setRight(this->getRight().clone());
}
return result;
}
diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h
index 70e5c8ad5..37b3305b3 100644
--- a/src/formula/Prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticBoundOperator.h
@@ -54,14 +54,13 @@ class IProbabilisticBoundOperatorModelChecker {
*/
template<class T>
class ProbabilisticBoundOperator : public storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>,
- public AbstractStateFormula {
+ public AbstractStateFormula<T> {
public:
/*!
* Empty constructor
*/
- ProbabilisticBoundOperator() : PathBoundOperator<T>
- (PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+ ProbabilisticBoundOperator() {
// Intentionally left empty
}
@@ -74,8 +73,10 @@ public:
* @param pathFormula The child node
*/
ProbabilisticBoundOperator(
- typename storm::formula::abstract::PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
- : storm::formula::abstract::ProbabilisticBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+ typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+ T bound,
+ AbstractPathFormula<T>* pathFormula)
+ : storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
// Intentionally left empty
}
@@ -87,8 +88,11 @@ public:
* @param minimumOperator
*/
ProbabilisticBoundOperator(
- typename storm::formula::abstract::PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
- : storm::formula::abstract::ProbabilisticBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
+ typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+ T bound,
+ AbstractPathFormula<T>* pathFormula,
+ bool minimumOperator)
+ : storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula, minimumOperator){
// Intentionally left empty
}
diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
index de444bd3c..9f55d1397 100644
--- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
@@ -8,7 +8,6 @@
#ifndef STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
-#include "AbstractFormula.h"
#include "AbstractPathFormula.h"
#include "src/formula/abstract/ProbabilisticNoBoundOperator.h"
diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h
index 1e182aabc..ee24d2e8e 100644
--- a/src/formula/Prctl/ReachabilityReward.h
+++ b/src/formula/Prctl/ReachabilityReward.h
@@ -90,8 +90,8 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
ReachabilityReward<T>* result = new ReachabilityReward<T>();
- if (getChild() != nullptr) {
- result->setChild(*getChild());
+ if (this->childIsSet()) {
+ result->setChild(this->getChild().clone());
}
return result;
}
diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h
index 67389bde4..0e2f06e61 100644
--- a/src/formula/Prctl/RewardBoundOperator.h
+++ b/src/formula/Prctl/RewardBoundOperator.h
@@ -57,11 +57,14 @@ public:
* @param pathFormula The child node
*/
RewardBoundOperator(
- typename storm::formula::abstract::PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
- storm::formula::abstract::RewardBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+ typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+ T bound,
+ AbstractPathFormula<T>* pathFormula) :
+ storm::formula::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula) {
// Intentionally left empty
}
+
/*!
* Constructor
*
@@ -71,8 +74,11 @@ public:
* @param minimumOperator
*/
RewardBoundOperator(
- typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
- : PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator) {
+ typename storm::formula::abstract::PathBoundOperator<T, AbstractPathFormula<T>>::ComparisonType comparisonRelation,
+ T bound,
+ AbstractPathFormula<T>* pathFormula,
+ bool minimumOperator)
+ : storm::formula::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>(comparisonRelation, bound, pathFormula, minimumOperator) {
// Intentionally left empty
}
diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h
index 76ca979c1..9f597c6ad 100644
--- a/src/formula/Prctl/RewardNoBoundOperator.h
+++ b/src/formula/Prctl/RewardNoBoundOperator.h
@@ -8,8 +8,8 @@
#ifndef STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
#define STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
-#include "AbstractFormula.h"
-#include "PathNoBoundOperator.h"
+#include "AbstractPathFormula.h"
+#include "src/formula/abstract/RewardNoBoundOperator.h"
namespace storm {
namespace formula {
@@ -45,13 +45,13 @@ namespace prctl {
* @see ProbabilisticIntervalOperator
* @see AbstractFormula
*/
-template <class T, class FormulaType>
-class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
+template <class T>
+class RewardNoBoundOperator: public storm::formula::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>> {
public:
/*!
* Empty constructor
*/
- RewardNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
+ RewardNoBoundOperator() {
// Intentionally left empty
}
@@ -60,7 +60,8 @@ public:
*
* @param pathFormula The child node.
*/
- RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+ RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula)
+ : storm::formula::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula) {
// Intentionally left empty
}
@@ -69,18 +70,12 @@ public:
*
* @param pathFormula The child node.
*/
- RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+ RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+ : storm::formula::abstract::RewardNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula, minimumOperator) {
// Intentionally left empty
}
- /*!
- * @returns a string representation of the formula
- */
- virtual std::string toString() const {
- std::string result = "R";
- result += PathNoBoundOperator<T>::toString();
- return result;
- }
+ //TODO: Clone?
};
} //namespace prctl
diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h
index ddfc2ba66..82a43423b 100644
--- a/src/formula/Prctl/Until.h
+++ b/src/formula/Prctl/Until.h
@@ -95,11 +95,11 @@ public:
*/
virtual AbstractPathFormula<T>* clone() const {
Until<T>* result = new Until();
- if (left != NULL) {
- result->setLeft(left->clone());
+ if (this->leftIsSet()) {
+ result->setLeft(this->getLeft().clone());
}
- if (right != NULL) {
- result->setRight(right->clone());
+ if (this->rightIsSet()) {
+ result->setRight(this->getRight().clone());
}
return result;
}
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
index ddb9d90ab..b3ff944a2 100644
--- a/src/formula/PrctlFormulaChecker.h
+++ b/src/formula/PrctlFormulaChecker.h
@@ -2,7 +2,7 @@
#define STORM_FORMULA_PRCTLFORMULACHECKER_H_
#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/Formulas.h"
+#include "src/formula/Prctl.h"
#include <iostream>
diff --git a/src/formula/abstract/AbstractFormula.h b/src/formula/abstract/AbstractFormula.h
index 0d41d4450..424d17394 100644
--- a/src/formula/abstract/AbstractFormula.h
+++ b/src/formula/abstract/AbstractFormula.h
@@ -10,14 +10,6 @@
#include <string>
-namespace storm {
-namespace formula {
-namespace abstract {
-template <class T> class AbstractFormula;
-}
-}
-}
-
#include "src/modelchecker/ForwardDeclarations.h"
#include "src/formula/AbstractFormulaChecker.h"