more refactoring of formula classes: in particular fragment checking

Former-commit-id: 544c5f953f

src/builder/DdPrismModelBuilder.cpp

@@ -227,11 +227,9 @@ namespace storm {
 
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
-                if (formula.containsRewardOperator()) {
                 std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
                 rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
             }
-            }
             
             // Extract all the labels used in the formula.
             std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();

src/builder/ExplicitPrismModelBuilder.cpp

@@ -185,11 +185,9 @@ namespace storm {
             
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
-                if (formula.containsRewardOperator()) {
                 std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
                 rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
             }
-            }
             
             // Extract all the labels used in the formula.
             if (!buildAllLabels) {

src/logic/AtomicExpressionFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/AtomicExpressionFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         AtomicExpressionFormula::AtomicExpressionFormula(storm::expressions::Expression const& expression) : expression(expression) {
@@ -10,20 +12,8 @@ namespace storm {
             return true;
         }
         
-        bool AtomicExpressionFormula::isPctlStateFormula() const {
-            return true;
-        }
-        
-        bool AtomicExpressionFormula::isPctlWithConditionalStateFormula() const {
-            return true;
-        }
-                
-        bool AtomicExpressionFormula::isLtlFormula() const {
-            return true;
-        }
-        
-        bool AtomicExpressionFormula::isPropositionalFormula() const {
-            return true;
+        boost::any AtomicExpressionFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         storm::expressions::Expression const& AtomicExpressionFormula::getExpression() const {

src/logic/AtomicExpressionFormula.h

@@ -15,10 +15,7 @@ namespace storm {
             
             virtual bool isAtomicExpressionFormula() const override;
             
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool isPropositionalFormula() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             storm::expressions::Expression const& getExpression() const;
             

src/logic/AtomicLabelFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/AtomicLabelFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         AtomicLabelFormula::AtomicLabelFormula(std::string const& label) : label(label) {
@@ -10,20 +12,8 @@ namespace storm {
             return true;
         }
         
-        bool AtomicLabelFormula::isPctlStateFormula() const {
-            return true;
-        }
-    
-        bool AtomicLabelFormula::isPctlWithConditionalStateFormula() const {
-            return true;
-        }
-        
-        bool AtomicLabelFormula::isLtlFormula() const {
-            return true;
-        }
-        
-        bool AtomicLabelFormula::isPropositionalFormula() const {
-            return true;
+        boost::any AtomicLabelFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         std::string const& AtomicLabelFormula::getLabel() const {

src/logic/AtomicLabelFormula.h

@@ -17,10 +17,7 @@ namespace storm {
             
             virtual bool isAtomicLabelFormula() const override;
 
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool isPropositionalFormula() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             std::string const& getLabel() const;
             

src/logic/BinaryBooleanStateFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/BinaryBooleanStateFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         BinaryBooleanStateFormula::BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryStateFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
@@ -10,8 +12,8 @@ namespace storm {
             return true;
         }
         
-        bool BinaryBooleanStateFormula::isPropositionalFormula() const {
-            return this->getLeftSubformula().isPropositionalFormula() && this->getRightSubformula().isPropositionalFormula();
+        boost::any BinaryBooleanStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         BinaryBooleanStateFormula::OperatorType BinaryBooleanStateFormula::getOperator() const {

src/logic/BinaryBooleanStateFormula.h

@@ -19,7 +19,7 @@ namespace storm {
             
             virtual bool isBinaryBooleanStateFormula() const override;
             
-            virtual bool isPropositionalFormula() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             OperatorType getOperator() const;
             

src/logic/BinaryPathFormula.cpp

@@ -10,46 +10,6 @@ namespace storm {
             return true;
         }
                 
-        bool BinaryPathFormula::isPctlPathFormula() const {
-            return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
-        }
-        
-        bool BinaryPathFormula::isPctlWithConditionalPathFormula() const {
-            return this->getLeftSubformula().isPctlWithConditionalPathFormula() && this->getRightSubformula().isPctlWithConditionalPathFormula();
-        }
-        
-        bool BinaryPathFormula::isCslPathFormula() const {
-            return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula();
-        }
-        
-        bool BinaryPathFormula::isLtlFormula() const {
-            return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
-        }
-        
-        bool BinaryPathFormula::containsBoundedUntilFormula() const {
-            return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula();
-        }
-        
-        bool BinaryPathFormula::containsNextFormula() const {
-            return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula();
-        }
-        
-        bool BinaryPathFormula::containsProbabilityOperator() const {
-            return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
-        }
-        
-        bool BinaryPathFormula::containsNestedProbabilityOperators() const {
-            return this->getLeftSubformula().containsNestedProbabilityOperators() || this->getRightSubformula().containsNestedProbabilityOperators();
-        }
-        
-        bool BinaryPathFormula::containsRewardOperator() const {
-            return this->getLeftSubformula().containsRewardOperator() || this->getRightSubformula().containsRewardOperator();
-        }
-        
-        bool BinaryPathFormula::containsNestedRewardOperators() const {
-            return this->getLeftSubformula().containsNestedRewardOperators() || this->getRightSubformula().containsNestedRewardOperators();
-        }
-        
         Formula const& BinaryPathFormula::getLeftSubformula() const {
             return *leftSubformula;
         }

src/logic/BinaryPathFormula.h

@@ -17,17 +17,6 @@ namespace storm {
             
             virtual bool isBinaryPathFormula() const override;
             
-            virtual bool isPctlPathFormula() const override;
-            virtual bool isPctlWithConditionalPathFormula() const override;
-            virtual bool isCslPathFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool containsBoundedUntilFormula() const override;
-            virtual bool containsNextFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
-            virtual bool containsRewardOperator() const override;
-            virtual bool containsNestedRewardOperators() const override;
-            
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;
             

src/logic/BinaryStateFormula.cpp

@@ -10,46 +10,6 @@ namespace storm {
             return true;
         }
                 
-        bool BinaryStateFormula::isPctlStateFormula() const {
-            return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
-        }
-        
-        bool BinaryStateFormula::isPctlWithConditionalStateFormula() const {
-            return this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula();
-        }
-
-        bool BinaryStateFormula::isCslStateFormula() const {
-            return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula();
-        }
-        
-        bool BinaryStateFormula::isLtlFormula() const {
-            return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
-        }
-        
-        bool BinaryStateFormula::containsBoundedUntilFormula() const {
-            return this->getLeftSubformula().containsBoundedUntilFormula() || this->getRightSubformula().containsBoundedUntilFormula();
-        }
-        
-        bool BinaryStateFormula::containsNextFormula() const {
-            return this->getLeftSubformula().containsNextFormula() || this->getRightSubformula().containsNextFormula();
-        }
-        
-        bool BinaryStateFormula::containsProbabilityOperator() const {
-            return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
-        }
-        
-        bool BinaryStateFormula::containsNestedProbabilityOperators() const {
-            return this->getLeftSubformula().containsNestedProbabilityOperators() || this->getRightSubformula().containsNestedProbabilityOperators();
-        }
-        
-        bool BinaryStateFormula::containsRewardOperator() const {
-            return this->getLeftSubformula().containsRewardOperator() || this->getRightSubformula().containsRewardOperator();
-        }
-        
-        bool BinaryStateFormula::containsNestedRewardOperators() const {
-            return this->containsNestedRewardOperators() || this->getRightSubformula().containsNestedRewardOperators();
-        }
-        
         Formula const& BinaryStateFormula::getLeftSubformula() const {
             return *leftSubformula;
         }

src/logic/BinaryStateFormula.h

@@ -15,17 +15,6 @@ namespace storm {
             
             virtual bool isBinaryStateFormula() const override;
 
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool isCslStateFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool containsBoundedUntilFormula() const override;
-            virtual bool containsNextFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
-            virtual bool containsRewardOperator() const override;
-            virtual bool containsNestedRewardOperators() const override;
-            
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;
             

src/logic/BooleanLiteralFormula.cpp

@@ -1,11 +1,17 @@
 #include "src/logic/BooleanLiteralFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         BooleanLiteralFormula::BooleanLiteralFormula(bool value) : value(value) {
             // Intenionally left empty.
         }
         
+        bool BooleanLiteralFormula::isBooleanLiteralFormula() const {
+            return true;
+        }
+
         bool BooleanLiteralFormula::isTrueFormula() const {
             return value;
         }
@@ -14,24 +20,8 @@ namespace storm {
             return !value;
         }
         
-        bool BooleanLiteralFormula::isPctlStateFormula() const {
-            return true;
-        }
-        
-        bool BooleanLiteralFormula::isPctlWithConditionalStateFormula() const {
-            return true;
-        }
-        
-        bool BooleanLiteralFormula::isLtlFormula() const {
-            return true;
-        }
-        
-        bool BooleanLiteralFormula::isPropositionalFormula() const {
-            return true;
-        }
-        
-        bool BooleanLiteralFormula::isBooleanLiteralFormula() const {
-            return true;
+        boost::any BooleanLiteralFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         std::shared_ptr<Formula> BooleanLiteralFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {

src/logic/BooleanLiteralFormula.h

@@ -17,10 +17,7 @@ namespace storm {
             virtual bool isTrueFormula() const override;
             virtual bool isFalseFormula() const override;
             
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool isPropositionalFormula() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             

src/logic/BoundedUntilFormula.cpp

@@ -3,6 +3,8 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, double lowerBound, double upperBound) : BinaryPathFormula(leftSubformula, rightSubformula), bounds(std::make_pair(lowerBound, upperBound)) {
@@ -22,28 +24,16 @@ namespace storm {
             return true;
         }
         
-        bool BoundedUntilFormula::containsBoundedUntilFormula() const {
-            return true;
-        }
-        
-        bool BoundedUntilFormula::hasDiscreteTimeBound() const {
-            return bounds.which() == 0;
-        }
-        
-        bool BoundedUntilFormula::isValidProbabilityPathFormula() const {
+        bool BoundedUntilFormula::isProbabilityPathFormula() const {
             return true;
         }
         
-        bool BoundedUntilFormula::isPctlPathFormula() const {
-            return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
-        }
-        
-        bool BoundedUntilFormula::isPctlWithConditionalPathFormula() const {
-            return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula();
+        boost::any BoundedUntilFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
 
-        bool BoundedUntilFormula::isCslPathFormula() const {
-            return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula();
+        bool BoundedUntilFormula::hasDiscreteTimeBound() const {
+            return bounds.which() == 0;
         }
                 
         std::pair<double, double> const& BoundedUntilFormula::getIntervalBounds() const {

src/logic/BoundedUntilFormula.h

@@ -15,18 +15,15 @@ namespace storm {
             
             virtual bool isBoundedUntilFormula() const override;
 
-            virtual bool containsBoundedUntilFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             bool hasDiscreteTimeBound() const;
             
             std::pair<double, double> const& getIntervalBounds() const;
             uint_fast64_t getDiscreteTimeBound() const;
 
-            virtual bool isValidProbabilityPathFormula() const override;
-            virtual bool isPctlWithConditionalPathFormula() const override;
-            virtual bool isPctlPathFormula() const override;
-            virtual bool isCslPathFormula() const override;
-
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;

src/logic/ConditionalFormula.cpp

@@ -0,0 +1,42 @@
+#include "src/logic/ConditionalFormula.h"
+
+#include "src/logic/FormulaVisitor.h"
+
+namespace storm {
+    namespace logic {
+        ConditionalFormula::ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, Context context) : subformula(subformula), conditionFormula(conditionFormula), context(context)  {
+            // Intentionally left empty.
+        }
+        
+        Formula const& ConditionalFormula::getSubformula() const {
+            return *subformula;
+        }
+        
+        Formula const& ConditionalFormula::getConditionFormula() const {
+            return *conditionFormula;
+        }
+        
+        bool ConditionalFormula::isConditionalProbabilityFormula() const {
+            return context == Context::Probability;
+        }
+        
+        bool ConditionalFormula::isConditionalRewardFormula() const {
+            return context == Context::Reward;
+        }
+        
+        boost::any ConditionalFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        std::shared_ptr<Formula> ConditionalFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+            return std::make_shared<ConditionalFormula>(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution));
+        }
+        
+        std::ostream& ConditionalFormula::writeToStream(std::ostream& out) const {
+            this->getSubformula().writeToStream(out);
+            out << " || ";
+            this->getConditionFormula().writeToStream(out);
+            return out;
+        }
+    }
+}

src/logic/ConditionalFormula.h

@@ -0,0 +1,38 @@
+#ifndef STORM_LOGIC_CONDITIONALFORMULA_H_
+#define STORM_LOGIC_CONDITIONALFORMULA_H_
+
+#include "src/logic/BinaryPathFormula.h"
+
+namespace storm {
+    namespace logic {
+        class ConditionalFormula : public Formula {
+        public:
+            enum class Context { Probability, Reward };
+            
+            ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, Context context = Context::Probability);
+            
+            virtual ~ConditionalFormula() {
+                // Intentionally left empty.
+            }
+            
+            Formula const& getSubformula() const;
+            Formula const& getConditionFormula() const;
+
+            virtual bool isConditionalProbabilityFormula() const override;
+            virtual bool isConditionalRewardFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
+            
+        private:
+            std::shared_ptr<Formula const> subformula;
+            std::shared_ptr<Formula const> conditionFormula;
+            Context context;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_CONDITIONALFORMULA_H_ */

src/logic/ConditionalPathFormula.cpp

@@ -1,40 +0,0 @@
-#include "src/logic/ConditionalPathFormula.h"
-
-namespace storm {
-    namespace logic {
-        ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, bool isRewardFormula) : BinaryPathFormula(leftSubformula, rightSubformula), isRewardFormula(isRewardFormula) {
-            // Intentionally left empty.
-        }
-        
-        bool ConditionalPathFormula::isConditionalPathFormula() const {
-            return true;
-        }
-        
-        bool ConditionalPathFormula::isValidProbabilityPathFormula() const {
-            return true;
-        }
-        
-        bool ConditionalPathFormula::isPctlWithConditionalPathFormula() const {
-            return this->getLeftSubformula().isPctlPathFormula() && this->getRightSubformula().isPctlPathFormula();
-        }
-        
-        bool ConditionalPathFormula::isRewardPathFormula() const {
-            return this->isRewardFormula && this->isValidRewardPathFormula();
-        }
-        
-        bool ConditionalPathFormula::isValidRewardPathFormula() const {
-            return this->getLeftSubformula().isRewardPathFormula() && !this->getLeftSubformula().isConditionalPathFormula() && this->getRightSubformula().isPctlPathFormula();
-        }
-        
-        std::shared_ptr<Formula> ConditionalPathFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ConditionalPathFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
-        }
-        
-        std::ostream& ConditionalPathFormula::writeToStream(std::ostream& out) const {
-            this->getLeftSubformula().writeToStream(out);
-            out << " || ";
-            this->getRightSubformula().writeToStream(out);
-            return out;
-        }
-    }
-}

src/logic/ConditionalPathFormula.h

@@ -1,32 +0,0 @@
-#ifndef STORM_LOGIC_CONDITIONALPATHFORMULA_H_
-#define STORM_LOGIC_CONDITIONALPATHFORMULA_H_
-
-#include "src/logic/BinaryPathFormula.h"
-
-namespace storm {
-    namespace logic {
-        class ConditionalPathFormula : public BinaryPathFormula {
-        public:
-            ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, bool isRewardFormula = false);
-            
-            virtual ~ConditionalPathFormula() {
-                // Intentionally left empty.
-            }
-            
-            virtual bool isPctlWithConditionalPathFormula() const override;
-            virtual bool isRewardPathFormula() const override;
-            virtual bool isConditionalPathFormula() const override;
-            virtual bool isValidProbabilityPathFormula() const override;
-            virtual bool isValidRewardPathFormula() const override;
-
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
-        private:
-            bool isRewardFormula;
-        };
-    }
-}
-
-#endif /* STORM_LOGIC_CONDITIONALPATHFORMULA_H_ */

src/logic/CumulativeRewardFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/CumulativeRewardFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         CumulativeRewardFormula::CumulativeRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) {
@@ -10,16 +12,16 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        bool CumulativeRewardFormula::isRewardPathFormula() const {
+        bool CumulativeRewardFormula::isCumulativeRewardFormula() const {
             return true;
         }
         
-        bool CumulativeRewardFormula::isCumulativeRewardFormula() const {
+        bool CumulativeRewardFormula::isRewardPathFormula() const {
             return true;
         }
         
-        bool CumulativeRewardFormula::isValidRewardPathFormula() const {
-            return true;
+        boost::any CumulativeRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         bool CumulativeRewardFormula::hasDiscreteTimeBound() const {

src/logic/CumulativeRewardFormula.h

@@ -17,9 +17,10 @@ namespace storm {
                 // Intentionally left empty.
             }
 
-            virtual bool isRewardPathFormula() const override;
             virtual bool isCumulativeRewardFormula() const override;
-            virtual bool isValidRewardPathFormula() const override;
+            virtual bool isRewardPathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             

src/logic/EventuallyFormula.cpp

@@ -1,25 +1,39 @@
 #include "src/logic/EventuallyFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
-        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, bool isRewardFormula) : UnaryPathFormula(subformula), isRewardFormula(isRewardFormula) {
+        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, Context context) : UnaryPathFormula(subformula), context(context) {
             // Intentionally left empty.
         }
         
         bool EventuallyFormula::isEventuallyFormula() const {
-            return true;
+            return context == Context::Probability;
+        }
+        
+        bool EventuallyFormula::isReachabilityRewardFormula() const {
+            return context == Context::Reward;
+        }
+        
+        bool EventuallyFormula::isReachbilityExpectedTimeFormula() const {
+            return context == Context::ExpectedTime;
+        }
+        
+        bool EventuallyFormula::isProbabilityPathFormula() const {
+            return this->isEventuallyFormula();
         }
         
         bool EventuallyFormula::isRewardPathFormula() const {
-            return isRewardFormula;
+            return this->isReachabilityRewardFormula();
         }
         
-        bool EventuallyFormula::isValidProbabilityPathFormula() const {
-            return !isRewardFormula;
+        bool EventuallyFormula::isExpectedTimePathFormula() const {
+            return this->isReachbilityExpectedTimeFormula();
         }
         
-        bool EventuallyFormula::isValidRewardPathFormula() const {
-            return isRewardFormula;
+        boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {

src/logic/EventuallyFormula.h

@@ -7,23 +7,29 @@ namespace storm {
     namespace logic {
         class EventuallyFormula : public UnaryPathFormula {
         public:
-            EventuallyFormula(std::shared_ptr<Formula const> const& subformula, bool isRewardFormula = false);
+            enum class Context { Probability, Reward, ExpectedTime };
+            
+            EventuallyFormula(std::shared_ptr<Formula const> const& subformula, Context context = Context::Probability);
             
             virtual ~EventuallyFormula() {
                 // Intentionally left empty.
             }
             
             virtual bool isEventuallyFormula() const override;
+            virtual bool isReachabilityRewardFormula() const override;
+            virtual bool isReachbilityExpectedTimeFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
             virtual bool isRewardPathFormula() const override;
-            virtual bool isValidProbabilityPathFormula() const override;
-            virtual bool isValidRewardPathFormula() const override;
+            virtual bool isExpectedTimePathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
 
         private:
-            bool isRewardFormula;
+            Context context;
         };
     }
 }

src/logic/ExpectedTimeOperatorFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/ExpectedTimeOperatorFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::none, boost::none, subformula) {
@@ -22,20 +24,8 @@ namespace storm {
             return true;
         }
         
-        bool ExpectedTimeOperatorFormula::isPctlStateFormula() const {
-            return this->getSubformula().isPctlStateFormula();
-        }
-        
-        bool ExpectedTimeOperatorFormula::isPctlWithConditionalStateFormula() const {
-            return this->getSubformula().isPctlWithConditionalStateFormula();
-        }
-        
-        bool ExpectedTimeOperatorFormula::containsProbabilityOperator() const {
-            return this->getSubformula().containsProbabilityOperator();
-        }
-        
-        bool ExpectedTimeOperatorFormula::containsNestedProbabilityOperators() const {
-            return this->getSubformula().containsNestedProbabilityOperators();
+        boost::any ExpectedTimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {

src/logic/ExpectedTimeOperatorFormula.h

@@ -3,6 +3,8 @@
 
 #include "src/logic/OperatorFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         class ExpectedTimeOperatorFormula : public OperatorFormula {
@@ -19,10 +21,7 @@ namespace storm {
             
             virtual bool isExpectedTimeOperatorFormula() const override;
 
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             

src/logic/Formula.cpp

@@ -71,135 +71,63 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isConditionalPathFormula() const {
+        bool Formula::isConditionalProbabilityFormula() const {
             return false;
         }
         
-        bool Formula::isNextFormula() const {
-            return false;
-        }
-        
-        bool Formula::isLongRunAverageOperatorFormula() const {
-            return false;
-        }
-        
-        bool Formula::isExpectedTimeOperatorFormula() const {
-            return false;
-        }
-        
-        bool Formula::isCumulativeRewardFormula() const {
-            return false;
-        }
-        
-        bool Formula::isInstantaneousRewardFormula() const {
-            return false;
-        }
-        
-        bool Formula::isLongRunAverageRewardFormula() const {
-            return false;
-        }
-        
-        bool Formula::isProbabilityOperatorFormula() const {
-            return false;
-        }
-        
-        bool Formula::isRewardOperatorFormula() const {
-            return false;
-        }
-        
-        bool Formula::isOperatorFormula() const {
+        bool Formula::isConditionalRewardFormula() const {
             return false;
         }
         
-        bool Formula::isPctlFormula() const {
-            return this->isPctlStateFormula() || this->isPctlPathFormula();
-        }
-        
-        bool Formula::isPctlWithConditionalFormula() const {
-            return this->isPctlWithConditionalStateFormula() || this->isPctlWithConditionalPathFormula();
-        }
-        
-        bool Formula::isRewardFormula() const {
-            return this->isRewardStateFormula() || this->isRewardPathFormula();
-        }
-        
-        bool Formula::isCslFormula() const {
-            return this->isCslStateFormula() || this->isCslPathFormula();
-        }
-        
-        bool Formula::isPctlPathFormula() const {
-            return false;
-        }
-        
-        bool Formula::isPctlStateFormula() const {
-            return false;
-        }
-        
-        bool Formula::isPctlWithConditionalPathFormula() const {
-            return false;
-        }
-        
-        bool Formula::isPctlWithConditionalStateFormula() const {
+        bool Formula::isProbabilityPathFormula() const {
             return false;
         }
         
-        bool Formula::isCslPathFormula() const {
-            return this->isPctlPathFormula();
-        }
-        
-        bool Formula::isCslStateFormula() const {
-            return this->isPctlStateFormula();
-        }
-        
         bool Formula::isRewardPathFormula() const {
             return false;
         }
         
-        bool Formula::isRewardStateFormula() const {
+        bool Formula::isExpectedTimePathFormula() const {
             return false;
         }
         
-        bool Formula::isPltlFormula() const {
-            return false;
-        }
-        
-        bool Formula::isLtlFormula() const {
+        bool Formula::isNextFormula() const {
             return false;
         }
         
-        bool Formula::isPropositionalFormula() const {
+        bool Formula::isLongRunAverageOperatorFormula() const {
             return false;
         }
         
-        bool Formula::isValidProbabilityPathFormula() const {
+        bool Formula::isExpectedTimeOperatorFormula() const {
             return false;
         }
         
-        bool Formula::isValidRewardPathFormula() const {
+        bool Formula::isCumulativeRewardFormula() const {
             return false;
         }
         
-        bool Formula::containsBoundedUntilFormula() const {
+        bool Formula::isInstantaneousRewardFormula() const {
             return false;
         }
         
-        bool Formula::containsNextFormula() const {
+        bool Formula::isLongRunAverageRewardFormula() const {
             return false;
         }
         
-        bool Formula::containsProbabilityOperator() const {
+        bool Formula::isReachbilityExpectedTimeFormula() const {
             return false;
         }
         
-        bool Formula::containsNestedProbabilityOperators() const {
+        bool Formula::isProbabilityOperatorFormula() const {
             return false;
         }
         
-        bool Formula::containsRewardOperator() const {
+        bool Formula::isRewardOperatorFormula() const {
             return false;
         }
         
-        bool Formula::containsNestedRewardOperators() const {
+        bool Formula::isOperatorFormula() const {
             return false;
         }
         
@@ -239,12 +167,12 @@ namespace storm {
             return dynamic_cast<UnaryStateFormula const&>(*this);
         }
         
-        ConditionalPathFormula& Formula::asConditionalPathFormula() {
-            return dynamic_cast<ConditionalPathFormula&>(*this);
+        ConditionalFormula& Formula::asConditionalFormula() {
+            return dynamic_cast<ConditionalFormula&>(*this);
         }
         
-        ConditionalPathFormula const& Formula::asConditionalPathFormula() const {
-            return dynamic_cast<ConditionalPathFormula const&>(*this);
+        ConditionalFormula const& Formula::asConditionalFormula() const {
+            return dynamic_cast<ConditionalFormula const&>(*this);
         }
         
         BinaryBooleanStateFormula& Formula::asBinaryBooleanStateFormula() {

src/logic/Formula.h

@@ -6,37 +6,18 @@
 #include <iostream>
 #include <set>
 
+#include <boost/any.hpp>
+
 #include "src/storage/expressions/Variable.h"
 #include "src/storage/expressions/Expression.h"
 
+#include "src/logic/FormulasForwardDeclarations.h"
+
 namespace storm {
     namespace logic {
-        // Forward-declare all formula classes.
-        class PathFormula;
-        class StateFormula;
-        class BinaryStateFormula;
-        class UnaryStateFormula;
-        class BinaryBooleanStateFormula;
-        class UnaryBooleanStateFormula;
-        class BooleanLiteralFormula;
-        class AtomicExpressionFormula;
-        class AtomicLabelFormula;
-        class UntilFormula;
-        class BoundedUntilFormula;
-        class EventuallyFormula;
-        class GloballyFormula;
-        class BinaryPathFormula;
-        class UnaryPathFormula;
-        class ConditionalPathFormula;
-        class NextFormula;
-        class LongRunAverageOperatorFormula;
-        class ExpectedTimeOperatorFormula;
-        class CumulativeRewardFormula;
-        class InstantaneousRewardFormula;
-        class LongRunAverageRewardFormula;
-        class ProbabilityOperatorFormula;
-        class RewardOperatorFormula;
-        class OperatorFormula;
+
+        // Forward-declare visitor for accept() method.
+        class FormulaVisitor;
 
         // Also foward-declare base model checker class.
         class ModelChecker;
@@ -50,58 +31,56 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& out, Formula const& formula);
 
-            // Methods for querying the exact formula type.
+            // Basic formula types.
             virtual bool isPathFormula() const;
             virtual bool isStateFormula() const;
-            virtual bool isBinaryStateFormula() const;
-            virtual bool isUnaryStateFormula() const;
+            virtual bool isConditionalProbabilityFormula() const;
+            virtual bool isConditionalRewardFormula() const;
+            
+            virtual bool isProbabilityPathFormula() const;
+            virtual bool isRewardPathFormula() const;
+            virtual bool isExpectedTimePathFormula() const;
+
             virtual bool isBinaryBooleanStateFormula() const;
             virtual bool isUnaryBooleanStateFormula() const;
+
+            // Operator formulas.
+            virtual bool isOperatorFormula() const;
+            virtual bool isLongRunAverageOperatorFormula() const;
+            virtual bool isExpectedTimeOperatorFormula() const;
+            virtual bool isProbabilityOperatorFormula() const;
+            virtual bool isRewardOperatorFormula() const;
+
+            // Atomic state formulas.
             virtual bool isBooleanLiteralFormula() const;
             virtual bool isTrueFormula() const;
             virtual bool isFalseFormula() const;
             virtual bool isAtomicExpressionFormula() const;
             virtual bool isAtomicLabelFormula() const;
+
+            // Probability path formulas.
+            virtual bool isNextFormula() const;
             virtual bool isUntilFormula() const;
             virtual bool isBoundedUntilFormula() const;
             virtual bool isEventuallyFormula() const;
             virtual bool isGloballyFormula() const;
-            virtual bool isBinaryPathFormula() const;
-            virtual bool isUnaryPathFormula() const;
-            virtual bool isConditionalPathFormula() const;
-            virtual bool isNextFormula() const;
-            virtual bool isLongRunAverageOperatorFormula() const;
-            virtual bool isExpectedTimeOperatorFormula() const;
+
+            // Reward formulas.
             virtual bool isCumulativeRewardFormula() const;
             virtual bool isInstantaneousRewardFormula() const;
+            virtual bool isReachabilityRewardFormula() const;
             virtual bool isLongRunAverageRewardFormula() const;
-            virtual bool isProbabilityOperatorFormula() const;
-            virtual bool isRewardOperatorFormula() const;
-            virtual bool isOperatorFormula() const;
             
-            bool isPctlFormula() const;
-            bool isPctlWithConditionalFormula() const;
-            bool isRewardFormula() const;
-            bool isCslFormula() const;
-            virtual bool isPctlPathFormula() const;
-            virtual bool isPctlStateFormula() const;
-            virtual bool isPctlWithConditionalPathFormula() const;
-            virtual bool isPctlWithConditionalStateFormula() const;
-            virtual bool isCslPathFormula() const;
-            virtual bool isCslStateFormula() const;
-            virtual bool isRewardPathFormula() const;
-            virtual bool isRewardStateFormula() const;
-            virtual bool isPltlFormula() const;
-            virtual bool isLtlFormula() const;
-            virtual bool isPropositionalFormula() const;
-            virtual bool isValidProbabilityPathFormula() const;
-            virtual bool isValidRewardPathFormula() const;
-            virtual bool containsBoundedUntilFormula() const;
-            virtual bool containsNextFormula() const;
-            virtual bool containsProbabilityOperator() const;
-            virtual bool containsNestedProbabilityOperators() const;
-            virtual bool containsRewardOperator() const;
-            virtual bool containsNestedRewardOperators() const;
+            // Expected time formulas.
+            virtual bool isReachbilityExpectedTimeFormula() const;
+            
+            // Type checks for abstract intermediate classes.
+            virtual bool isBinaryPathFormula() const;
+            virtual bool isBinaryStateFormula() const;
+            virtual bool isUnaryPathFormula() const;
+            virtual bool isUnaryStateFormula() const;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const = 0;
             
             static std::shared_ptr<Formula const> getTrueFormula();
             
@@ -150,8 +129,8 @@ namespace storm {
             UnaryPathFormula& asUnaryPathFormula();
             UnaryPathFormula const& asUnaryPathFormula() const;
             
-            ConditionalPathFormula& asConditionalPathFormula();
-            ConditionalPathFormula const& asConditionalPathFormula() const;
+            ConditionalFormula& asConditionalFormula();
+            ConditionalFormula const& asConditionalFormula() const;
             
             NextFormula& asNextFormula();
             NextFormula const& asNextFormula() const;

src/logic/FormulaVisitor.h

@@ -0,0 +1,36 @@
+#ifndef STORM_LOGIC_FORMULAVISITOR_H_
+#define STORM_LOGIC_FORMULAVISITOR_H_
+
+#include <boost/any.hpp>
+
+#include "src/logic/FormulasForwardDeclarations.h"
+
+namespace storm {
+    namespace logic {
+
+        class FormulaVisitor {
+        public:
+            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0;
+        };
+        
+    }
+}
+
+#endif /* STORM_LOGIC_FORMULAVISITOR_H_ */

src/logic/Formulas.h

@@ -23,7 +23,7 @@
 #include "src/logic/UnaryPathFormula.h"
 #include "src/logic/UnaryStateFormula.h"
 #include "src/logic/UntilFormula.h"
-#include "src/logic/ConditionalPathFormula.h"
+#include "src/logic/ConditionalFormula.h"
 #include "src/logic/ProbabilityOperatorFormula.h"
 #include "src/logic/RewardOperatorFormula.h"
 #include "src/logic/ComparisonType.h"

src/logic/FormulasForwardDeclarations.h

@@ -0,0 +1,36 @@
+#ifndef STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_
+#define STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_
+
+namespace storm {
+    namespace logic {
+        // Forward-declare all formula classes.
+        class Formula;
+        class AtomicExpressionFormula;
+        class AtomicLabelFormula;
+        class BinaryBooleanStateFormula;
+        class BinaryPathFormula;
+        class BinaryStateFormula;
+        class BooleanLiteralFormula;
+        class BoundedUntilFormula;
+        class ConditionalFormula;
+        class CumulativeRewardFormula;
+        class EventuallyFormula;
+        class ExpectedTimeOperatorFormula;
+        class GloballyFormula;
+        class InstantaneousRewardFormula;
+        class LongRunAverageOperatorFormula;
+        class LongRunAverageRewardFormula;
+        class NextFormula;
+        class OperatorFormula;
+        class PathFormula;
+        class ProbabilityOperatorFormula;
+        class RewardOperatorFormula;
+        class StateFormula;
+        class UnaryBooleanStateFormula;
+        class UnaryPathFormula;
+        class UnaryStateFormula;
+        class UntilFormula;
+    }
+}
+
+#endif /* STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ */

src/logic/FragmentChecker.cpp

@@ -0,0 +1,118 @@
+#include "src/logic/FragmentChecker.h"
+
+#include "src/logic/Formulas.h"
+
+namespace storm {
+    namespace logic {
+        bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const {
+            boost::any result = f.accept(*this, specification);
+            return boost::any_cast<bool>(result);
+        }
+        
+        boost::any FragmentChecker::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areAtomicExpressionFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(AtomicLabelFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areAtomicLabelFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            bool result = specification.areBinaryBooleanStateFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, specification));
+            result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, specification));
+            return result;
+        }
+        
+        boost::any FragmentChecker::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areBooleanLiteralFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            bool result = specification.areBoundedUntilFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data));
+            result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
+            return result;
+        }
+        
+        boost::any FragmentChecker::visit(ConditionalFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            bool result = true;
+            if (f.isConditionalProbabilityFormula()) {
+                result &= specification.areConditionalProbabilityFormulasAllowed();
+            } else if (f.Formula::isConditionalRewardFormula()) {
+                result &= specification.areConditionalRewardFormulasFormulasAllowed();
+            }
+            result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            result = result && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data));
+            return result;
+        }
+        
+        boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areCumulativeRewardFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            bool result = specification.areEventuallyFormulasAllowed();
+            result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
+        }
+        
+        boost::any FragmentChecker::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areExpectedTimeOperatorsAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areGloballyFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areInstantaneousRewardFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areLongRunAverageOperatorsAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areLongRunAverageRewardFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areNextFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areProbabilityOperatorsAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areRewardOperatorsAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areUnaryBooleanStateFormulasAllowed();
+        }
+        
+        boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const {
+            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
+            return specification.areUntilFormulasAllowed();
+        }
+    }
+}

src/logic/FragmentChecker.h

@@ -0,0 +1,39 @@
+#ifndef STORM_LOGIC_FRAGMENTCHECKER_H_
+#define STORM_LOGIC_FRAGMENTCHECKER_H_
+
+#include "src/logic/FormulaVisitor.h"
+
+#include "src/logic/FragmentSpecification.h"
+
+namespace storm {
+    namespace logic {
+        
+        class FragmentChecker : public FormulaVisitor {
+        public:
+            bool conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const;
+            
+            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;
+            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+        };
+        
+    }
+}
+
+
+#endif /* STORM_LOGIC_FRAGMENTCHECKER_H_ */

src/logic/FragmentSpecification.cpp

@@ -0,0 +1,209 @@
+#include "src/logic/FragmentSpecification.h"
+
+namespace storm {
+    namespace logic {
+        
+        FragmentSpecification FragmentSpecification::copy() const {
+            return FragmentSpecification(*this);
+        }
+        
+        bool FragmentSpecification::areProbabilityOperatorsAllowed() const {
+            return probabilityOperator;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setProbabilityOperatorsAllowed(bool newValue) {
+            this->probabilityOperator = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areRewardOperatorsAllowed() const {
+            return rewardOperator;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setRewardOperatorsAllowed(bool newValue) {
+            this->rewardOperator = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areExpectedTimeOperatorsAllowed() const {
+            return expectedTimeOperator;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setExpectedTimeOperatorsAllowed(bool newValue) {
+            this->expectedTimeOperator = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areLongRunAverageOperatorsAllowed() const {
+            return longRunAverageOperator;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setLongRunAverageOperatorsAllowed(bool newValue) {
+            this->longRunAverageOperator = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areGloballyFormulasAllowed() const {
+            return globallyFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setGloballyFormulasAllowed(bool newValue) {
+            this->globallyFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areEventuallyFormulasAllowed() const {
+            return eventuallyFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setEventuallyFormulasAllowed(bool newValue) {
+            this->eventuallyFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areNextFormulasAllowed() const {
+            return nextFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setNextFormulasAllowed(bool newValue) {
+            this->nextFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areUntilFormulasAllowed() const {
+            return untilFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setUntilFormulasAllowed(bool newValue) {
+            this->untilFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areBoundedUntilFormulasAllowed() const {
+            return boundedUntilFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setBoundedUntilFormulasAllowed(bool newValue) {
+            this->boundedUntilFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const {
+            return atomicExpressionFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setAtomicExpressionFormulasAllowed(bool newValue) {
+            this->atomicExpressionFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areAtomicLabelFormulasAllowed() const {
+            return atomicLabelFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setAtomicLabelFormulasAllowed(bool newValue) {
+            this->atomicLabelFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areBooleanLiteralFormulasAllowed() const {
+            return booleanLiteralFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setBooleanLiteralFormulasAllowed(bool newValue) {
+            this->booleanLiteralFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areUnaryBooleanStateFormulasAllowed() const {
+            return unaryBooleanStateFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setUnaryBooleanStateFormulasAllowed(bool newValue) {
+            this->unaryBooleanStateFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const {
+            return binaryBooleanStateFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) {
+            this->binaryBooleanStateFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areCumulativeRewardFormulasAllowed() const {
+            return cumulativeRewardFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setCumulativeRewardFormulasAllowed(bool newValue) {
+            this->cumulativeRewardFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areInstantaneousRewardFormulasAllowed() const {
+            return instantaneousRewardFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setInstantaneousFormulasAllowed(bool newValue) {
+            this->instantaneousRewardFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areReachabilityRewardFormulasAllowed() const {
+            return reachabilityRewardFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setReachabilityRewardFormulasAllowed(bool newValue) {
+            this->reachabilityRewardFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areLongRunAverageRewardFormulasAllowed() const {
+            return longRunAverageRewardFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setLongRunAverageRewardFormulasAllowed(bool newValue) {
+            this->longRunAverageRewardFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areConditionalProbabilityFormulasAllowed() const {
+            return conditionalProbabilityFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setConditionalProbabilityFormulasAllowed(bool newValue) {
+            this->conditionalProbabilityFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areConditionalRewardFormulasFormulasAllowed() const {
+            return conditionalRewardFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setConditionalRewardFormulasAllowed(bool newValue) {
+            this->conditionalRewardFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areReachbilityExpectedTimeFormulasAllowed() const {
+            return reachabilityExpectedTimeFormula;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setReachbilityExpectedTimeFormulasAllowed(bool newValue) {
+            this->reachabilityExpectedTimeFormula = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areNestedOperatorsAllowed() const {
+            return this->nestedOperators;
+        }
+            
+        FragmentSpecification& FragmentSpecification::setNestedOperatorsAllowed(bool newValue) {
+            this->nestedOperators = newValue;
+            return *this;
+        }
+        
+    }
+}

src/logic/FragmentSpecification.h

@@ -0,0 +1,112 @@
+#ifndef STORM_LOGIC_FRAGMENTSPECIFICATION_H_
+#define STORM_LOGIC_FRAGMENTSPECIFICATION_H_
+
+namespace storm {
+    namespace logic {
+        class FragmentSpecification {
+        public:
+            FragmentSpecification copy() const;
+            
+            bool areProbabilityOperatorsAllowed() const;
+            FragmentSpecification& setProbabilityOperatorsAllowed(bool newValue);
+            
+            bool areRewardOperatorsAllowed() const;
+            FragmentSpecification& setRewardOperatorsAllowed(bool newValue);
+            
+            bool areExpectedTimeOperatorsAllowed() const;
+            FragmentSpecification& setExpectedTimeOperatorsAllowed(bool newValue);
+
+            bool areLongRunAverageOperatorsAllowed() const;
+            FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue);
+
+            bool areGloballyFormulasAllowed() const;
+            FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
+
+            bool areEventuallyFormulasAllowed() const;
+            FragmentSpecification& setEventuallyFormulasAllowed(bool newValue);
+
+            bool areNextFormulasAllowed() const;
+            FragmentSpecification& setNextFormulasAllowed(bool newValue);
+
+            bool areUntilFormulasAllowed() const;
+            FragmentSpecification& setUntilFormulasAllowed(bool newValue);
+
+            bool areBoundedUntilFormulasAllowed() const;
+            FragmentSpecification& setBoundedUntilFormulasAllowed(bool newValue);
+
+            bool areAtomicExpressionFormulasAllowed() const;
+            FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue);
+
+            bool areAtomicLabelFormulasAllowed() const;
+            FragmentSpecification& setAtomicLabelFormulasAllowed(bool newValue);
+
+            bool areBooleanLiteralFormulasAllowed() const;
+            FragmentSpecification& setBooleanLiteralFormulasAllowed(bool newValue);
+
+            bool areUnaryBooleanStateFormulasAllowed() const;
+            FragmentSpecification& setUnaryBooleanStateFormulasAllowed(bool newValue);
+
+            bool areBinaryBooleanStateFormulasAllowed() const;
+            FragmentSpecification& setBinaryBooleanStateFormulasAllowed(bool newValue);
+
+            bool areCumulativeRewardFormulasAllowed() const;
+            FragmentSpecification& setCumulativeRewardFormulasAllowed(bool newValue);
+
+            bool areInstantaneousRewardFormulasAllowed() const;
+            FragmentSpecification& setInstantaneousFormulasAllowed(bool newValue);
+
+            bool areReachabilityRewardFormulasAllowed() const;
+            FragmentSpecification& setReachabilityRewardFormulasAllowed(bool newValue);
+            
+            bool areLongRunAverageRewardFormulasAllowed() const;
+            FragmentSpecification& setLongRunAverageRewardFormulasAllowed(bool newValue);
+
+            bool areConditionalProbabilityFormulasAllowed() const;
+            FragmentSpecification& setConditionalProbabilityFormulasAllowed(bool newValue);
+
+            bool areConditionalRewardFormulasFormulasAllowed() const;
+            FragmentSpecification& setConditionalRewardFormulasAllowed(bool newValue);
+
+            bool areReachbilityExpectedTimeFormulasAllowed() const;
+            FragmentSpecification& setReachbilityExpectedTimeFormulasAllowed(bool newValue);
+
+            bool areNestedOperatorsAllowed() const;
+            FragmentSpecification& setNestedOperatorsAllowed(bool newValue);
+
+        private:
+            // Flags that indicate whether it is legal to see such a formula.
+            bool probabilityOperator;
+            bool rewardOperator;
+            bool expectedTimeOperator;
+            bool longRunAverageOperator;
+            
+            bool globallyFormula;
+            bool eventuallyFormula;
+            bool nextFormula;
+            bool untilFormula;
+            bool boundedUntilFormula;
+            
+            bool atomicExpressionFormula;
+            bool atomicLabelFormula;
+            bool booleanLiteralFormula;
+            bool unaryBooleanStateFormula;
+            bool binaryBooleanStateFormula;
+            
+            bool cumulativeRewardFormula;
+            bool instantaneousRewardFormula;
+            bool reachabilityRewardFormula;
+            bool longRunAverageRewardFormula;
+            
+            bool conditionalProbabilityFormula;
+            bool conditionalRewardFormula;
+            
+            bool reachabilityExpectedTimeFormula;
+            
+            // Members that indicate certain restrictions.
+            bool nestedOperators;
+            
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_FRAGMENTSPECIFICATION_H_ */

src/logic/GloballyFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/GloballyFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         GloballyFormula::GloballyFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) {
@@ -10,10 +12,14 @@ namespace storm {
             return true;
         }
 
-        bool GloballyFormula::isValidProbabilityPathFormula() const {
+        bool GloballyFormula::isProbabilityPathFormula() const {
             return true;
         }
         
+        boost::any GloballyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+
         std::shared_ptr<Formula> GloballyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return std::make_shared<GloballyFormula>(this->getSubformula().substitute(substitution));
         }

src/logic/GloballyFormula.h

@@ -14,7 +14,9 @@ namespace storm {
             }
             
             virtual bool isGloballyFormula() const override;
-            virtual bool isValidProbabilityPathFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             

src/logic/InstantaneousRewardFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/InstantaneousRewardFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         InstantaneousRewardFormula::InstantaneousRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) {
@@ -14,12 +16,12 @@ namespace storm {
             return true;
         }
         
-        bool InstantaneousRewardFormula::isValidRewardPathFormula() const {
+        bool InstantaneousRewardFormula::isRewardPathFormula() const {
             return true;
         }
         
-        bool InstantaneousRewardFormula::isRewardPathFormula() const {
-            return true;
+        boost::any InstantaneousRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         bool InstantaneousRewardFormula::hasDiscreteTimeBound() const {

src/logic/InstantaneousRewardFormula.h

@@ -17,9 +17,11 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            virtual bool isRewardPathFormula() const override;
             virtual bool isInstantaneousRewardFormula() const override;
-            virtual bool isValidRewardPathFormula() const override;
+
+            virtual bool isRewardPathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             

src/logic/LongRunAverageOperatorFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/LongRunAverageOperatorFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::none, boost::none, subformula) {
@@ -22,20 +24,8 @@ namespace storm {
             return true;
         }
         
-        bool LongRunAverageOperatorFormula::isPctlStateFormula() const {
-            return this->getSubformula().isPctlStateFormula();
-        }
-        
-        bool LongRunAverageOperatorFormula::isPctlWithConditionalStateFormula() const {
-            return this->getSubformula().isPctlWithConditionalStateFormula();
-        }
-        
-        bool LongRunAverageOperatorFormula::containsProbabilityOperator() const {
-            return this->getSubformula().containsProbabilityOperator();
-        }
-        
-        bool LongRunAverageOperatorFormula::containsNestedProbabilityOperators() const {
-            return this->getSubformula().containsNestedProbabilityOperators();
+        boost::any LongRunAverageOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {

src/logic/LongRunAverageOperatorFormula.h

@@ -19,10 +19,7 @@ namespace storm {
             
             virtual bool isLongRunAverageOperatorFormula() const override;
             
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
 

src/logic/LongRunAverageRewardFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/LongRunAverageRewardFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         LongRunAverageRewardFormula::LongRunAverageRewardFormula() {
@@ -10,12 +12,12 @@ namespace storm {
             return true;
         }
         
-        bool LongRunAverageRewardFormula::isValidRewardPathFormula() const {
+        bool LongRunAverageRewardFormula::isRewardPathFormula() const {
             return true;
         }
         
-        bool LongRunAverageRewardFormula::isRewardPathFormula() const {
-            return true;
+        boost::any LongRunAverageRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         std::shared_ptr<Formula> LongRunAverageRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {

src/logic/LongRunAverageRewardFormula.h

@@ -13,9 +13,10 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            virtual bool isRewardPathFormula() const override;
             virtual bool isLongRunAverageRewardFormula() const override;
-            virtual bool isValidRewardPathFormula() const override;
+            virtual bool isRewardPathFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             

src/logic/NextFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/NextFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         NextFormula::NextFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) {
@@ -10,12 +12,12 @@ namespace storm {
             return true;
         }
         
-        bool NextFormula::isValidProbabilityPathFormula() const {
+        bool NextFormula::isProbabilityPathFormula() const {
             return true;
         }
         
-        bool NextFormula::containsNextFormula() const {
-            return true;
+        boost::any NextFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         std::shared_ptr<Formula> NextFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {

src/logic/NextFormula.h

@@ -14,9 +14,9 @@ namespace storm {
             }
             
             virtual bool isNextFormula() const override;
-            virtual bool isValidProbabilityPathFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
 
-            virtual bool containsNextFormula() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             

src/logic/ProbabilityOperatorFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/ProbabilityOperatorFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         ProbabilityOperatorFormula::ProbabilityOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ProbabilityOperatorFormula(boost::none, boost::none, subformula) {
@@ -22,28 +24,8 @@ namespace storm {
             return true;
         }
         
-        bool ProbabilityOperatorFormula::isPctlStateFormula() const {
-            return this->getSubformula().isPctlPathFormula();
-        }
-        
-        bool ProbabilityOperatorFormula::isPctlWithConditionalStateFormula() const {
-            return this->getSubformula().isPctlWithConditionalPathFormula();
-        }
-        
-        bool ProbabilityOperatorFormula::isCslStateFormula() const {
-            return this->getSubformula().isCslPathFormula();
-        }
-        
-        bool ProbabilityOperatorFormula::isPltlFormula() const {
-            return this->getSubformula().isLtlFormula();
-        }
-        
-        bool ProbabilityOperatorFormula::containsProbabilityOperator() const {
-            return true;
-        }
-        
-        bool ProbabilityOperatorFormula::containsNestedProbabilityOperators() const {
-            return this->getSubformula().containsProbabilityOperator();
+        boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
                 
         ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimizationDirection> optimalityType, boost::optional<Bound<double>> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, bound, subformula) {

src/logic/ProbabilityOperatorFormula.h

@@ -17,15 +17,10 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool isCslStateFormula() const override;
-            virtual bool isPltlFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
-            
             virtual bool isProbabilityOperatorFormula() const override;
 
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/RewardOperatorFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/RewardOperatorFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         RewardOperatorFormula::RewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::shared_ptr<Formula const> const& subformula) : RewardOperatorFormula(rewardModelName, boost::none, boost::none, subformula) {
@@ -22,20 +24,8 @@ namespace storm {
             return true;
         }
         
-        bool RewardOperatorFormula::isRewardStateFormula() const {
-            return this->getSubformula().isRewardPathFormula();
-        }
-        
-        bool RewardOperatorFormula::containsRewardOperator() const {
-            return true;
-        }
-        
-        bool RewardOperatorFormula::containsNestedRewardOperators() const {
-            return this->getSubformula().containsRewardOperator();
-        }
-        
-        bool RewardOperatorFormula::hasRewardModelName() const {
-            return static_cast<bool>(this->rewardModelName);
+        boost::any RewardOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         std::string const& RewardOperatorFormula::getRewardModelName() const {

src/logic/RewardOperatorFormula.h

@@ -19,10 +19,8 @@ namespace storm {
             }
             
             virtual bool isRewardOperatorFormula() const override;
-            virtual bool isRewardStateFormula() const override;
 
-            virtual bool containsRewardOperator() const override;
-            virtual bool containsNestedRewardOperators() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
             

src/logic/UnaryBooleanStateFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/UnaryBooleanStateFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         UnaryBooleanStateFormula::UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula) : UnaryStateFormula(subformula), operatorType(operatorType) {
@@ -10,6 +12,10 @@ namespace storm {
             return true;
         }
 
+        boost::any UnaryBooleanStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
         UnaryBooleanStateFormula::OperatorType UnaryBooleanStateFormula::getOperator() const {
             return operatorType;
         }

src/logic/UnaryBooleanStateFormula.h

@@ -17,6 +17,8 @@ namespace storm {
             
             virtual bool isUnaryBooleanStateFormula() const override;
 
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
             OperatorType getOperator() const;
             
             virtual bool isNot() const;

src/logic/UnaryPathFormula.cpp

@@ -10,42 +10,6 @@ namespace storm {
             return true;
         }
 
-        bool UnaryPathFormula::isPctlPathFormula() const {
-            return this->getSubformula().isPctlStateFormula();
-        }
-        
-        bool UnaryPathFormula::isPctlWithConditionalPathFormula() const {
-            return this->getSubformula().isPctlWithConditionalStateFormula();
-        }
-        
-        bool UnaryPathFormula::isLtlFormula() const {
-            return this->getSubformula().isLtlFormula();
-        }
-        
-        bool UnaryPathFormula::containsBoundedUntilFormula() const {
-            return this->getSubformula().containsBoundedUntilFormula();
-        }
-        
-        bool UnaryPathFormula::containsNextFormula() const {
-            return this->getSubformula().containsNextFormula();
-        }
-        
-        bool UnaryPathFormula::containsProbabilityOperator() const {
-            return this->getSubformula().containsProbabilityOperator();
-        }
-        
-        bool UnaryPathFormula::containsNestedProbabilityOperators() const {
-            return this->getSubformula().containsNestedProbabilityOperators();
-        }
-        
-        bool UnaryPathFormula::containsRewardOperator() const {
-            return this->getSubformula().containsRewardOperator();
-        }
-        
-        bool UnaryPathFormula::containsNestedRewardOperators() const {
-            return this->getSubformula().containsNestedRewardOperators();
-        }
-        
         Formula const& UnaryPathFormula::getSubformula() const {
             return *subformula;
         }

src/logic/UnaryPathFormula.h

@@ -17,16 +17,6 @@ namespace storm {
 
             virtual bool isUnaryPathFormula() const override;
             
-            virtual bool isPctlPathFormula() const override;
-            virtual bool isPctlWithConditionalPathFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool containsBoundedUntilFormula() const override;
-            virtual bool containsNextFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
-            virtual bool containsRewardOperator() const override;
-            virtual bool containsNestedRewardOperators() const override;
-            
             Formula const& getSubformula() const;
             
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;

src/logic/UnaryStateFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/UnaryStateFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         UnaryStateFormula::UnaryStateFormula(std::shared_ptr<Formula const> subformula) : subformula(subformula) {
@@ -10,44 +12,8 @@ namespace storm {
             return true;
         }
         
-        bool UnaryStateFormula::isPropositionalFormula() const {
-            return this->getSubformula().isPropositionalFormula();
-        }
-        
-        bool UnaryStateFormula::isPctlStateFormula() const {
-            return this->getSubformula().isPctlStateFormula();
-        }
-        
-        bool UnaryStateFormula::isPctlWithConditionalStateFormula() const {
-            return this->getSubformula().isPctlWithConditionalStateFormula();
-        }
-
-        bool UnaryStateFormula::isLtlFormula() const {
-            return this->getSubformula().isLtlFormula();
-        }
-        
-        bool UnaryStateFormula::containsBoundedUntilFormula() const {
-            return this->getSubformula().containsBoundedUntilFormula();
-        }
-        
-        bool UnaryStateFormula::containsNextFormula() const {
-            return this->getSubformula().containsNextFormula();
-        }
-        
-        bool UnaryStateFormula::containsProbabilityOperator() const {
-            return getSubformula().containsProbabilityOperator();
-        }
-        
-        bool UnaryStateFormula::containsNestedProbabilityOperators() const {
-            return getSubformula().containsNestedProbabilityOperators();
-        }
-        
-        bool UnaryStateFormula::containsRewardOperator() const {
-            return this->getSubformula().containsRewardOperator();
-        }
-        
-        bool UnaryStateFormula::containsNestedRewardOperators() const {
-            return this->getSubformula().containsNestedRewardOperators();
+        boost::any UnaryStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
         }
         
         Formula const& UnaryStateFormula::getSubformula() const {

src/logic/UnaryStateFormula.h

@@ -15,16 +15,7 @@ namespace storm {
             
             virtual bool isUnaryStateFormula() const override;
 
-            virtual bool isPropositionalFormula() const override;
-            virtual bool isPctlWithConditionalStateFormula() const override;
-            virtual bool isPctlStateFormula() const override;
-            virtual bool isLtlFormula() const override;
-            virtual bool containsBoundedUntilFormula() const override;
-            virtual bool containsNextFormula() const override;
-            virtual bool containsProbabilityOperator() const override;
-            virtual bool containsNestedProbabilityOperators() const override;
-            virtual bool containsRewardOperator() const override;
-            virtual bool containsNestedRewardOperators() const override;
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             Formula const& getSubformula() const;
             

src/logic/UntilFormula.cpp

@@ -1,5 +1,7 @@
 #include "src/logic/UntilFormula.h"
 
+#include "src/logic/FormulaVisitor.h"
+
 namespace storm {
     namespace logic {
         UntilFormula::UntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) {
@@ -10,10 +12,14 @@ namespace storm {
             return true;
         }
         
-        bool UntilFormula::isValidProbabilityPathFormula() const {
+        bool UntilFormula::isProbabilityPathFormula() const {
             return true;
         }
         
+        boost::any UntilFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
         std::shared_ptr<Formula> UntilFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return std::make_shared<UntilFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
         }

src/logic/UntilFormula.h

@@ -14,7 +14,9 @@ namespace storm {
             }
             
             virtual bool isUntilFormula() const override;
-            virtual bool isValidProbabilityPathFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             

src/modelchecker/AbstractModelChecker.cpp

@@ -17,11 +17,15 @@ namespace storm {
             if (formula.isStateFormula()) {
                 return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula()));
             } else if (formula.isPathFormula()) {
-                if (checkTask.computeProbabilities()) {
+                if (formula.isProbabilityPathFormula()) {
                     return this->computeProbabilities(checkTask.substituteFormula(formula.asPathFormula()));
-                } else if (checkTask.computeRewards()) {
+                } else if (formula.isRewardPathFormula()) {
                     return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula()));
                 }
+            } else if (formula.isConditionalProbabilityFormula()) {
+                return this->computeConditionalProbabilities(checkTask.substituteFormula(formula.asConditionalFormula()));
+            } else if (formula.isConditionalRewardFormula()) {
+                return this->computeConditionalRewards(checkTask.substituteFormula(formula.asConditionalFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }
@@ -30,8 +34,6 @@ namespace storm {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
             if (pathFormula.isBoundedUntilFormula()) {
                 return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(pathFormula.asBoundedUntilFormula()));
-            } else if (pathFormula.isConditionalPathFormula()) {
-                return this->computeConditionalProbabilities(checkTask.substituteFormula(pathFormula.asConditionalPathFormula()));
             } else if (pathFormula.isEventuallyFormula()) {
                 return this->computeEventuallyProbabilities(checkTask.substituteFormula(pathFormula.asEventuallyFormula()));
             } else if (pathFormula.isGloballyFormula()) {
@@ -48,7 +50,7 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
@@ -84,6 +86,10 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
         }
         
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
+        }
+        
         std::unique_ptr<CheckResult> AbstractModelChecker::computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
@@ -171,8 +177,6 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask) {
             storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
-            STORM_LOG_THROW(stateFormula.getSubformula().isValidProbabilityPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
-            
             std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula()));
             
             if (stateFormula.hasBound()) {
@@ -185,8 +189,6 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask) {
             storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
-            STORM_LOG_THROW(stateFormula.getSubformula().isValidRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
-            
             std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula()));
             
             if (checkTask.isBoundSet()) {

src/modelchecker/AbstractModelChecker.h

@@ -36,8 +36,8 @@ namespace storm {
                         
             // The methods to compute probabilities for path formulas.
             virtual std::unique_ptr<CheckResult> computeProbabilities(CheckTask<storm::logic::PathFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask);
@@ -45,6 +45,7 @@ namespace storm {
             
             // The methods to compute the rewards for path formulas.
             virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::PathFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeConditionalRewards(CheckTask<storm::logic::ConditionalFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask);

src/modelchecker/CheckTask.h

@@ -63,8 +63,6 @@ namespace storm {
                         }
                     }
                 } else if (formula.isRewardOperatorFormula()) {
-                    this->checkType = CheckType::Rewards;
-                    
                     storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
                     this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
                     
@@ -82,7 +80,7 @@ namespace storm {
              */
             template<typename NewFormulaType>
             CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
-                return CheckTask<NewFormulaType, ValueType>(newFormula, this->checkType, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers);
+                return CheckTask<NewFormulaType, ValueType>(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers);
             }
             
             /*!
@@ -92,27 +90,6 @@ namespace storm {
                 return formula.get();
             }
             
-            /*!
-             * Retrieves whether probabilities are to be computed.
-             */
-            bool computeProbabilities() const {
-                return checkType == CheckType::Probabilities;
-            }
-            
-            /*!
-             * Retrieves whether rewards are to be computed.
-             */
-            bool computeRewards() const {
-                return checkType == CheckType::Rewards;
-            }
-            
-            /*!
-             * Retrieves the type of this task.
-             */
-            CheckType getCheckType() const {
-                return checkType;
-            }
-            
             /*!
              * Retrieves whether an optimization direction was set.
              */
@@ -211,7 +188,6 @@ namespace storm {
              * Creates a task object with the given options.
              *
              * @param formula The formula to attach to the task.
-             * @param checkType The type of task: whether to compute probabilities or rewards.
              * @param optimizationDirection If set, the probabilities will be minimized/maximized.
              * @param rewardModelName If given, the checking has to be done wrt. to this reward model.
              * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values
@@ -222,16 +198,13 @@ namespace storm {
              * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve
              * a value will be produced if this flag is set.
              */
-            CheckTask(std::reference_wrapper<FormulaType const> const& formula, CheckType checkType, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound<ValueType>> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), checkType(checkType), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) {
+            CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound<ValueType>> const& bound, bool qualitative, bool produceSchedulers) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers) {
                 // Intentionally left empty.
             }
             
             // The formula that is to be checked.
             std::reference_wrapper<FormulaType const> formula;
             
-            // A type indicating whether probabilities or rewards are to be computed.
-            CheckType checkType;
-            
             // If set, the probabilities will be minimized/maximized.
             boost::optional<storm::OptimizationDirection> optimizationDirection;