more refactoring regarding fragment checking

Former-commit-id: fd335f6f8e

src/logic/Formula.cpp

@@ -1,6 +1,9 @@
 #include "src/logic/Formulas.h"
 #include <sstream>
 
+#include "src/logic/FragmentChecker.h"
+#include "src/logic/FormulaInformationVisitor.h"
+
 namespace storm {
     namespace logic {
         bool Formula::isPathFormula() const {
@@ -111,6 +114,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isReachabilityRewardFormula() const {
+            return false;
+        }
+        
         bool Formula::isLongRunAverageRewardFormula() const {
             return false;
         }
@@ -131,6 +138,16 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isInFragment(FragmentSpecification const& fragment) const {
+            FragmentChecker checker;
+            return checker.conformsToSpecification(*this, fragment);
+        }
+        
+        FormulaInformation Formula::info() const {
+            FormulaInformationVisitor visitor;
+            return visitor.getInformation(*this);
+        }
+        
         std::shared_ptr<Formula const> Formula::getTrueFormula() {
             return std::shared_ptr<Formula const>(new BooleanLiteralFormula(true));
         }

src/logic/Formula.h

@@ -19,8 +19,11 @@ namespace storm {
         // Forward-declare visitor for accept() method.
         class FormulaVisitor;
 
-        // Also foward-declare base model checker class.
-        class ModelChecker;
+        // Forward-declare fragment specification for isInFragment() method.
+        class FragmentSpecification;
+        
+        // Forward-declare formula information class for info() method.
+        class FormulaInformation;
         
         class Formula : public std::enable_shared_from_this<Formula const> {
         public:
@@ -80,7 +83,10 @@ namespace storm {
             virtual bool isUnaryPathFormula() const;
             virtual bool isUnaryStateFormula() const;
 
-            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const = 0;
+            bool isInFragment(FragmentSpecification const& fragment) const;
+            FormulaInformation info() const;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0;
             
             static std::shared_ptr<Formula const> getTrueFormula();
             

src/logic/FormulaInformation.cpp

@@ -0,0 +1,46 @@
+#include "src/logic/FormulaInformation.h"
+
+namespace storm {
+    namespace logic {
+        FormulaInformation::FormulaInformation() {
+            this->mContainsRewardOperator = false;
+            this->mContainsNextFormula = false;
+            this->mContainsBoundedUntilFormula = false;
+        }
+        
+        bool FormulaInformation::containsRewardOperator() const {
+            return this->mContainsRewardOperator;
+        }
+        
+        bool FormulaInformation::containsNextFormula() const {
+            return this->mContainsNextFormula;
+        }
+        
+        bool FormulaInformation::containsBoundedUntilFormula() const {
+            return this-mContainsBoundedUntilFormula;
+        }
+        
+        FormulaInformation FormulaInformation::join(FormulaInformation const& other) {
+            FormulaInformation result;
+            result.mContainsRewardOperator = this->containsRewardOperator() || other.containsRewardOperator();
+            result.mContainsNextFormula = this->containsNextFormula() || other.containsNextFormula();
+            result.mContainsBoundedUntilFormula = this->containsBoundedUntilFormula() || other.containsBoundedUntilFormula();
+            return result;
+        }
+        
+        FormulaInformation& FormulaInformation::setContainsRewardOperator(bool newValue) {
+            this->mContainsRewardOperator = newValue;
+            return *this;
+        }
+        
+        FormulaInformation& FormulaInformation::setContainsNextFormula(bool newValue) {
+            this->mContainsNextFormula = newValue;
+            return *this;
+        }
+        
+        FormulaInformation& FormulaInformation::setContainsBoundedUntilFormula(bool newValue) {
+            this->mContainsBoundedUntilFormula = newValue;
+            return *this;
+        }
+    }
+}

src/logic/FormulaInformation.h

@@ -0,0 +1,29 @@
+#ifndef STORM_LOGIC_FORMULAINFORMATION_H_
+#define STORM_LOGIC_FORMULAINFORMATION_H_
+
+namespace storm {
+    namespace logic {
+        
+        class FormulaInformation {
+        public:
+            FormulaInformation();
+            bool containsRewardOperator() const;
+            bool containsNextFormula() const;
+            bool containsBoundedUntilFormula() const;
+            
+            FormulaInformation join(FormulaInformation const& other);
+            
+            FormulaInformation& setContainsRewardOperator(bool newValue = true);
+            FormulaInformation& setContainsNextFormula(bool newValue = true);
+            FormulaInformation& setContainsBoundedUntilFormula(bool newValue = true);
+            
+        private:
+            bool mContainsRewardOperator;
+            bool mContainsNextFormula;
+            bool mContainsBoundedUntilFormula;
+        };
+        
+    }
+}
+
+#endif /* STORM_LOGIC_FORMULAINFORMATION_H_ */

src/logic/FormulaInformationVisitor.cpp

@@ -0,0 +1,85 @@
+#include "src/logic/FormulaInformationVisitor.h"
+
+#include "src/logic/Formulas.h"
+
+namespace storm {
+    namespace logic {
+        FormulaInformation FormulaInformationVisitor::getInformation(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<FormulaInformation>(result);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this))).setContainsBoundedUntilFormula();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).join(boost::any_cast<FormulaInformation>(f.getConditionFormula().accept(*this)));
+        }
+        
+        boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(ExpectedTimeOperatorFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsNextFormula();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsRewardOperator();
+        }
+        
+        boost::any FormulaInformationVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this);
+        }
+        
+        boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+        }
+
+    }
+}

