From 3e554514cb3118a3fab97e3c46d2512a57d9fb42 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 16 Apr 2013 15:29:45 +0200 Subject: [PATCH] Correct formulas --- src/formula/AbstractFormulaChecker.h | 2 +- src/formula/Prctl/And.h | 8 +++--- src/formula/Prctl/Ap.h | 4 +-- src/formula/Prctl/BoundedEventually.h | 6 ++--- src/formula/Prctl/BoundedNaryUntil.h | 6 ++--- src/formula/Prctl/BoundedUntil.h | 14 +++++------ src/formula/Prctl/Eventually.h | 4 +-- src/formula/Prctl/Globally.h | 6 ++--- src/formula/Prctl/InstantaneousReward.h | 4 +-- src/formula/Prctl/Next.h | 4 +-- src/formula/Prctl/Not.h | 4 +-- src/formula/Prctl/Or.h | 8 +++--- .../Prctl/ProbabilisticBoundOperator.h | 18 +++++++------ .../Prctl/ProbabilisticNoBoundOperator.h | 1 - src/formula/Prctl/ReachabilityReward.h | 4 +-- src/formula/Prctl/RewardBoundOperator.h | 14 ++++++++--- src/formula/Prctl/RewardNoBoundOperator.h | 25 ++++++++----------- src/formula/Prctl/Until.h | 8 +++--- src/formula/PrctlFormulaChecker.h | 2 +- src/formula/abstract/AbstractFormula.h | 8 ------ 20 files changed, 73 insertions(+), 77 deletions(-) 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* clone() const { And* 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 Ap : public storm::formula::abstract::Ap, public AbstractFormula { +class Ap : public storm::formula::abstract::Ap, public AbstractStateFormula { public: /*! @@ -78,7 +78,7 @@ public: * @returns a new AND-object that is identical the called object. */ virtual AbstractStateFormula* 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* clone() const { BoundedEventually* result = new BoundedEventually(); - 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* clone() const { BoundedNaryUntil* result = new BoundedNaryUntil(); - if (left != NULL) { - result->setLeft(left->clone()); + if (this->leftIsSet()) { + result->setLeft(this->getLeft().clone()); } - if (right != NULL) { + if (this->rightIsSet()) { std::vector*,T,T>>* newright = new std::vector*,T,T>>(); for (auto it = this->right->begin(); it != this->right->end(); ++it) { newright->push_back(std::tuple*,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 BoundedUntil : public storm::formula::abstract::BoundedUntil, +class BoundedUntil : public storm::formula::abstract::BoundedUntil>, public AbstractPathFormula { public: @@ -76,7 +76,7 @@ public: */ BoundedUntil(AbstractStateFormula* left, AbstractStateFormula* right, uint_fast64_t bound) : - storm::formula::abstract::BoundedUntil(left,right,bound) { + storm::formula::abstract::BoundedUntil>(left,right,bound) { //intentionally left empty } @@ -99,12 +99,12 @@ public: */ virtual AbstractPathFormula* clone() const { BoundedUntil* result = new BoundedUntil(); - 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* clone() const { Eventually* result = new Eventually(); - 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* clone() const { - Next* result = new Next(); - if (child != nullptr) { - result->setChild(child); + Globally* result = new Globally(); + 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 InstantaneousReward : public storm::formula::abstract::InstantaneousReward, +class InstantaneousReward : public storm::formula::abstract::InstantaneousReward, public AbstractPathFormula { public: @@ -86,7 +86,7 @@ public: * @returns a new InstantaneousReward-object that is identical the called object. */ virtual AbstractPathFormula* 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* clone() const { Next* result = new Next(); - 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* clone() const { Not* result = new Not(); - 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* clone() const { Or* 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 ProbabilisticBoundOperator : public storm::formula::abstract::ProbabilisticBoundOperator>, - public AbstractStateFormula { + public AbstractStateFormula { public: /*! * Empty constructor */ - ProbabilisticBoundOperator() : PathBoundOperator - (PathBoundOperator::LESS_EQUAL, storm::utility::constGetZero(), nullptr) { + ProbabilisticBoundOperator() { // Intentionally left empty } @@ -74,8 +73,10 @@ public: * @param pathFormula The child node */ ProbabilisticBoundOperator( - typename storm::formula::abstract::PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) - : storm::formula::abstract::ProbabilisticBoundOperator(comparisonRelation, bound, pathFormula) { + typename storm::formula::abstract::PathBoundOperator>::ComparisonType comparisonRelation, + T bound, + AbstractPathFormula* pathFormula) + : storm::formula::abstract::ProbabilisticBoundOperator>(comparisonRelation, bound, pathFormula) { // Intentionally left empty } @@ -87,8 +88,11 @@ public: * @param minimumOperator */ ProbabilisticBoundOperator( - typename storm::formula::abstract::PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) - : storm::formula::abstract::ProbabilisticBoundOperator(comparisonRelation, bound, pathFormula, minimumOperator){ + typename storm::formula::abstract::PathBoundOperator>::ComparisonType comparisonRelation, + T bound, + AbstractPathFormula* pathFormula, + bool minimumOperator) + : storm::formula::abstract::ProbabilisticBoundOperator>(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* clone() const { ReachabilityReward* result = new ReachabilityReward(); - 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::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) : - storm::formula::abstract::RewardBoundOperator(comparisonRelation, bound, pathFormula) { + typename storm::formula::abstract::PathBoundOperator>::ComparisonType comparisonRelation, + T bound, + AbstractPathFormula* pathFormula) : + storm::formula::abstract::RewardBoundOperator>(comparisonRelation, bound, pathFormula) { // Intentionally left empty } + /*! * Constructor * @@ -71,8 +74,11 @@ public: * @param minimumOperator */ RewardBoundOperator( - typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) - : PathBoundOperator(comparisonRelation, bound, pathFormula, minimumOperator) { + typename storm::formula::abstract::PathBoundOperator>::ComparisonType comparisonRelation, + T bound, + AbstractPathFormula* pathFormula, + bool minimumOperator) + : storm::formula::abstract::RewardBoundOperator>(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 RewardNoBoundOperator: public PathNoBoundOperator { +template +class RewardNoBoundOperator: public storm::formula::abstract::RewardNoBoundOperator> { public: /*! * Empty constructor */ - RewardNoBoundOperator() : PathNoBoundOperator(nullptr) { + RewardNoBoundOperator() { // Intentionally left empty } @@ -60,7 +60,8 @@ public: * * @param pathFormula The child node. */ - RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator(pathFormula) { + RewardNoBoundOperator(AbstractPathFormula* pathFormula) + : storm::formula::abstract::RewardNoBoundOperator>(pathFormula) { // Intentionally left empty } @@ -69,18 +70,12 @@ public: * * @param pathFormula The child node. */ - RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator(pathFormula, minimumOperator) { + RewardNoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) + : storm::formula::abstract::RewardNoBoundOperator>(pathFormula, minimumOperator) { // Intentionally left empty } - /*! - * @returns a string representation of the formula - */ - virtual std::string toString() const { - std::string result = "R"; - result += PathNoBoundOperator::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* clone() const { Until* 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 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 -namespace storm { -namespace formula { -namespace abstract { -template class AbstractFormula; -} -} -} - #include "src/modelchecker/ForwardDeclarations.h" #include "src/formula/AbstractFormulaChecker.h"