(LTL) FormulaInformation: add containsComplexPathFormula()

We want to differentiate between a simple path formula (single G, F,
U, X, with negation over state formulas) and complex path formulas
(nested temporal operators, conjunction/disjunction, etc).

Adapt FormulaInformation and FormulaInformationVisitor accordingly.

Additionally, we tweak the FormulaInformationVisitor so that we can
optionally prohibit recursing into operator subformulas (e.g.,
P>0[...]). For PRCTL*, such subformulas are treated just as state
subformulas, and we would like to have the ability to get
FormulaInformation just for the structure of the "surface-level"
formula, without looking into the probability, long-run, reward,
... sub-formulas.

refactor FormulaInformationVisitor to support stopping recursion into nested operators and for detecting complex path formulas

 Conflicts:
	src/storm/logic/Formula.cpp

src/storm/logic/Formula.cpp

@@ -192,9 +192,8 @@ namespace storm {
             return checker.conformsToSpecification(*this, fragment);
         }
 
-        FormulaInformation Formula::info() const {
-            FormulaInformationVisitor visitor;
-            return visitor.getInformation(*this);
+        FormulaInformation Formula::info(bool recurseIntoOperators) const {
+            return FormulaInformationVisitor::getInformation(*this, recurseIntoOperators);
         }
 
         std::shared_ptr<Formula const> Formula::getTrueFormula() {

src/storm/logic/Formula.h

@@ -100,7 +100,7 @@ namespace storm {
             virtual bool hasQuantitativeResult() const;
 
             bool isInFragment(FragmentSpecification const& fragment) const;
-            FormulaInformation info() const;
+            FormulaInformation info(bool recurseIntoOperators = true) const;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0;
 

src/storm/logic/FormulaInformation.cpp

@@ -2,7 +2,7 @@
 
 namespace storm {
     namespace logic {
-        FormulaInformation::FormulaInformation() : mContainsRewardOperator(false), mContainsNextFormula(false), mContainsBoundedUntilFormula(false), mContainsCumulativeRewardFormula(false), mContainsRewardBoundedFormula(false), mContainsLongRunFormula(false) {
+        FormulaInformation::FormulaInformation() : mContainsRewardOperator(false), mContainsNextFormula(false), mContainsBoundedUntilFormula(false), mContainsCumulativeRewardFormula(false), mContainsRewardBoundedFormula(false), mContainsLongRunFormula(false), mContainsComplexPathFormula(false) {
             // Intentionally left empty
         }
         
@@ -30,6 +30,10 @@ namespace storm {
             return this->mContainsLongRunFormula;
         }
         
+        bool FormulaInformation::containsComplexPathFormula() const {
+            return this->mContainsComplexPathFormula;
+        }
+
         FormulaInformation FormulaInformation::join(FormulaInformation const& other) {
             FormulaInformation result;
             result.mContainsRewardOperator = this->containsRewardOperator() || other.containsRewardOperator();
@@ -38,6 +42,7 @@ namespace storm {
             result.mContainsCumulativeRewardFormula = this->containsCumulativeRewardFormula() || other.containsCumulativeRewardFormula();
             result.mContainsRewardBoundedFormula = this->containsRewardBoundedFormula() || other.containsRewardBoundedFormula();
             result.mContainsLongRunFormula = this->containsLongRunFormula() || other.containsLongRunFormula();
+            result.mContainsComplexPathFormula = this->containsComplexPathFormula() || other.containsComplexPathFormula();
             return result;
         }
         
@@ -70,5 +75,11 @@ namespace storm {
             this->mContainsLongRunFormula = newValue;
             return *this;
         }
+
+        FormulaInformation& FormulaInformation::setContainsComplexPathFormula(bool newValue) {
+            this->mContainsComplexPathFormula = newValue;
+            return *this;
+        }
+
     }
 }

src/storm/logic/FormulaInformation.h

@@ -18,6 +18,7 @@ namespace storm {
             bool containsCumulativeRewardFormula() const;
             bool containsRewardBoundedFormula() const;
             bool containsLongRunFormula() const;
+            bool containsComplexPathFormula() const;
             
             FormulaInformation join(FormulaInformation const& other);
             
@@ -27,6 +28,7 @@ namespace storm {
             FormulaInformation& setContainsCumulativeRewardFormula(bool newValue = true);
             FormulaInformation& setContainsRewardBoundedFormula(bool newValue = true);
             FormulaInformation& setContainsLongRunFormula(bool newValue = true);
+            FormulaInformation& setContainsComplexPathFormula(bool newValue = true);
             
         private:
             bool mContainsRewardOperator;
@@ -35,6 +37,7 @@ namespace storm {
             bool mContainsCumulativeRewardFormula;
             bool mContainsRewardBoundedFormula;
             bool mContainsLongRunFormula;
+            bool mContainsComplexPathFormula;
         };
         
     }

src/storm/logic/FormulaInformationVisitor.cpp

@@ -4,11 +4,15 @@
 
 namespace storm {
     namespace logic {
-        FormulaInformation FormulaInformationVisitor::getInformation(Formula const& f) const {
-            boost::any result = f.accept(*this, boost::any());
+        FormulaInformation FormulaInformationVisitor::getInformation(Formula const& f, bool recurseIntoOperators) {
+            FormulaInformationVisitor visitor(recurseIntoOperators);
+            boost::any result = f.accept(visitor, boost::any());
             return boost::any_cast<FormulaInformation>(result);
         }
         
+        FormulaInformationVisitor::FormulaInformationVisitor(bool recurseIntoOperators) : recurseIntoOperators(recurseIntoOperators) {
+        }
+
         boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const {
             return FormulaInformation();
         }
@@ -22,7 +26,8 @@ namespace storm {
         }
         
         boost::any FormulaInformationVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
-            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+            FormulaInformation result = boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+            return result.setContainsComplexPathFormula();
         }
 
         boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
@@ -46,10 +51,16 @@ namespace storm {
                 for (unsigned i = 0; i < f.getDimension(); ++i) {
                     result.join(boost::any_cast<FormulaInformation>(f.getLeftSubformula(i).accept(*this, data)));
                     result.join(boost::any_cast<FormulaInformation>(f.getRightSubformula(i).accept(*this, data)));
+                    if (f.getLeftSubformula(i).isPathFormula() || f.getRightSubformula(i).isPathFormula()) {
+                        result.setContainsComplexPathFormula();
+                    }
                 }
             } else {
                 result.join(boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)));
                 result.join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this, data)));
+                if (f.getLeftSubformula().isPathFormula() || f.getRightSubformula().isPathFormula()) {
+                    result.setContainsComplexPathFormula();
+                }
             }
             return result;
         }
@@ -70,7 +81,11 @@ namespace storm {
         }
 
         boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
-            return f.getSubformula().accept(*this, data);
+            FormulaInformation result = boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data));
+            if (f.getSubformula().isPathFormula()) {
+                result.setContainsComplexPathFormula();
+            }
+            return result;
         }
 
         boost::any FormulaInformationVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