src/logic/FormulaInformationVisitor.h

@@ -0,0 +1,38 @@
+#ifndef STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_
+#define STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_
+
+#include "src/logic/FormulaVisitor.h"
+#include "src/logic/FormulaInformation.h"
+
+namespace storm {
+    namespace logic {
+        
+        class FormulaInformationVisitor : public FormulaVisitor {
+        public:
+            FormulaInformation getInformation(Formula const& f) 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_FORMULAINFORMATIONVISITOR_H_ */

src/logic/FragmentChecker.cpp

@@ -4,49 +4,75 @@
 
 namespace storm {
     namespace logic {
+        class InheritedInformation {
+        public:
+            InheritedInformation(FragmentSpecification const& fragmentSpecification) : fragmentSpecification(fragmentSpecification) {
+                // Intentionally left empty.
+            }
+            
+            FragmentSpecification const& getSpecification() const {
+                return fragmentSpecification;
+            }
+
+        private:
+            FragmentSpecification const& fragmentSpecification;
+        };
+        
         bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const {
-            boost::any result = f.accept(*this, specification);
+            boost::any result = f.accept(*this, InheritedInformation(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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().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));
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areBinaryBooleanStateFormulasAllowed();
+            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(BooleanLiteralFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areBooleanLiteralFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areBoundedUntilFormulasAllowed();
+            if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                result = result && !f.getLeftSubformula().isPathFormula();
+                result = result && !f.getRightSubformula().isPathFormula();
+            }
+            if (f.hasDiscreteTimeBound()) {
+                result = result && inherited.getSpecification().areStepBoundedUntilFormulasAllowed();
+            } else {
+                result = result && inherited.getSpecification().areTimeBoundedUntilFormulasAllowed();
+            }
             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);
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = true;
             if (f.isConditionalProbabilityFormula()) {
-                result &= specification.areConditionalProbabilityFormulasAllowed();
+                result = result && inherited.getSpecification().areConditionalProbabilityFormulasAllowed();
             } else if (f.Formula::isConditionalRewardFormula()) {
-                result &= specification.areConditionalRewardFormulasFormulasAllowed();
+                result = result && inherited.getSpecification().areConditionalRewardFormulasFormulasAllowed();
+            }
+            if (inherited.getSpecification().areOnlyEventuallyFormuluasInConditionalFormulasAllowed()) {
+                result = result && f.getSubformula().isEventuallyFormula() && f.getConditionFormula().isEventuallyFormula();
             }
             result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
             result = result && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data));
@@ -54,65 +80,124 @@ namespace storm {
         }
         
         boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areCumulativeRewardFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = true;
+            if (f.isEventuallyFormula()) {
+                result = inherited.getSpecification().areEventuallyFormulasAllowed();
+                if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                    result = result && !f.getSubformula().isPathFormula();
+                }
+            } else if (f.isReachabilityRewardFormula()) {
+                result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
+                result = result && f.getSubformula().isStateFormula();
+            } else if (f.isReachbilityExpectedTimeFormula()) {
+                result = result && inherited.getSpecification().areReachbilityExpectedTimeFormulasAllowed();
+                result = result && f.getSubformula().isStateFormula();
+            }
             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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areExpectedTimeOperatorsAllowed();
+            result = result && f.getSubformula().isExpectedTimePathFormula();
+            if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
+            } else {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            }
+            return result;
         }
         
         boost::any FragmentChecker::visit(GloballyFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areGloballyFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areGloballyFormulasAllowed();
+            if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                result = result && !f.getSubformula().isPathFormula();
+            }
+            result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
         }
         
         boost::any FragmentChecker::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areInstantaneousRewardFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areLongRunAverageOperatorsAllowed();
