From 80779523317a0e2ccd66a2d322f9a5c15d3786d4 Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 29 Jan 2013 20:14:38 +0100 Subject: [PATCH] adding needed methods for more formula classes --- src/formula/And.h | 7 ++++++- src/formula/BoundOperator.h | 5 +++++ src/formula/BoundedEventually.h | 5 +++++ src/formula/CumulativeReward.h | 5 +++++ src/formula/Globally.h | 5 +++++ src/formula/InstantaneousReward.h | 5 +++++ src/formula/Next.h | 5 +++++ src/formula/Or.h | 7 ++++++- src/formula/ProbabilisticBoundOperator.h | 2 ++ src/formula/RewardBoundOperator.h | 1 + 10 files changed, 45 insertions(+), 2 deletions(-) diff --git a/src/formula/And.h b/src/formula/And.h index 601872f79..abc407683 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -9,6 +9,7 @@ #define STORM_FORMULA_AND_H_ #include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "src/modelChecker/AbstractModelChecker.h" #include @@ -149,9 +150,13 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) { + virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkAnd(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->left) && checker.conforms(this->right); + } private: AbstractStateFormula* left; diff --git a/src/formula/BoundOperator.h b/src/formula/BoundOperator.h index 67d92df8a..c86455f60 100644 --- a/src/formula/BoundOperator.h +++ b/src/formula/BoundOperator.h @@ -10,6 +10,7 @@ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractPathFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "src/modelChecker/AbstractModelChecker.h" #include "src/utility/ConstTemplates.h" @@ -157,6 +158,10 @@ public: virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkBoundOperator(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->pathFormula); + } private: ComparisonType comparisonOperator; diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h index 5c92ea3d8..995d4c899 100644 --- a/src/formula/BoundedEventually.h +++ b/src/formula/BoundedEventually.h @@ -10,6 +10,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include #include "src/modelChecker/AbstractModelChecker.h" @@ -147,6 +148,10 @@ public: virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkBoundedEventually(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->child); + } private: AbstractStateFormula* child; diff --git a/src/formula/CumulativeReward.h b/src/formula/CumulativeReward.h index bdc1e70b1..ac8c6eab1 100644 --- a/src/formula/CumulativeReward.h +++ b/src/formula/CumulativeReward.h @@ -10,6 +10,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include @@ -111,6 +112,10 @@ public: virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkCumulativeReward(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return true; + } private: uint_fast64_t bound; diff --git a/src/formula/Globally.h b/src/formula/Globally.h index 46d464fad..39dad85ff 100644 --- a/src/formula/Globally.h +++ b/src/formula/Globally.h @@ -10,6 +10,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -121,6 +122,10 @@ public: virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkGlobally(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->child); + } private: AbstractStateFormula* child; diff --git a/src/formula/InstantaneousReward.h b/src/formula/InstantaneousReward.h index da6d3269b..3ab36c584 100644 --- a/src/formula/InstantaneousReward.h +++ b/src/formula/InstantaneousReward.h @@ -10,6 +10,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" #include "boost/integer/integer_mask.hpp" #include @@ -111,6 +112,10 @@ public: virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkInstantaneousReward(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return true; + } private: uint_fast64_t bound; diff --git a/src/formula/Next.h b/src/formula/Next.h index 763d6068c..8884ac5b6 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -10,6 +10,7 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { @@ -123,6 +124,10 @@ public: virtual std::vector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkNext(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->child); + } private: AbstractStateFormula* child; diff --git a/src/formula/Or.h b/src/formula/Or.h index e5143ebeb..6a071f395 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -8,7 +8,8 @@ #ifndef STORM_FORMULA_OR_H_ #define STORM_FORMULA_OR_H_ -#include "AbstractStateFormula.h" +#include "src/formula/AbstractStateFormula.h" +#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace formula { @@ -150,6 +151,10 @@ public: virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker& modelChecker) const { return modelChecker.template as()->checkOr(*this); } + + virtual bool conforms(const AbstractFormulaChecker& checker) const { + return checker.conforms(this->left) && checker.conforms(this->right); + } private: AbstractStateFormula* left; diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index 37fe7858d..3e6e7fde6 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -45,10 +45,12 @@ public: /*! * Empty constructor */ +//! TODO: this constructor should give a comparisontype as first argument ProbabilisticBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { // Intentionally left empty } + /*! * Constructor * diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index 26f6ae7aa..b2c6065ff 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -44,6 +44,7 @@ public: /*! * Empty constructor */ +//! TODO: this constructor should give a comparisontype as first argument RewardBoundOperator() : BoundOperator(storm::utility::constGetZero(), storm::utility::constGetZero(), nullptr) { // Intentionally left empty }