FormulaInformation: Also track whether a formula contains a long-run average formula

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;
+        }
     }
 }

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;
         };
         
     }

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<FormulaInformation>(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 {