+            result = result && f.getSubformula().isStateFormula();
+            if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
+            } else {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            }
+            return result;
         }
         
         boost::any FragmentChecker::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areLongRunAverageRewardFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().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();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areNextFormulasAllowed();
+            if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                result = result && !f.getSubformula().isPathFormula();
+            }
+            result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
         }
         
         boost::any FragmentChecker::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areProbabilityOperatorsAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areProbabilityOperatorsAllowed();
+            result = result && f.getSubformula().isProbabilityPathFormula();
+            if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
+            } else {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            }
+            return result;
         }
         
         boost::any FragmentChecker::visit(RewardOperatorFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areRewardOperatorsAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areRewardOperatorsAllowed();
+            result = result && f.getSubformula().isRewardPathFormula();
+            if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, inherited.getSpecification().copy().setOperatorsAllowed(false)));
+            } else {
+                result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            }
+            return result;
         }
         
         boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areUnaryBooleanStateFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
         }
         
         boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const {
-            FragmentSpecification const& specification = boost::any_cast<FragmentSpecification const&>(data);
-            return specification.areUntilFormulasAllowed();
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areUntilFormulasAllowed();
+            if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
+                result = result && !f.getLeftSubformula().isPathFormula();
+                result = result && !f.getRightSubformula().isPathFormula();
+            }
+            result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data));
+            result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
+            return result;
         }
     }
 }

src/logic/FragmentSpecification.cpp

