diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h index 72f035713..55661093c 100644 --- a/src/formula/NoBoundOperator.h +++ b/src/formula/NoBoundOperator.h @@ -11,6 +11,7 @@ #include "src/formula/AbstractFormula.h" #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractFormulaChecker.h" +#include "src/formula/OptimizingOperator.h" #include "src/modelchecker/ForwardDeclarations.h" @@ -69,12 +70,12 @@ class INoBoundOperatorModelChecker { * @see AbstractFormula */ template -class NoBoundOperator: public storm::formula::AbstractFormula { +class NoBoundOperator: public storm::formula::AbstractFormula, public OptimizingOperator { public: /*! * Empty constructor */ - NoBoundOperator() : optimalityOperator(false), minimumOperator(false) { + NoBoundOperator() { this->pathFormula = nullptr; } @@ -83,7 +84,7 @@ public: * * @param pathFormula The child node. */ - NoBoundOperator(AbstractPathFormula* pathFormula) : optimalityOperator(false), minimumOperator(false) { + NoBoundOperator(AbstractPathFormula* pathFormula) { this->pathFormula = pathFormula; } @@ -95,7 +96,7 @@ public: * maximizing operator. */ NoBoundOperator(AbstractPathFormula* pathFormula, bool minimumOperator) - : optimalityOperator(true), minimumOperator(minimumOperator) { + : OptimizingOperator(minimumOperator) { this->pathFormula = pathFormula; } @@ -154,34 +155,8 @@ public: return checker.conforms(this->pathFormula); } - /*! - * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator. - * @returns True if the operator is an optimizing operator. - */ - bool isOptimalityOperator() const { - return optimalityOperator; - } - - /*! - * Retrieves whether the operator is a minimizing operator given that it is an optimality - * operator. - * @returns True if the operator is an optimizing operator and it is a minimizing operator and - * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator. - */ - bool isMinimumOperator() const { - return optimalityOperator && minimumOperator; - } - private: AbstractPathFormula* pathFormula; - - // A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator - // over a nondeterministic model. - bool optimalityOperator; - - // In the case this operator is an optimizing operator, this flag indicates whether it is - // looking for the minimum or the maximum value. - bool minimumOperator; }; } /* namespace formula */ diff --git a/src/formula/OptimizingOperator.h b/src/formula/OptimizingOperator.h new file mode 100644 index 000000000..030655fce --- /dev/null +++ b/src/formula/OptimizingOperator.h @@ -0,0 +1,56 @@ +#ifndef STORM_FORMULA_OPTIMIZINGOPERATOR_H_ +#define STORM_FORMULA_OPTIMIZINGOPERATOR_H_ + +namespace storm { + +namespace formula { + +class OptimizingOperator { +public: + /*! + * Empty constructor + */ + OptimizingOperator() : optimalityOperator(false), minimumOperator(false) { + } + + /*! + * Constructor + * + * @param minimumOperator A flag indicating whether this operator is a minimizing or a maximizing operator. + */ + OptimizingOperator(bool minimumOperator) : optimalityOperator(true), minimumOperator(minimumOperator) { + } + + /*! + * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator. + * @returns True if the operator is an optimizing operator. + */ + bool isOptimalityOperator() const { + return optimalityOperator; + } + + /*! + * Retrieves whether the operator is a minimizing operator given that it is an optimality + * operator. + * @returns True if the operator is an optimizing operator and it is a minimizing operator and + * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator. + */ + bool isMinimumOperator() const { + return optimalityOperator && minimumOperator; + } + +private: + // A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator + // over a nondeterministic model. + bool optimalityOperator; + + // In the case this operator is an optimizing operator, this flag indicates whether it is + // looking for the minimum or the maximum value. + bool minimumOperator; +}; + +} /* namespace formula */ + +} /* namespace storm */ + +#endif /* STORM_FORMULA_OPTIMIZINGOPERATOR_H_ */ diff --git a/src/formula/PathBoundOperator.h b/src/formula/PathBoundOperator.h index f18bc3977..b838b9bc0 100644 --- a/src/formula/PathBoundOperator.h +++ b/src/formula/PathBoundOperator.h @@ -11,6 +11,8 @@ #include "src/formula/AbstractStateFormula.h" #include "src/formula/AbstractPathFormula.h" #include "src/formula/AbstractFormulaChecker.h" +#include "src/formula/OptimizingOperator.h" + #include "src/modelchecker/ForwardDeclarations.h" #include "src/utility/ConstTemplates.h" @@ -42,7 +44,7 @@ template class PathBoundOperator; * @see AbstractFormula */ template -class PathBoundOperator : public AbstractStateFormula { +class PathBoundOperator : public AbstractStateFormula, public OptimizingOperator { public: enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL }; @@ -55,8 +57,7 @@ public: * @param pathFormula The child node */ PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula) - : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), - optimalityOperator(false), minimumOperator(false) { + : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) { // Intentionally left empty } @@ -69,8 +70,7 @@ public: * @param minimumOperator Indicator, if operator should be minimum or maximum operator. */ PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) - : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), - optimalityOperator(true), minimumOperator(minimumOperator) { + : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) { // Intentionally left empty } @@ -176,36 +176,10 @@ public: return checker.conforms(this->pathFormula); } - /*! - * Retrieves whether the operator is to be interpreted as an optimizing (i.e. min/max) operator. - * @returns True if the operator is an optimizing operator. - */ - bool isOptimalityOperator() const { - return optimalityOperator; - } - - /*! - * Retrieves whether the operator is a minimizing operator given that it is an optimality - * operator. - * @returns True if the operator is an optimizing operator and it is a minimizing operator and - * false otherwise, i.e. if it is either not an optimizing operator or not a minimizing operator. - */ - bool isMinimumOperator() const { - return optimalityOperator && minimumOperator; - } - private: ComparisonType comparisonOperator; T bound; AbstractPathFormula* pathFormula; - - // A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator - // over a nondeterministic model. - bool optimalityOperator; - - // In the case this operator is an optimizing operator, this flag indicates whether it is - // looking for the minimum or the maximum value. - bool minimumOperator; }; } //namespace formula diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h index 7104da47a..14429c677 100644 --- a/src/formula/ProbabilisticBoundOperator.h +++ b/src/formula/ProbabilisticBoundOperator.h @@ -11,6 +11,7 @@ #include "AbstractStateFormula.h" #include "AbstractPathFormula.h" #include "src/formula/PathBoundOperator.h" +#include "src/formula/OptimizingOperator.h" #include "utility/ConstTemplates.h" namespace storm { @@ -72,8 +73,14 @@ public: * @param pathFormula The child node */ ProbabilisticBoundOperator( - typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) : - PathBoundOperator(comparisonRelation, bound, pathFormula) { + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula) + : PathBoundOperator(comparisonRelation, bound, pathFormula) { + // Intentionally left empty + } + + ProbabilisticBoundOperator( + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) + : PathBoundOperator(comparisonRelation, bound, pathFormula, minimumOperator){ // Intentionally left empty } diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h index ec507176a..f602f89b9 100644 --- a/src/formula/RewardBoundOperator.h +++ b/src/formula/RewardBoundOperator.h @@ -74,6 +74,12 @@ public: // Intentionally left empty } + RewardBoundOperator( + typename PathBoundOperator::ComparisonType comparisonRelation, T bound, AbstractPathFormula* pathFormula, bool minimumOperator) + : PathBoundOperator(comparisonRelation, bound, pathFormula, minimumOperator) { + // Intentionally left empty + } + /*! * @returns a string representation of the formula */