From 7f15f358c1994e4222bc822512908fddbb9e7e16 Mon Sep 17 00:00:00 2001 From: masawei Date: Thu, 14 Aug 2014 13:17:11 +0200 Subject: [PATCH] Removed the FormulaCheckers. Former-commit-id: 24910974c628020bbf89d0754f0957ff3e3e02ad --- src/formula/AbstractFormula.h | 19 +---- src/formula/AbstractFormulaChecker.h | 74 ------------------- src/formula/PrctlFormulaChecker.h | 49 ------------ src/formula/csl/AbstractCslFormula.h | 4 + src/formula/csl/And.h | 11 --- src/formula/csl/Ap.h | 13 ---- src/formula/csl/Eventually.h | 10 --- src/formula/csl/Globally.h | 11 --- src/formula/csl/Next.h | 11 --- src/formula/csl/Not.h | 11 --- src/formula/csl/Or.h | 11 --- src/formula/csl/ProbabilisticBoundOperator.h | 10 --- src/formula/csl/SteadyStateBoundOperator.h | 11 --- src/formula/csl/TimeBoundedEventually.h | 10 --- src/formula/csl/TimeBoundedUntil.h | 10 --- src/formula/csl/Until.h | 11 --- src/formula/ltl/And.h | 11 --- src/formula/ltl/Ap.h | 12 --- src/formula/ltl/BoundedEventually.h | 11 --- src/formula/ltl/BoundedUntil.h | 10 --- src/formula/ltl/Eventually.h | 10 --- src/formula/ltl/Globally.h | 11 --- src/formula/ltl/Next.h | 11 --- src/formula/ltl/Not.h | 11 --- src/formula/ltl/Or.h | 10 --- src/formula/ltl/Until.h | 11 --- src/formula/prctl/AbstractPrctlFormula.h | 4 + src/formula/prctl/And.h | 11 --- src/formula/prctl/Ap.h | 13 ---- src/formula/prctl/BoundedEventually.h | 11 --- src/formula/prctl/BoundedNaryUntil.h | 14 ---- src/formula/prctl/BoundedUntil.h | 10 --- src/formula/prctl/CumulativeReward.h | 13 ---- src/formula/prctl/Eventually.h | 10 --- src/formula/prctl/Globally.h | 11 --- src/formula/prctl/InstantaneousReward.h | 13 ---- src/formula/prctl/Next.h | 11 --- src/formula/prctl/Not.h | 12 --- src/formula/prctl/Or.h | 11 --- .../prctl/ProbabilisticBoundOperator.h | 10 --- src/formula/prctl/ReachabilityReward.h | 11 --- src/formula/prctl/RewardBoundOperator.h | 10 --- src/formula/prctl/SteadyStateReward.h | 13 ---- src/formula/prctl/Until.h | 11 --- 44 files changed, 9 insertions(+), 574 deletions(-) delete mode 100644 src/formula/AbstractFormulaChecker.h delete mode 100644 src/formula/PrctlFormulaChecker.h diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h index c790d8eae..8ab2fd130 100644 --- a/src/formula/AbstractFormula.h +++ b/src/formula/AbstractFormula.h @@ -9,6 +9,7 @@ #define STORM_FORMULA_ABSTRACTFORMULA_H_ #include +#include namespace storm { namespace property { @@ -16,8 +17,6 @@ template class AbstractFormula; } //namespace property } //namespace storm -#include "src/formula/AbstractFormulaChecker.h" - namespace storm { namespace property { @@ -64,22 +63,6 @@ public: */ virtual std::string toString() const = 0; - /*! - * @brief Checks if all subtrees are valid in some logic. - * - * @note Every subclass must implement this method. - * - * This method is given a checker object that knows which formula - * classes are allowed within the logic the checker represents. Every - * subclass is supposed to call checker.validate() for all child - * formulas and return true if and only if all those calls returned - * true. - * - * @param checker Checker object. - * @return true iff all subtrees are valid. - */ - virtual bool validate(AbstractFormulaChecker const & checker) const = 0; - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h deleted file mode 100644 index 97c0446ee..000000000 --- a/src/formula/AbstractFormulaChecker.h +++ /dev/null @@ -1,74 +0,0 @@ -#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_ -#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_ - -namespace storm { -namespace property { - -template class AbstractFormulaChecker; - -} //namespace property -} //namespace storm - - -#include "src/formula/AbstractFormula.h" -#include - -namespace storm { -namespace property { - -/*! - * @brief Base class for all formula checkers. - * - * A formula checker is used to check if a given formula is valid in some - * logic. Hence, this pure virtual base class should be subclassed for - * every logic we support. - * - * Every subclass must implement validate(). It gets a pointer to an - * AbstractFormula object and should return if the subtree represented by - * this formula is valid in the logic. - * - * Usually, this will be implemented like this: - * @code - * if ( - * dynamic_cast*>(formula) || - * dynamic_cast*>(formula) || - * dynamic_cast*>(formula) - * ) { - * return formula->validate(*this); - * } else return false; - * @endcode - * - * Every formula class implements a validate() method itself which calls - * validate() on the given checker for every child in the formula tree. - * - * If the formula structure is not an actual tree, but an directed acyclic - * graph, the shared subtrees will be checked twice. If we have directed - * cycles, we will have infinite recursions. - */ -template -class AbstractFormulaChecker { - public: - /*! - * Virtual destructor - * To ensure that the right destructor is called - */ - virtual ~AbstractFormulaChecker() { - //intentionally left empty - } - - /*! - * @brief Checks if the given formula is valid in some logic. - * - * Every subclass must implement this method and check, if the - * formula object is valid in the logic of the subclass. - * - * @param formula A pointer to some formula object. - * @return true iff the formula is valid. - */ - virtual bool validate(std::shared_ptr> const & formula) const = 0; -}; - -} // namespace property -} // namespace storm - -#endif diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h deleted file mode 100644 index 5ed817e09..000000000 --- a/src/formula/PrctlFormulaChecker.h +++ /dev/null @@ -1,49 +0,0 @@ -#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_ -#define STORM_FORMULA_PRCTLFORMULACHECKER_H_ - -#include "src/formula/AbstractFormulaChecker.h" -#include "src/formula/Prctl.h" - -#include -#include - -namespace storm { -namespace property { - -/*! - * @brief Checks formulas if they are within PRCTL. - * - * This class implements AbstractFormulaChecker to check if a given formula - * is part of PRCTL logic. - */ -template -class PrctlFormulaChecker : public AbstractFormulaChecker { - public: - /*! - * Implementation of AbstractFormulaChecker::validate() using code - * looking exactly like the sample code given there. - */ - virtual bool validate(std::shared_ptr> const & formula) const { - // What to support: Principles of Model Checking Def. 10.76 + syntactic sugar - if ( - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) || - dynamic_pointer_cast>(formula) - ) { - return formula->validate(*this); - } - return false; - } -}; - -} // namespace property -} // namespace storm - -#endif diff --git a/src/formula/csl/AbstractCslFormula.h b/src/formula/csl/AbstractCslFormula.h index 6631a753f..73d4f3dcd 100644 --- a/src/formula/csl/AbstractCslFormula.h +++ b/src/formula/csl/AbstractCslFormula.h @@ -47,19 +47,23 @@ public: */ bool isProbEventuallyAP() const { + // Test if a probabilistic bound operator is at the root. if(dynamic_cast const *>(this) == nullptr) { return false; } auto probFormula = dynamic_cast const *>(this); + // Check if the direct subformula of the probabilistic bound operator is an eventually or until formula. if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + // Get the subformula and check if its subformulas are propositional. auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return eventuallyFormula->getChild()->isPropositional(); } else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + // Get the subformula and check if its subformulas are propositional. auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional(); } diff --git a/src/formula/csl/And.h b/src/formula/csl/And.h index 0218edecb..afb78ceeb 100644 --- a/src/formula/csl/And.h +++ b/src/formula/csl/And.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_CSL_AND_H_ #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" #include @@ -129,16 +128,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. * diff --git a/src/formula/csl/Ap.h b/src/formula/csl/Ap.h index 284f94eeb..a80f8fdfe 100644 --- a/src/formula/csl/Ap.h +++ b/src/formula/csl/Ap.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_CSL_AP_H_ #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { @@ -94,18 +93,6 @@ public: return modelChecker.template as()->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(AbstractFormulaChecker const & checker) const override { - return true; - } - /*! Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. * diff --git a/src/formula/csl/Eventually.h b/src/formula/csl/Eventually.h index 8428d5f00..21bdd71b4 100644 --- a/src/formula/csl/Eventually.h +++ b/src/formula/csl/Eventually.h @@ -119,16 +119,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/csl/Globally.h b/src/formula/csl/Globally.h index 211532efb..e93baeca5 100644 --- a/src/formula/csl/Globally.h +++ b/src/formula/csl/Globally.h @@ -10,7 +10,6 @@ #include "src/formula/csl/AbstractPathFormula.h" #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { @@ -120,16 +119,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/csl/Next.h b/src/formula/csl/Next.h index 3148377a6..8c86095b8 100644 --- a/src/formula/csl/Next.h +++ b/src/formula/csl/Next.h @@ -10,7 +10,6 @@ #include "src/formula/csl/AbstractPathFormula.h" #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -119,16 +118,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/csl/Not.h b/src/formula/csl/Not.h index 698b92b89..9c23323ce 100644 --- a/src/formula/csl/Not.h +++ b/src/formula/csl/Not.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_CSL_NOT_H_ #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/csl/ForwardDeclarations.h" namespace storm { @@ -115,16 +114,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. * diff --git a/src/formula/csl/Or.h b/src/formula/csl/Or.h index 2ecc7fab9..b6017d4be 100644 --- a/src/formula/csl/Or.h +++ b/src/formula/csl/Or.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_CSL_OR_H_ #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -127,16 +126,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. * diff --git a/src/formula/csl/ProbabilisticBoundOperator.h b/src/formula/csl/ProbabilisticBoundOperator.h index 6d0e0d6a3..f0c51af72 100644 --- a/src/formula/csl/ProbabilisticBoundOperator.h +++ b/src/formula/csl/ProbabilisticBoundOperator.h @@ -114,16 +114,6 @@ public: return modelChecker.template as()->checkProbabilisticBoundOperator(*this); } - /*! - * @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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns a string representation of the formula */ diff --git a/src/formula/csl/SteadyStateBoundOperator.h b/src/formula/csl/SteadyStateBoundOperator.h index c53823639..3c664f05a 100644 --- a/src/formula/csl/SteadyStateBoundOperator.h +++ b/src/formula/csl/SteadyStateBoundOperator.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_ #include "AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/formula/ComparisonType.h" namespace storm { @@ -111,16 +110,6 @@ public: return modelChecker.template as()->checkSteadyStateBoundOperator(*this); } - /*! - * @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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->stateFormula); - } - /*! * @returns a string representation of the formula */ diff --git a/src/formula/csl/TimeBoundedEventually.h b/src/formula/csl/TimeBoundedEventually.h index 8564a0db3..e4c6aa483 100644 --- a/src/formula/csl/TimeBoundedEventually.h +++ b/src/formula/csl/TimeBoundedEventually.h @@ -86,16 +86,6 @@ public: return modelChecker.template as()->checkTimeBoundedEventually(*this, qualitative); } - /*! - * @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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns a string representation of the formula */ diff --git a/src/formula/csl/TimeBoundedUntil.h b/src/formula/csl/TimeBoundedUntil.h index 1bdf2f0aa..170ddf54a 100644 --- a/src/formula/csl/TimeBoundedUntil.h +++ b/src/formula/csl/TimeBoundedUntil.h @@ -101,16 +101,6 @@ public: return modelChecker.template as()->checkTimeBoundedUntil(*this, qualitative); } - /*! - * @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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * @returns a string representation of the formula */ diff --git a/src/formula/csl/Until.h b/src/formula/csl/Until.h index ea0209053..8d2446489 100644 --- a/src/formula/csl/Until.h +++ b/src/formula/csl/Until.h @@ -10,7 +10,6 @@ #include "src/formula/csl/AbstractPathFormula.h" #include "src/formula/csl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -124,16 +123,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Sets the left child node. * diff --git a/src/formula/ltl/And.h b/src/formula/ltl/And.h index 48c4350cb..06fc83cae 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/AbstractFormulaChecker.h" #include "src/modelchecker/ltl/ForwardDeclarations.h" #include @@ -128,16 +127,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/ltl/Ap.h b/src/formula/ltl/Ap.h index c7845604f..451dadb99 100644 --- a/src/formula/ltl/Ap.h +++ b/src/formula/ltl/Ap.h @@ -106,18 +106,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return true; - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/ltl/BoundedEventually.h b/src/formula/ltl/BoundedEventually.h index 40cdb4038..630e0bbae 100644 --- a/src/formula/ltl/BoundedEventually.h +++ b/src/formula/ltl/BoundedEventually.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_ #include "AbstractLtlFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include #include #include "src/modelchecker/ltl/ForwardDeclarations.h" @@ -126,16 +125,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/ltl/BoundedUntil.h b/src/formula/ltl/BoundedUntil.h index b17b901f4..87e0a7a2d 100644 --- a/src/formula/ltl/BoundedUntil.h +++ b/src/formula/ltl/BoundedUntil.h @@ -135,16 +135,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Sets the left child node. * diff --git a/src/formula/ltl/Eventually.h b/src/formula/ltl/Eventually.h index b8662cd69..328fd993b 100644 --- a/src/formula/ltl/Eventually.h +++ b/src/formula/ltl/Eventually.h @@ -117,16 +117,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/ltl/Globally.h b/src/formula/ltl/Globally.h index 50d977ee8..060b5bba2 100644 --- a/src/formula/ltl/Globally.h +++ b/src/formula/ltl/Globally.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_LTL_GLOBALLY_H_ #include "AbstractLtlFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/ltl/ForwardDeclarations.h" namespace storm { @@ -118,16 +117,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/ltl/Next.h b/src/formula/ltl/Next.h index 0fd069135..a038252c2 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/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -117,16 +116,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/ltl/Not.h b/src/formula/ltl/Not.h index 99a90736c..2538298a4 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/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -113,16 +112,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/ltl/Or.h b/src/formula/ltl/Or.h index 336da397b..42296766f 100644 --- a/src/formula/ltl/Or.h +++ b/src/formula/ltl/Or.h @@ -125,16 +125,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/ltl/Until.h b/src/formula/ltl/Until.h index 95c999e39..92a6e4ed1 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/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -146,16 +145,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Sets the left child node. * diff --git a/src/formula/prctl/AbstractPrctlFormula.h b/src/formula/prctl/AbstractPrctlFormula.h index 044996b9c..f728110fe 100644 --- a/src/formula/prctl/AbstractPrctlFormula.h +++ b/src/formula/prctl/AbstractPrctlFormula.h @@ -46,19 +46,23 @@ public: */ bool isProbEventuallyAP() const { + // Test if a probabilistic bound operator is at the root. if(dynamic_cast const *>(this) == nullptr) { return false; } auto probFormula = dynamic_cast const *>(this); + // Check if the direct subformula of the probabilistic bound operator is an eventually or until formula. if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + // Get the subformula and check if its subformulas are propositional. auto eventuallyFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return eventuallyFormula->getChild()->isPropositional(); } else if(std::dynamic_pointer_cast>(probFormula->getChild()).get() != nullptr) { + // Get the subformula and check if its subformulas are propositional. auto untilFormula = std::dynamic_pointer_cast>(probFormula->getChild()); return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional(); } diff --git a/src/formula/prctl/And.h b/src/formula/prctl/And.h index 80a9cffd3..81b33ad28 100644 --- a/src/formula/prctl/And.h +++ b/src/formula/prctl/And.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_PRCTL_AND_H_ #include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" #include @@ -129,16 +128,6 @@ public: 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& checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/prctl/Ap.h b/src/formula/prctl/Ap.h index ef6d77b12..7df3cabd8 100644 --- a/src/formula/prctl/Ap.h +++ b/src/formula/prctl/Ap.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_PRCTL_AP_H_ #include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { @@ -94,18 +93,6 @@ public: return modelChecker.template as()->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& checker) const override { - return true; - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/prctl/BoundedEventually.h b/src/formula/prctl/BoundedEventually.h index 70e10020d..16b7df1d8 100644 --- a/src/formula/prctl/BoundedEventually.h +++ b/src/formula/prctl/BoundedEventually.h @@ -10,7 +10,6 @@ #include "src/formula/prctl/AbstractPathFormula.h" #include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include #include #include "src/modelchecker/prctl/ForwardDeclarations.h" @@ -126,16 +125,6 @@ public: 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& checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/prctl/BoundedNaryUntil.h b/src/formula/prctl/BoundedNaryUntil.h index 0cf02d4f4..1c9863ac7 100644 --- a/src/formula/prctl/BoundedNaryUntil.h +++ b/src/formula/prctl/BoundedNaryUntil.h @@ -142,20 +142,6 @@ public: 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& checker) const override { - bool res = checker.validate(left); - for (auto it = right->begin(); it != right->end(); ++it) { - res &= checker.validate(std::get<0>(*it)); - } - return res; - } - /*! * Sets the left child node. * diff --git a/src/formula/prctl/BoundedUntil.h b/src/formula/prctl/BoundedUntil.h index d018567eb..92d119583 100644 --- a/src/formula/prctl/BoundedUntil.h +++ b/src/formula/prctl/BoundedUntil.h @@ -130,16 +130,6 @@ public: 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& checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Sets the left child node. * diff --git a/src/formula/prctl/CumulativeReward.h b/src/formula/prctl/CumulativeReward.h index 84861ed91..4a94c021b 100644 --- a/src/formula/prctl/CumulativeReward.h +++ b/src/formula/prctl/CumulativeReward.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_PRCTL_CUMULATIVEREWARD_H_ #include "AbstractRewardPathFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include namespace storm { @@ -108,18 +107,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return true; - } - /*! * @returns the time instance for the instantaneous reward operator */ diff --git a/src/formula/prctl/Eventually.h b/src/formula/prctl/Eventually.h index 321ac872f..77dcb3c73 100644 --- a/src/formula/prctl/Eventually.h +++ b/src/formula/prctl/Eventually.h @@ -118,16 +118,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(child); - } - /*! * @returns the child node */ diff --git a/src/formula/prctl/Globally.h b/src/formula/prctl/Globally.h index 7296a9534..8f0b9c910 100644 --- a/src/formula/prctl/Globally.h +++ b/src/formula/prctl/Globally.h @@ -10,7 +10,6 @@ #include "src/formula/prctl/AbstractPathFormula.h" #include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { @@ -119,16 +118,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(child); - } - /*! * @returns the child node */ diff --git a/src/formula/prctl/InstantaneousReward.h b/src/formula/prctl/InstantaneousReward.h index 3a65583a6..18cf7eeae 100644 --- a/src/formula/prctl/InstantaneousReward.h +++ b/src/formula/prctl/InstantaneousReward.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_ #include "AbstractRewardPathFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include #include @@ -110,18 +109,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return true; - } - /*! * @returns the time instance for the instantaneous reward operator */ diff --git a/src/formula/prctl/Next.h b/src/formula/prctl/Next.h index 49b66c062..052adf9ca 100644 --- a/src/formula/prctl/Next.h +++ b/src/formula/prctl/Next.h @@ -10,7 +10,6 @@ #include "src/formula/prctl/AbstractPathFormula.h" #include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -118,16 +117,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/prctl/Not.h b/src/formula/prctl/Not.h index 7531989f6..a58c5d3f4 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/AbstractFormulaChecker.h" #include "src/modelchecker/prctl/ForwardDeclarations.h" namespace storm { @@ -114,17 +113,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/prctl/Or.h b/src/formula/prctl/Or.h index 7bbc0e045..646b5735c 100644 --- a/src/formula/prctl/Or.h +++ b/src/formula/prctl/Or.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_PRCTL_OR_H_ #include "src/formula/prctl/AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -126,16 +125,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->left) && checker.validate(this->right); - } - /*! * Returns whether the formula is a propositional logic formula. * That is, this formula and all its subformulas consist only of And, Or, Not and AP. diff --git a/src/formula/prctl/ProbabilisticBoundOperator.h b/src/formula/prctl/ProbabilisticBoundOperator.h index e1557ce04..6905d9069 100644 --- a/src/formula/prctl/ProbabilisticBoundOperator.h +++ b/src/formula/prctl/ProbabilisticBoundOperator.h @@ -113,16 +113,6 @@ public: return modelChecker.template as()->checkProbabilisticBoundOperator(*this); } - /*! - * @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(AbstractFormulaChecker const & checker) const override { - return checker.validate(child); - } - /*! * @returns a string representation of the formula */ diff --git a/src/formula/prctl/ReachabilityReward.h b/src/formula/prctl/ReachabilityReward.h index eacc49e3e..0fe5f5792 100644 --- a/src/formula/prctl/ReachabilityReward.h +++ b/src/formula/prctl/ReachabilityReward.h @@ -10,7 +10,6 @@ #include "AbstractRewardPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -114,16 +113,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns the child node */ diff --git a/src/formula/prctl/RewardBoundOperator.h b/src/formula/prctl/RewardBoundOperator.h index cfebea0d6..12900c58c 100644 --- a/src/formula/prctl/RewardBoundOperator.h +++ b/src/formula/prctl/RewardBoundOperator.h @@ -111,16 +111,6 @@ public: return modelChecker.template as()->checkRewardBoundOperator(*this); } - /*! - * @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(AbstractFormulaChecker const & checker) const override { - return checker.validate(this->child); - } - /*! * @returns a string representation of the formula */ diff --git a/src/formula/prctl/SteadyStateReward.h b/src/formula/prctl/SteadyStateReward.h index d7dfc5416..84774998f 100644 --- a/src/formula/prctl/SteadyStateReward.h +++ b/src/formula/prctl/SteadyStateReward.h @@ -9,7 +9,6 @@ #define STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_ #include "AbstractRewardPathFormula.h" -#include "src/formula/AbstractFormulaChecker.h" #include namespace storm { @@ -88,18 +87,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return true; - } }; } //namespace prctl diff --git a/src/formula/prctl/Until.h b/src/formula/prctl/Until.h index 3d8a5f4e2..eb939b54f 100644 --- a/src/formula/prctl/Until.h +++ b/src/formula/prctl/Until.h @@ -10,7 +10,6 @@ #include "AbstractPathFormula.h" #include "AbstractStateFormula.h" -#include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace property { @@ -124,16 +123,6 @@ public: 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(AbstractFormulaChecker const & checker) const override { - return checker.validate(left) && checker.validate(right); - } - /*! * Sets the left child node. *