@@ -3,6 +3,99 @@
 namespace storm {
     namespace logic {
         
+        FragmentSpecification propositional() {
+            FragmentSpecification propositional;
+            
+            propositional.setBooleanLiteralFormulasAllowed(true);
+            propositional.setBinaryBooleanStateFormulasAllowed(true);
+            propositional.setUnaryBooleanStateFormulasAllowed(true);
+            propositional.setAtomicExpressionFormulasAllowed(true);
+            propositional.setAtomicLabelFormulasAllowed(true);
+            
+            return propositional;
+        }
+        
+        FragmentSpecification pctl() {
+            FragmentSpecification pctl = propositional();
+            
+            pctl.setProbabilityOperatorsAllowed(true);
+            pctl.setGloballyFormulasAllowed(true);
+            pctl.setEventuallyFormulasAllowed(true);
+            pctl.setNextFormulasAllowed(true);
+            pctl.setUntilFormulasAllowed(true);
+            pctl.setBoundedUntilFormulasAllowed(true);
+            pctl.setStepBoundedUntilFormulasAllowed(true);
+            
+            return pctl;
+        }
+        
+        FragmentSpecification prctl() {
+            FragmentSpecification prctl = pctl();
+            
+            prctl.setRewardOperatorsAllowed(true);
+            prctl.setCumulativeRewardFormulasAllowed(true);
+            prctl.setInstantaneousFormulasAllowed(true);
+            prctl.setReachabilityRewardFormulasAllowed(true);
+            prctl.setLongRunAverageOperatorsAllowed(true);
+            
+            return prctl;
+        }
+        
+        FragmentSpecification csl() {
+            FragmentSpecification csl = pctl();
+            
+            csl.setTimeBoundedUntilFormulasAllowed(true);
+            
+            return csl;
+        }
+        
+        FragmentSpecification csrl() {
+            FragmentSpecification csrl;
+            
+            csrl.setRewardOperatorsAllowed(true);
+            csrl.setCumulativeRewardFormulasAllowed(true);
+            csrl.setInstantaneousFormulasAllowed(true);
+            csrl.setReachabilityRewardFormulasAllowed(true);
+            csrl.setLongRunAverageOperatorsAllowed(true);
+            
+            return csrl;
+        }
+        
+        FragmentSpecification::FragmentSpecification() {
+            probabilityOperator = false;
+            rewardOperator = false;
+            expectedTimeOperator = false;
+            longRunAverageOperator = false;
+            
+            globallyFormula = false;
+            eventuallyFormula = false;
+            nextFormula = false;
+            untilFormula = false;
+            boundedUntilFormula = false;
+            
+            atomicExpressionFormula = false;
+            atomicLabelFormula = false;
+            booleanLiteralFormula = false;
+            unaryBooleanStateFormula = false;
+            binaryBooleanStateFormula = false;
+            
+            cumulativeRewardFormula = false;
+            instantaneousRewardFormula = false;
+            reachabilityRewardFormula = false;
+            longRunAverageRewardFormula = false;
+            
+            conditionalProbabilityFormula = false;
+            conditionalRewardFormula = false;
+            
+            reachabilityExpectedTimeFormula = false;
+            
+            nestedOperators = true;
+            nestedPathFormulas = false;
+            onlyEventuallyFormuluasInConditionalFormulas = true;
+            stepBoundedUntilFormulas = false;
+            timeBoundedUntilFormulas = false;
+        }
+        
         FragmentSpecification FragmentSpecification::copy() const {
             return FragmentSpecification(*this);
         }
@@ -205,5 +298,60 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::areNestedPathFormulasAllowed() const {
+            return this->nestedPathFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setNestedPathFormulasAllowed(bool newValue) {
+            this->nestedPathFormulas = newValue;
+            return *this;
+        }
+
+        bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const {
+            return this->onlyEventuallyFormuluasInConditionalFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue) {
+            this->onlyEventuallyFormuluasInConditionalFormulas = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areStepBoundedUntilFormulasAllowed() const {
+            return this->stepBoundedUntilFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setStepBoundedUntilFormulasAllowed(bool newValue) {
+            this->stepBoundedUntilFormulas = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areTimeBoundedUntilFormulasAllowed() const {
+            return this->timeBoundedUntilFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setTimeBoundedUntilFormulasAllowed(bool newValue) {
+            this->timeBoundedUntilFormulas = newValue;
+            return *this;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) {
+            this->setProbabilityOperatorsAllowed(newValue);
+            this->setRewardOperatorsAllowed(newValue);
+            this->setLongRunAverageOperatorsAllowed(newValue);
+            this->setExpectedTimeOperatorsAllowed(newValue);
+            return *this;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setExpectedTimeAllowed(bool newValue) {
+            this->setExpectedTimeOperatorsAllowed(newValue);
+            this->setReachbilityExpectedTimeFormulasAllowed(newValue);
+            return *this;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setLongRunAverageProbabilitiesAllowed(bool newValue) {
+            this->setLongRunAverageOperatorsAllowed(newValue);
+            return *this;
+        }
+        
     }
 }

src/logic/FragmentSpecification.h

@@ -5,6 +5,12 @@ namespace storm {
     namespace logic {
         class FragmentSpecification {
         public:
+            FragmentSpecification();
+            FragmentSpecification(FragmentSpecification const& other) = default;
+            FragmentSpecification(FragmentSpecification&& other) = default;
+            FragmentSpecification& operator=(FragmentSpecification const& other) = default;
+            FragmentSpecification& operator=(FragmentSpecification&& other) = default;
+            
             FragmentSpecification copy() const;
             
             bool areProbabilityOperatorsAllowed() const;
@@ -73,6 +79,22 @@ namespace storm {
             bool areNestedOperatorsAllowed() const;
             FragmentSpecification& setNestedOperatorsAllowed(bool newValue);
 
+            bool areNestedPathFormulasAllowed() const;
+            FragmentSpecification& setNestedPathFormulasAllowed(bool newValue);
+            
+            bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const;
+            FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue);
+
+            bool areStepBoundedUntilFormulasAllowed() const;
+            FragmentSpecification& setStepBoundedUntilFormulasAllowed(bool newValue);
+            
+            bool areTimeBoundedUntilFormulasAllowed() const;
+            FragmentSpecification& setTimeBoundedUntilFormulasAllowed(bool newValue);
+            
+            FragmentSpecification& setOperatorsAllowed(bool newValue);
+            FragmentSpecification& setExpectedTimeAllowed(bool newValue);
+            FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
+            
         private:
             // Flags that indicate whether it is legal to see such a formula.
             bool probabilityOperator;
@@ -104,8 +126,27 @@ namespace storm {
             
             // Members that indicate certain restrictions.
             bool nestedOperators;
-            
+            bool nestedPathFormulas;
+            bool onlyEventuallyFormuluasInConditionalFormulas;
+            bool stepBoundedUntilFormulas;
+            bool timeBoundedUntilFormulas;
         };
+        
+        // Propositional.
+        FragmentSpecification propositional();
+        
+        // Regular PCTL.
+        FragmentSpecification pctl();
+        
+        // PCTL + cumulative, instantaneous, reachability and long-run rewards.
+        FragmentSpecification prctl();
+        
+        // Regular CSL.
+        FragmentSpecification csl();
+        
+        // CSL + cumulative, instantaneous, reachability and long-run rewards.
+        FragmentSpecification csrl();
+
     }
 }
 

src/logic/RewardOperatorFormula.cpp

@@ -32,6 +32,10 @@ namespace storm {
             return this->rewardModelName.get();
         }
         
+        bool RewardOperatorFormula::hasRewardModelName() const {
+            return static_cast<bool>(rewardModelName);
+        }
+        
         boost::optional<std::string> const& RewardOperatorFormula::getOptionalRewardModelName() const {
             return this->rewardModelName;
         }

src/logic/UnaryStateFormula.cpp

@@ -12,10 +12,6 @@ namespace storm {
             return true;
         }
         
-        boost::any UnaryStateFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
-            return visitor.visit(*this, data);
-        }
-        
         Formula const& UnaryStateFormula::getSubformula() const {
             return *subformula;
         }

src/logic/UnaryStateFormula.h

@@ -15,8 +15,6 @@ namespace storm {
             
             virtual bool isUnaryStateFormula() const override;
             
-            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-            
             Formula const& getSubformula() const;
             
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;

src/modelchecker/csl/HybridCtmcCslModelChecker.cpp

@@ -10,6 +10,8 @@
 #include "src/storage/dd/Add.h"
 #include "src/storage/dd/Bdd.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 namespace storm {
     namespace modelchecker {
         template<storm::dd::DdType DdType, class ValueType>
@@ -25,7 +27,7 @@ namespace storm {
         template<storm::dd::DdType DdType, class ValueType>
         bool HybridCtmcCslModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isCslFormula() || formula.isRewardFormula();
+            return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true));
         }
                 
         template<storm::dd::DdType DdType, class ValueType>

src/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -13,6 +13,8 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/exceptions/NotImplementedException.h"
@@ -32,7 +34,7 @@ namespace storm {
         template <typename SparseCtmcModelType>
         bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isCslStateFormula() || formula.isCslPathFormula();
+            return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true));
         }
         
         template <typename SparseCtmcModelType>

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -12,6 +12,8 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/exceptions/NotImplementedException.h"
 
@@ -30,7 +32,9 @@ namespace storm {
         template<typename SparseMarkovAutomatonModelType>
         bool SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isCslStateFormula() || formula.isCslPathFormula();
+            storm::logic::FragmentSpecification fragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setReachabilityRewardFormulasAllowed(true);
+            fragment.setExpectedTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true);
+            return formula.isInFragment(fragment);
         }
         
         template<typename SparseMarkovAutomatonModelType>

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -17,6 +17,8 @@
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
 #include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/exceptions/InvalidArgumentException.h"
@@ -36,7 +38,7 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         bool HybridDtmcPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isPctlStateFormula() || formula.isPctlPathFormula();
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true));
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>

src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@@ -8,6 +8,8 @@
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/solver/MinMaxLinearEquationSolver.h"
 
 #include "src/settings/modules/GeneralSettings.h"
@@ -30,16 +32,7 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         bool HybridMdpPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
-                return true;
-            }
-            if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
-            }
-            if (formula.isGloballyFormula()) {
-                return true;
-            }
-            return false;
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -11,6 +11,8 @@
 #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
 #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/models/sparse/StandardRewardModel.h"
 
 #include "src/settings/modules/GeneralSettings.h"
