diff --git a/src/storm/logic/FormulaInformation.cpp b/src/storm/logic/FormulaInformation.cpp index a6f471922..50ddf2e76 100644 --- a/src/storm/logic/FormulaInformation.cpp +++ b/src/storm/logic/FormulaInformation.cpp @@ -26,6 +26,10 @@ namespace storm { return this->mContainsRewardBoundedFormula; } + bool FormulaInformation::containsLongRunFormula() const { + return this->mContainsLongRunFormula; + } + FormulaInformation FormulaInformation::join(FormulaInformation const& other) { FormulaInformation result; result.mContainsRewardOperator = this->containsRewardOperator() || other.containsRewardOperator(); @@ -33,6 +37,7 @@ namespace storm { result.mContainsBoundedUntilFormula = this->containsBoundedUntilFormula() || other.containsBoundedUntilFormula(); result.mContainsCumulativeRewardFormula = this->containsCumulativeRewardFormula() || other.containsCumulativeRewardFormula(); result.mContainsRewardBoundedFormula = this->containsRewardBoundedFormula() || other.containsRewardBoundedFormula(); + result.mContainsLongRunFormula = this->containsLongRunFormula() || other.containsLongRunFormula(); return result; } @@ -60,5 +65,10 @@ namespace storm { this->mContainsRewardBoundedFormula = newValue; return *this; } + + FormulaInformation& FormulaInformation::setContainsLongRunFormula(bool newValue) { + this->mContainsLongRunFormula = newValue; + return *this; + } } } diff --git a/src/storm/logic/FormulaInformation.h b/src/storm/logic/FormulaInformation.h index 06e1ff4ea..6c2c320b2 100644 --- a/src/storm/logic/FormulaInformation.h +++ b/src/storm/logic/FormulaInformation.h @@ -17,6 +17,7 @@ namespace storm { bool containsBoundedUntilFormula() const; bool containsCumulativeRewardFormula() const; bool containsRewardBoundedFormula() const; + bool containsLongRunFormula() const; FormulaInformation join(FormulaInformation const& other); @@ -25,6 +26,7 @@ namespace storm { FormulaInformation& setContainsBoundedUntilFormula(bool newValue = true); FormulaInformation& setContainsCumulativeRewardFormula(bool newValue = true); FormulaInformation& setContainsRewardBoundedFormula(bool newValue = true); + FormulaInformation& setContainsLongRunFormula(bool newValue = true); private: bool mContainsRewardOperator; @@ -32,6 +34,7 @@ namespace storm { bool mContainsBoundedUntilFormula; bool mContainsCumulativeRewardFormula; bool mContainsRewardBoundedFormula; + bool mContainsLongRunFormula; }; } diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp index b3ad356db..e4e9a15ed 100644 --- a/src/storm/logic/FormulaInformationVisitor.cpp +++ b/src/storm/logic/FormulaInformationVisitor.cpp @@ -78,11 +78,16 @@ namespace storm { } boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { - return f.getSubformula().accept(*this, data); + FormulaInformation result; + result.setContainsLongRunFormula(true); + result.join(boost::any_cast(f.getSubformula().accept(*this, data))); + return result; } boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const { - return FormulaInformation(); + FormulaInformation result; + result.setContainsLongRunFormula(true); + return result; } boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {