From 38652f44e4ecc24ba7b4f232dd3924eed006f55e Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 15 Apr 2013 14:51:43 +0200 Subject: [PATCH] Restructuring formula classes, part I Sorted formulas into respective folders, depending on which logic they belong to (or if they are abstract). The Code is NOTadapted to the new structure yet. --- src/formula/{ => Csl}/AbstractPathFormula.h | 0 src/formula/{ => Csl}/AbstractStateFormula.h | 0 src/formula/{ => Csl}/CumulativeReward.h | 0 .../{ => Csl}/SteadyStateBoundOperator.h | 0 .../{ => Csl}/SteadyStateNoBoundOperator.h | 0 src/formula/{ => Csl}/TimeBoundedEventually.h | 0 src/formula/{ => Csl}/TimeBoundedUntil.h | 0 src/formula/Ltl/AbstractLtlFormula.h | 39 +++++++++++ src/formula/Prtl/AbstractPathFormula.h | 70 +++++++++++++++++++ src/formula/Prtl/AbstractStateFormula.h | 68 ++++++++++++++++++ src/formula/{ => Prtl}/InstantaneousReward.h | 0 src/formula/{ => Prtl}/ReachabilityReward.h | 0 src/formula/{ => Prtl}/RewardBoundOperator.h | 0 .../{ => Prtl}/RewardNoBoundOperator.h | 0 src/formula/{ => Prtl}/SteadyStateReward.h | 0 src/formula/{ => abstract}/AbstractFormula.h | 17 +++-- src/formula/{ => abstract}/And.h | 16 ++--- src/formula/{ => abstract}/Ap.h | 0 .../{ => abstract}/BoundedEventually.h | 0 src/formula/{ => abstract}/BoundedNaryUntil.h | 0 src/formula/{ => abstract}/BoundedUntil.h | 0 src/formula/{ => abstract}/Eventually.h | 0 src/formula/{ => abstract}/Globally.h | 0 src/formula/{ => abstract}/Next.h | 0 src/formula/{ => abstract}/Not.h | 0 .../{ => abstract}/OptimizingOperator.h | 0 src/formula/{ => abstract}/Or.h | 0 .../{ => abstract}/PathBoundOperator.h | 0 .../{ => abstract}/PathNoBoundOperator.h | 0 .../ProbabilisticBoundOperator.h | 0 .../ProbabilisticNoBoundOperator.h | 0 .../{ => abstract}/StateBoundOperator.h | 0 .../{ => abstract}/StateNoBoundOperator.h | 0 .../{ => abstract}/TimeBoundedOperator.h | 0 src/formula/{ => abstract}/Until.h | 0 35 files changed, 196 insertions(+), 14 deletions(-) rename src/formula/{ => Csl}/AbstractPathFormula.h (100%) rename src/formula/{ => Csl}/AbstractStateFormula.h (100%) rename src/formula/{ => Csl}/CumulativeReward.h (100%) rename src/formula/{ => Csl}/SteadyStateBoundOperator.h (100%) rename src/formula/{ => Csl}/SteadyStateNoBoundOperator.h (100%) rename src/formula/{ => Csl}/TimeBoundedEventually.h (100%) rename src/formula/{ => Csl}/TimeBoundedUntil.h (100%) create mode 100644 src/formula/Ltl/AbstractLtlFormula.h create mode 100644 src/formula/Prtl/AbstractPathFormula.h create mode 100644 src/formula/Prtl/AbstractStateFormula.h rename src/formula/{ => Prtl}/InstantaneousReward.h (100%) rename src/formula/{ => Prtl}/ReachabilityReward.h (100%) rename src/formula/{ => Prtl}/RewardBoundOperator.h (100%) rename src/formula/{ => Prtl}/RewardNoBoundOperator.h (100%) rename src/formula/{ => Prtl}/SteadyStateReward.h (100%) rename src/formula/{ => abstract}/AbstractFormula.h (86%) rename src/formula/{ => abstract}/And.h (92%) rename src/formula/{ => abstract}/Ap.h (100%) rename src/formula/{ => abstract}/BoundedEventually.h (100%) rename src/formula/{ => abstract}/BoundedNaryUntil.h (100%) rename src/formula/{ => abstract}/BoundedUntil.h (100%) rename src/formula/{ => abstract}/Eventually.h (100%) rename src/formula/{ => abstract}/Globally.h (100%) rename src/formula/{ => abstract}/Next.h (100%) rename src/formula/{ => abstract}/Not.h (100%) rename src/formula/{ => abstract}/OptimizingOperator.h (100%) rename src/formula/{ => abstract}/Or.h (100%) rename src/formula/{ => abstract}/PathBoundOperator.h (100%) rename src/formula/{ => abstract}/PathNoBoundOperator.h (100%) rename src/formula/{ => abstract}/ProbabilisticBoundOperator.h (100%) rename src/formula/{ => abstract}/ProbabilisticNoBoundOperator.h (100%) rename src/formula/{ => abstract}/StateBoundOperator.h (100%) rename src/formula/{ => abstract}/StateNoBoundOperator.h (100%) rename src/formula/{ => abstract}/TimeBoundedOperator.h (100%) rename src/formula/{ => abstract}/Until.h (100%) diff --git a/src/formula/AbstractPathFormula.h b/src/formula/Csl/AbstractPathFormula.h similarity index 100% rename from src/formula/AbstractPathFormula.h rename to src/formula/Csl/AbstractPathFormula.h diff --git a/src/formula/AbstractStateFormula.h b/src/formula/Csl/AbstractStateFormula.h similarity index 100% rename from src/formula/AbstractStateFormula.h rename to src/formula/Csl/AbstractStateFormula.h diff --git a/src/formula/CumulativeReward.h b/src/formula/Csl/CumulativeReward.h similarity index 100% rename from src/formula/CumulativeReward.h rename to src/formula/Csl/CumulativeReward.h diff --git a/src/formula/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h similarity index 100% rename from src/formula/SteadyStateBoundOperator.h rename to src/formula/Csl/SteadyStateBoundOperator.h diff --git a/src/formula/SteadyStateNoBoundOperator.h b/src/formula/Csl/SteadyStateNoBoundOperator.h similarity index 100% rename from src/formula/SteadyStateNoBoundOperator.h rename to src/formula/Csl/SteadyStateNoBoundOperator.h diff --git a/src/formula/TimeBoundedEventually.h b/src/formula/Csl/TimeBoundedEventually.h similarity index 100% rename from src/formula/TimeBoundedEventually.h rename to src/formula/Csl/TimeBoundedEventually.h diff --git a/src/formula/TimeBoundedUntil.h b/src/formula/Csl/TimeBoundedUntil.h similarity index 100% rename from src/formula/TimeBoundedUntil.h rename to src/formula/Csl/TimeBoundedUntil.h diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h new file mode 100644 index 000000000..ba258a3fc --- /dev/null +++ b/src/formula/Ltl/AbstractLtlFormula.h @@ -0,0 +1,39 @@ +/* + * AbstractLtlFormula.h + * + * Created on: 15.04.2013 + * Author: thomas + */ + +#ifndef ABSTRACTLTLFORMULA_H_ +#define ABSTRACTLTLFORMULA_H_ + +namespace storm { +namespace formula { + +class AbstractLtlFormula { +public: + /** + * Empty destructor + */ + virtual ~AbstractLtlFormula() { + // Intentionally left empty + } + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @note This function is not implemented in this class. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; +}; + +} /* namespace formula */ +} /* namespace storm */ +#endif /* ABSTRACTLTLFORMULA_H_ */ diff --git a/src/formula/Prtl/AbstractPathFormula.h b/src/formula/Prtl/AbstractPathFormula.h new file mode 100644 index 000000000..459cbd057 --- /dev/null +++ b/src/formula/Prtl/AbstractPathFormula.h @@ -0,0 +1,70 @@ +/* + * AbstractPathFormula.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_ +#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_ + +namespace storm { namespace formula { +template class AbstractPathFormula; +}} + +#include "src/formula/AbstractFormula.h" +#include "src/modelchecker/ForwardDeclarations.h" + +#include +#include +#include + +namespace storm { +namespace formula { + +/*! + * @brief + * Abstract base class for Abstract path formulas. + * + * @attention This class is abstract. + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method + * clone(). + */ +template +class AbstractPathFormula : public virtual AbstractFormula { + +public: + /*! + * empty destructor + */ + virtual ~AbstractPathFormula() { } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @note This function is not implemented in this class. + * @returns a new AND-object that is identical the called object. + */ + virtual AbstractPathFormula* clone() const = 0; + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @note This function is not implemented in this class. + * + * @returns A vector indicating the probability that the formula holds for each state. + */ + virtual std::vector* check(const storm::modelchecker::AbstractModelChecker& modelChecker, bool qualitative) const = 0; +}; + +} //namespace formula +} //namespace storm + +#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */ diff --git a/src/formula/Prtl/AbstractStateFormula.h b/src/formula/Prtl/AbstractStateFormula.h new file mode 100644 index 000000000..cf15fdb30 --- /dev/null +++ b/src/formula/Prtl/AbstractStateFormula.h @@ -0,0 +1,68 @@ +/* + * AbstractStateFormula.h + * + * Created on: 19.10.2012 + * Author: Thomas Heinemann + */ + +#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_ +#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_ + +namespace storm { namespace formula { +template class AbstractStateFormula; +}} + +#include "src/formula/AbstractFormula.h" +#include "src/storage/BitVector.h" +#include "src/modelchecker/ForwardDeclarations.h" + +namespace storm { +namespace formula { + +/*! + * @brief + * Abstract base class for Abstract state formulas. + * + * @attention This class is abstract. + * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so + * the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method + * clone(). + */ +template +class AbstractStateFormula : public AbstractFormula { + +public: + /*! + * empty destructor + */ + virtual ~AbstractStateFormula() { } + + /*! + * Clones the called object. + * + * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones + * + * @note This function is not implemented in this class. + * @returns a new AND-object that is identical the called object. + */ + virtual AbstractStateFormula* clone() const = 0; + + /*! + * Calls the model checker to check this formula. + * Needed to infer the correct type of formula class. + * + * @note This function should only be called in a generic check function of a model checker class. For other uses, + * the methods of the model checker should be used. + * + * @note This function is not implemented in this class. + * + * @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) const = 0; // { +}; + +} //namespace formula +} //namespace storm + + +#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */ diff --git a/src/formula/InstantaneousReward.h b/src/formula/Prtl/InstantaneousReward.h similarity index 100% rename from src/formula/InstantaneousReward.h rename to src/formula/Prtl/InstantaneousReward.h diff --git a/src/formula/ReachabilityReward.h b/src/formula/Prtl/ReachabilityReward.h similarity index 100% rename from src/formula/ReachabilityReward.h rename to src/formula/Prtl/ReachabilityReward.h diff --git a/src/formula/RewardBoundOperator.h b/src/formula/Prtl/RewardBoundOperator.h similarity index 100% rename from src/formula/RewardBoundOperator.h rename to src/formula/Prtl/RewardBoundOperator.h diff --git a/src/formula/RewardNoBoundOperator.h b/src/formula/Prtl/RewardNoBoundOperator.h similarity index 100% rename from src/formula/RewardNoBoundOperator.h rename to src/formula/Prtl/RewardNoBoundOperator.h diff --git a/src/formula/SteadyStateReward.h b/src/formula/Prtl/SteadyStateReward.h similarity index 100% rename from src/formula/SteadyStateReward.h rename to src/formula/Prtl/SteadyStateReward.h diff --git a/src/formula/AbstractFormula.h b/src/formula/abstract/AbstractFormula.h similarity index 86% rename from src/formula/AbstractFormula.h rename to src/formula/abstract/AbstractFormula.h index 517f4ba62..b7f453fcb 100644 --- a/src/formula/AbstractFormula.h +++ b/src/formula/abstract/AbstractFormula.h @@ -5,21 +5,25 @@ * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_ABSTRACTFORMULA_H_ -#define STORM_FORMULA_ABSTRACTFORMULA_H_ +#ifndef STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_ +#define STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_ #include -namespace storm { namespace formula { +namespace storm { +namespace formula { +namespace abstract { template class AbstractFormula; -}} +} +} +} #include "src/modelchecker/ForwardDeclarations.h" #include "src/formula/AbstractFormulaChecker.h" namespace storm { namespace formula { - +namespace abstract { //abstract /*! @@ -67,7 +71,8 @@ public: virtual bool conforms(const AbstractFormulaChecker& checker) const = 0; }; +} // namespace abstract } // namespace formula } // namespace storm -#endif /* STORM_FORMULA_ABSTRACTFORMULA_H_ */ +#endif /* STORM_FORMULA_ABSTRACT_ABSTRACTFORMULA_H_ */ diff --git a/src/formula/And.h b/src/formula/abstract/And.h similarity index 92% rename from src/formula/And.h rename to src/formula/abstract/And.h index 80f46a821..1bdbca9ed 100644 --- a/src/formula/And.h +++ b/src/formula/abstract/And.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef STORM_FORMULA_AND_H_ -#define STORM_FORMULA_AND_H_ +#ifndef STORM_FORMULA_ABSTRACT_AND_H_ +#define STORM_FORMULA_ABSTRACT_AND_H_ -#include "src/formula/AbstractStateFormula.h" +#include "src/formula/abstract/AbstractFormula.h" #include "src/formula/AbstractFormulaChecker.h" #include "src/modelchecker/ForwardDeclarations.h" #include @@ -52,7 +52,7 @@ class IAndModelChecker { * @see AbstractFormula */ template -class And : public AbstractStateFormula { +class And : public AbstractFormula { public: /*! @@ -71,7 +71,7 @@ public: * @param left The left sub formula * @param right The right sub formula */ - And(AbstractStateFormula* left, AbstractStateFormula* right) { + And(AbstractFormula* left, AbstractFormula* right) { this->left = left; this->right = right; } @@ -177,12 +177,12 @@ public: } private: - AbstractStateFormula* left; - AbstractStateFormula* right; + AbstractFormula* left; + AbstractFormula* right; }; } //namespace formula } //namespace storm -#endif /* STORM_FORMULA_AND_H_ */ +#endif /* STORM_FORMULA_ABSTRACT_AND_H_ */ diff --git a/src/formula/Ap.h b/src/formula/abstract/Ap.h similarity index 100% rename from src/formula/Ap.h rename to src/formula/abstract/Ap.h diff --git a/src/formula/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h similarity index 100% rename from src/formula/BoundedEventually.h rename to src/formula/abstract/BoundedEventually.h diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h similarity index 100% rename from src/formula/BoundedNaryUntil.h rename to src/formula/abstract/BoundedNaryUntil.h diff --git a/src/formula/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h similarity index 100% rename from src/formula/BoundedUntil.h rename to src/formula/abstract/BoundedUntil.h diff --git a/src/formula/Eventually.h b/src/formula/abstract/Eventually.h similarity index 100% rename from src/formula/Eventually.h rename to src/formula/abstract/Eventually.h diff --git a/src/formula/Globally.h b/src/formula/abstract/Globally.h similarity index 100% rename from src/formula/Globally.h rename to src/formula/abstract/Globally.h diff --git a/src/formula/Next.h b/src/formula/abstract/Next.h similarity index 100% rename from src/formula/Next.h rename to src/formula/abstract/Next.h diff --git a/src/formula/Not.h b/src/formula/abstract/Not.h similarity index 100% rename from src/formula/Not.h rename to src/formula/abstract/Not.h diff --git a/src/formula/OptimizingOperator.h b/src/formula/abstract/OptimizingOperator.h similarity index 100% rename from src/formula/OptimizingOperator.h rename to src/formula/abstract/OptimizingOperator.h diff --git a/src/formula/Or.h b/src/formula/abstract/Or.h similarity index 100% rename from src/formula/Or.h rename to src/formula/abstract/Or.h diff --git a/src/formula/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h similarity index 100% rename from src/formula/PathBoundOperator.h rename to src/formula/abstract/PathBoundOperator.h diff --git a/src/formula/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h similarity index 100% rename from src/formula/PathNoBoundOperator.h rename to src/formula/abstract/PathNoBoundOperator.h diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h similarity index 100% rename from src/formula/ProbabilisticBoundOperator.h rename to src/formula/abstract/ProbabilisticBoundOperator.h diff --git a/src/formula/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h similarity index 100% rename from src/formula/ProbabilisticNoBoundOperator.h rename to src/formula/abstract/ProbabilisticNoBoundOperator.h diff --git a/src/formula/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h similarity index 100% rename from src/formula/StateBoundOperator.h rename to src/formula/abstract/StateBoundOperator.h diff --git a/src/formula/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h similarity index 100% rename from src/formula/StateNoBoundOperator.h rename to src/formula/abstract/StateNoBoundOperator.h diff --git a/src/formula/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h similarity index 100% rename from src/formula/TimeBoundedOperator.h rename to src/formula/abstract/TimeBoundedOperator.h diff --git a/src/formula/Until.h b/src/formula/abstract/Until.h similarity index 100% rename from src/formula/Until.h rename to src/formula/abstract/Until.h