@@ -34,22 +36,7 @@ namespace storm {
         template<typename SparseDtmcModelType>
         bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
-                return true;
-            }
-            if (formula.isGloballyFormula()) {
-                return true;
-            }
-            if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
-            }
-            if (formula.isConditionalPathFormula()) {
-                storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula();
-                if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
-                    return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula());
-                }
-            }
-            return false;
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
         }
         
         template<typename SparseDtmcModelType>
@@ -129,13 +116,13 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) {
-            storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula();
-            STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
-            STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+            storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
+            STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
+            STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
 
-            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula());
-            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -24,7 +24,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -8,6 +8,8 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/models/sparse/StandardRewardModel.h"
 
 #include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
@@ -39,22 +41,7 @@ namespace storm {
         template<typename SparseMdpModelType>
         bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
-                return true;
-            }
-            if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
-            }
-            if (formula.isGloballyFormula()) {
-                return true;
-            }
-            if (formula.isConditionalPathFormula()) {
-                storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula();
-                if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
-                    return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula());
-                }
-            }
-            return false;
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
         }
         
         template<typename SparseMdpModelType>
@@ -106,15 +93,15 @@ namespace storm {
         }
         
         template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) {
-            storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+            storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state.");
-            STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
-            STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
+            STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
+            STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
 
-            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula());
-            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula());
             ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
 

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -22,7 +22,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;