@@ -78,7 +93,11 @@ namespace storm {
         }
 
         boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
-            return f.getSubformula().accept(*this, data);
+            FormulaInformation result = boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data));
+            if (f.getSubformula().isPathFormula()) {
+                result.setContainsComplexPathFormula();
+            }
+            return result;
         }
 
         boost::any FormulaInformationVisitor::visit(GameFormula const& f, boost::any const& data) const {
@@ -92,7 +111,9 @@ namespace storm {
         boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
             FormulaInformation result;
             result.setContainsLongRunFormula(true);
-            result.join(boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)));
+            if (recurseIntoOperators) {
+                result.join(boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)));
+	    }
             return result;
         }
 
@@ -104,26 +125,45 @@ namespace storm {
 
         boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
             FormulaInformation result;
-            for(auto const& subF : f.getSubformulas()){
-                result.join(boost::any_cast<FormulaInformation>(subF->accept(*this, data)));
+            if (recurseIntoOperators) {
+                for(auto const& subF : f.getSubformulas()){
+                    result.join(boost::any_cast<FormulaInformation>(subF->accept(*this, data)));
+                }
             }
             return result;
         }
         
         boost::any FormulaInformationVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
-            return f.getSubformula().accept(*this, data);
+            // TODO (joachim): check is this correct?
+            if (recurseIntoOperators) {
+                return f.getSubformula().accept(*this, data);
+	    } else {
+	        return FormulaInformation();
+	    }
         }
         
         boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
-            return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsNextFormula();
+            FormulaInformation result = boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsNextFormula();
+            if (f.getSubformula().isPathFormula()) {
+                result.setContainsComplexPathFormula();
+            }
+            return result;
         }
         
         boost::any FormulaInformationVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
-            return f.getSubformula().accept(*this, data);
+            if (recurseIntoOperators) {
+                return f.getSubformula().accept(*this, data);
+            } else {
+                return FormulaInformation();
+            }
         }
         
         boost::any FormulaInformationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
-            return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsRewardOperator();
+            if (recurseIntoOperators) {
+                return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsRewardOperator();
+            } else {
+                return FormulaInformation();
+            }
         }
         
         boost::any FormulaInformationVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
@@ -135,17 +175,25 @@ namespace storm {
         }
         
         boost::any FormulaInformationVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
-            return f.getSubformula().accept(*this, data);
+            FormulaInformation result = boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data));
+            result.setContainsComplexPathFormula();
+            return result;
         }
 
         boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const {
-            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+            FormulaInformation result = boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+            if (f.getLeftSubformula().isPathFormula() || f.getRightSubformula().isPathFormula()) {
+                result.setContainsComplexPathFormula();
+            }
+            return result;
         }
 
         boost::any FormulaInformationVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
             FormulaInformation info;
-            for (auto& mapped : f.getAPMapping()) {
-                info = info.join(boost::any_cast<FormulaInformation>(mapped.second->accept(*this, data)));
+            if (recurseIntoOperators) {
+                for (auto& mapped : f.getAPMapping()) {
+                    info = info.join(boost::any_cast<FormulaInformation>(mapped.second->accept(*this, data)));
+                }
             }
             return info;
         }

src/storm/logic/FormulaInformationVisitor.h

@@ -9,8 +9,14 @@ namespace storm {
         
         class FormulaInformationVisitor : public FormulaVisitor {
         public:
-            FormulaInformation getInformation(Formula const& f) const;
-            
+            static FormulaInformation getInformation(Formula const& f, bool recurseIntoOperators = true);
+
+            explicit FormulaInformationVisitor(bool recurseIntoOperators);
+            FormulaInformationVisitor(FormulaInformationVisitor const& other) = default;
+            FormulaInformationVisitor(FormulaInformationVisitor&& other) = default;
+            FormulaInformationVisitor& operator=(FormulaInformationVisitor const& other) = default;
+            FormulaInformationVisitor& operator=(FormulaInformationVisitor&& other) = default;
+
             virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
@@ -37,6 +43,9 @@ namespace storm {
             virtual boost::any visit(UnaryBooleanPathFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
+
+        private:
+            bool recurseIntoOperators;
         };
         
     }