src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -10,6 +10,9 @@
 
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/solver/SymbolicLinearEquationSolver.h"
 
 #include "src/settings/modules/GeneralSettings.h"
@@ -32,16 +35,7 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         bool SymbolicDtmcPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
-                return true;
-            }
-            if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
-            }
-            if (formula.isGloballyFormula()) {
-                return true;
-            }
-            return false;
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
         }
         
         template<storm::dd::DdType DdType, typename ValueType>

src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp

@@ -5,6 +5,8 @@
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/models/symbolic/StandardRewardModel.h"
 
 #include "src/utility/macros.h"
@@ -32,16 +34,7 @@ namespace storm {
         template<storm::dd::DdType DdType, typename ValueType>
         bool SymbolicMdpPrctlModelChecker<DdType, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
-                return true;
-            }
-            if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
-            }
-            if (formula.isGloballyFormula()) {
-                return true;
-            }
-            return false;
+            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false));
         }
         
         template<storm::dd::DdType DdType, typename ValueType>

src/modelchecker/propositional/SparsePropositionalModelChecker.cpp

@@ -10,6 +10,8 @@
 
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidPropertyException.h"
 
@@ -23,7 +25,7 @@ namespace storm {
         template<typename SparseModelType>
         bool SparsePropositionalModelChecker<SparseModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isPropositionalFormula();
+            return formula.isInFragment(storm::logic::propositional());
         }
         
         template<typename SparseModelType>

src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp

@@ -10,6 +10,8 @@
 
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidPropertyException.h"
 
@@ -23,7 +25,7 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         bool SymbolicPropositionalModelChecker<Type, ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isPropositionalFormula();
+            return formula.isInFragment(storm::logic::propositional());
         }
         
         template<storm::dd::DdType Type, typename ValueType>

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -16,6 +16,8 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/utility/graph.h"
 #include "src/utility/vector.h"
 #include "src/utility/macros.h"
@@ -82,45 +84,9 @@ namespace storm {
         template<typename SparseDtmcModelType>
         bool SparseDtmcEliminationModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
-            } else if (formula.isRewardOperatorFormula()) {
-                return this->canHandle(checkTask.substituteFormula(formula.asRewardOperatorFormula().getSubformula()));
-            } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
-                if (formula.isUntilFormula()) {
-                    storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
-                    if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) {
-                        return true;
-                    }
-                } else if (formula.isEventuallyFormula()) {
-                    storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula();
-                    if (eventuallyFormula.getSubformula().isPropositionalFormula()) {
-                        return true;
-                    }
-                }
-            } else if (formula.isBoundedUntilFormula()) {
-                storm::logic::BoundedUntilFormula const& boundedUntilFormula = formula.asBoundedUntilFormula();
-                if (boundedUntilFormula.getLeftSubformula().isPropositionalFormula() && boundedUntilFormula.getRightSubformula().isPropositionalFormula()) {
-                    return true;
-                }
-            } else if (formula.isConditionalPathFormula()) {
-                storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula();
-                if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
-                    return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula());
-                }
-            } else if (formula.isLongRunAverageOperatorFormula()) {
-                storm::logic::LongRunAverageOperatorFormula const& longRunAverageOperatorFormula = formula.asLongRunAverageOperatorFormula();
-                if (longRunAverageOperatorFormula.getSubformula().isPropositionalFormula()) {
-                    return true;
-                }
-            } else if (formula.isLongRunAverageRewardFormula()) {
-                return true;
-            }
-            
-            else if (formula.isPropositionalFormula()) {
-                return true;
-            }
-            return false;
+            storm::logic::FragmentSpecification fragment = storm::logic::prctl().setCumulativeRewardFormulasAllowed(false).setInstantaneousFormulasAllowed(false);
+            fragment.setNestedOperatorsAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true);
+            return formula.isInFragment(fragment);
         }
         
         template<typename SparseDtmcModelType>
@@ -646,15 +612,15 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) {
-            storm::logic::ConditionalPathFormula const& pathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) {
+            storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();
             
             // Retrieve the appropriate bitvectors by model checking the subformulas.
-            STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
-            STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
+            STORM_LOG_THROW(conditionalFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
+            STORM_LOG_THROW(conditionalFormula.getConditionFormula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
             
-            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula());
-            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(conditionalFormula.getSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(conditionalFormula.getConditionFormula().asEventuallyFormula().getSubformula());
             storm::storage::BitVector phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
             storm::storage::BitVector psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
             storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
@@ -680,7 +646,7 @@ namespace storm {
             if (this->getModel().getInitialStates().isSubsetOf(statesWithProbability1)) {
                 STORM_LOG_INFO("The condition holds with probability 1, so the regular reachability probability is computed.");
                 std::shared_ptr<storm::logic::BooleanLiteralFormula> trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-                std::shared_ptr<storm::logic::UntilFormula> untilFormula = std::make_shared<storm::logic::UntilFormula>(trueFormula, pathFormula.getLeftSubformula().asSharedPointer());
+                std::shared_ptr<storm::logic::UntilFormula> untilFormula = std::make_shared<storm::logic::UntilFormula>(trueFormula, conditionalFormula.getSubformula().asSharedPointer());
                 return this->computeUntilProbabilities(*untilFormula);
             }
             

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -28,7 +28,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
         private:

src/parser/FormulaParser.cpp

@@ -120,8 +120,8 @@ namespace storm {
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expressionFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
             
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(bool), Skipper> conditionalFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(bool), Skipper> eventuallyFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::ConditionalFormula::Context), Skipper> conditionalFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(storm::logic::EventuallyFormula::Context), Skipper> eventuallyFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> nextFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> globallyFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> untilFormula;
@@ -142,11 +142,11 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
             std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;
             std::shared_ptr<storm::logic::Formula> createAtomicLabelFormula(std::string const& label) const;
-            std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, bool reward, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
-            std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, bool reward) const;
+            std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::ConditionalFormula::Context context) const;
             std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const;
             std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
@@ -253,7 +253,7 @@ namespace storm {
             cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
             cumulativeRewardFormula.name("cumulative reward formula");
             
-            rewardPathFormula = eventuallyFormula(true) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(true);
+            rewardPathFormula = eventuallyFormula(storm::logic::EventuallyFormula::Context::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(storm::logic::ConditionalFormula::Context::Reward);
             rewardPathFormula.name("reward path formula");
             
             expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
@@ -286,7 +286,7 @@ namespace storm {
             nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
             nextFormula.name("next formula");
             
-            pathFormulaWithoutUntil = eventuallyFormula(false) | globallyFormula | nextFormula | stateFormula;
+            pathFormulaWithoutUntil = eventuallyFormula(storm::logic::EventuallyFormula::Context::Probability) | globallyFormula | nextFormula | stateFormula;
             pathFormulaWithoutUntil.name("path formula");
             
             untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
@@ -298,7 +298,7 @@ namespace storm {
             timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") >  qi::uint_)[qi::_val = qi::_1];
             timeBound.name("time bound");
             
-            pathFormula = conditionalFormula(false);
+            pathFormula = conditionalFormula(storm::logic::ConditionalFormula::Context::Probability);
             pathFormula.name("path formula");
             
             operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
@@ -313,7 +313,7 @@ namespace storm {
             rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
             rewardOperator.name("reward operator");
             
-            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(true) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::EventuallyFormula::Context::ExpectedTime) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             expectedTimeOperator.name("expected time operator");
             
             probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
@@ -422,7 +422,7 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, bool reward, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, storm::logic::EventuallyFormula::Context context, std::shared_ptr<storm::logic::Formula> const& subformula) const {
             if (timeBound) {
                 if (timeBound.get().which() == 0) {
                     std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
@@ -431,7 +431,7 @@ namespace storm {
                     return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
                 }
             } else {
-                return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula, reward));
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula, context));
             }
         }
         
@@ -456,8 +456,8 @@ namespace storm {
             }
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, bool reward) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula, reward));
+        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::ConditionalFormula::Context context) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
         }
         
         std::pair<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::Bound<double>>> FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {

src/storage/bisimulation/BisimulationDecomposition.cpp

@@ -15,6 +15,9 @@
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GeneralSettings.h"
 
+#include "src/logic/FormulaInformation.h"
+#include "src/logic/FragmentSpecification.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/IllegalFunctionCallException.h"
 #include "src/exceptions/InvalidOptionException.h"
@@ -55,11 +58,14 @@ namespace storm {
             phiStates = boost::none;
             psiStates = boost::none;
             
+            // Retrieve information about formula.
+            storm::logic::FormulaInformation info = formula.info();
+            
             // Preserve rewards if necessary.
-            keepRewards = keepRewards || formula.containsRewardOperator();
+            keepRewards = keepRewards || info.containsRewardOperator();
             
             // Preserve bounded properties if necessary.
-            bounded = bounded || (formula.containsBoundedUntilFormula() || formula.containsNextFormula());
+            bounded = bounded || (info.containsBoundedUntilFormula() || info.containsNextFormula());
             
             // Compute the relevant labels and expressions.
             this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
@@ -67,10 +73,13 @@ namespace storm {
         
         template<typename ModelType, typename BlockDataType>
         void BisimulationDecomposition<ModelType, BlockDataType>::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) {
-            keepRewards = formula.containsRewardOperator();
+            // Retrieve information about formula.
+            storm::logic::FormulaInformation info = formula.info();
+
+            keepRewards = info.containsRewardOperator();
             
             // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
-            bounded = formula.containsBoundedUntilFormula() || formula.containsNextFormula();
+            bounded = info.containsBoundedUntilFormula() || info.containsNextFormula();
             
             // Compute the relevant labels and expressions.
             this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
@@ -114,12 +123,12 @@ namespace storm {
             if (newFormula->isUntilFormula()) {
                 leftSubformula = newFormula->asUntilFormula().getLeftSubformula().asSharedPointer();
                 rightSubformula = newFormula->asUntilFormula().getRightSubformula().asSharedPointer();
-                if (leftSubformula->isPropositionalFormula() && rightSubformula->isPropositionalFormula()) {
+                if (leftSubformula->isInFragment(storm::logic::propositional()) && rightSubformula->isInFragment(storm::logic::propositional())) {
                     measureDrivenInitialPartition = true;
                 }
             } else if (newFormula->isEventuallyFormula()) {
                 rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer();
-                if (rightSubformula->isPropositionalFormula()) {
+                if (rightSubformula->isInFragment(storm::logic::propositional())) {
                     measureDrivenInitialPartition = true;
                 }
             }

test/functional/logic/FragmentCheckerTest.cpp

@@ -0,0 +1,14 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/FormulaParser.h"
+#include "src/logic/FragmentSpecification.h"
+#include "src/exceptions/WrongFormatException.h"
+
+TEST(FragmentCheckerTest, PctlTest) {
+    storm::parser::FormulaParser formulaParser;
+    
+    std::string input = "\"label\"";
+    std::shared_ptr<const storm::logic::Formula> formula(nullptr);
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
+    
+}

test/functional/parser/FormulaParserTest.cpp

@@ -1,6 +1,7 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 #include "src/parser/FormulaParser.h"
+#include "src/logic/FragmentSpecification.h"
 #include "src/exceptions/WrongFormatException.h"
 
 TEST(FormulaParserTest, LabelTest) {
@@ -20,7 +21,7 @@ TEST(FormulaParserTest, ComplexLabelTest) {
     std::shared_ptr<const storm::logic::Formula> formula(nullptr);
 	ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
 
-    EXPECT_TRUE(formula->isPropositionalFormula());
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
     EXPECT_TRUE(formula->isBinaryBooleanStateFormula());
 }
 
@@ -35,7 +36,7 @@ TEST(FormulaParserTest, ExpressionTest) {
     std::shared_ptr<const storm::logic::Formula> formula(nullptr);
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
     
-    EXPECT_TRUE(formula->isPropositionalFormula());
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
     EXPECT_TRUE(formula->isUnaryBooleanStateFormula());
 }
 
@@ -50,11 +51,11 @@ TEST(FormulaParserTest, LabelAndExpressionTest) {
     std::shared_ptr<const storm::logic::Formula> formula(nullptr);
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
     
-    EXPECT_TRUE(formula->isPropositionalFormula());
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
     
     input = "x | y > 3 | !\"a\"";
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
-    EXPECT_TRUE(formula->isPropositionalFormula());
+    EXPECT_TRUE(formula->isInFragment(storm::logic::propositional()));
 }
 
 TEST(FormulaParserTest, ProbabilityOperatorTest) {
@@ -98,7 +99,7 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) {
     
     EXPECT_TRUE(formula->isProbabilityOperatorFormula());
     storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asProbabilityOperatorFormula();
-    EXPECT_TRUE(probFormula.getSubformula().isConditionalPathFormula());
+    EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula());
 }
 
 TEST(FormulaParserTest, NestedPathFormulaTest) {