introduced some methods to query formula type

Former-commit-id: 9ecc13566d
9 years ago · be8c65525e
38 changed files with 159 additions and 25 deletions
--- a/src/logic/AtomicExpressionFormula.cpp
+++ b/src/logic/AtomicExpressionFormula.cpp
@ -13,6 +13,10 @@ namespace storm {
        bool AtomicExpressionFormula::isPctlStateFormula() const {
            return true;
        }
+        
+        bool AtomicExpressionFormula::isPctlWithConditionalStateFormula() const {
+            return true;
+        }
                
        bool AtomicExpressionFormula::isLtlFormula() const {
            return true;
--- a/src/logic/AtomicExpressionFormula.h
+++ b/src/logic/AtomicExpressionFormula.h
@ -16,6 +16,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;
            
--- a/src/logic/AtomicLabelFormula.cpp
+++ b/src/logic/AtomicLabelFormula.cpp
@ -14,6 +14,10 @@ namespace storm {
            return true;
        }
    
+        bool AtomicLabelFormula::isPctlWithConditionalStateFormula() const {
+            return true;
+        }
+        
        bool AtomicLabelFormula::isLtlFormula() const {
            return true;
        }
--- a/src/logic/AtomicLabelFormula.h
+++ b/src/logic/AtomicLabelFormula.h
@ -18,6 +18,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;
            
--- a/src/logic/BinaryPathFormula.cpp
+++ b/src/logic/BinaryPathFormula.cpp
@ -14,6 +14,10 @@ namespace storm {
            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();
        }
--- a/src/logic/BinaryPathFormula.h
+++ b/src/logic/BinaryPathFormula.h
@ -18,6 +18,7 @@ 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;
--- a/src/logic/BinaryStateFormula.cpp
+++ b/src/logic/BinaryStateFormula.cpp
@ -13,6 +13,10 @@ namespace storm {
        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();
--- a/src/logic/BinaryStateFormula.h
+++ b/src/logic/BinaryStateFormula.h
@ -16,6 +16,7 @@ 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;
--- a/src/logic/BooleanLiteralFormula.cpp
+++ b/src/logic/BooleanLiteralFormula.cpp
@ -18,6 +18,10 @@ namespace storm {
            return true;
        }
        
+        bool BooleanLiteralFormula::isPctlWithConditionalStateFormula() const {
+            return true;
+        }
+        
        bool BooleanLiteralFormula::isLtlFormula() const {
            return true;
        }
--- a/src/logic/BooleanLiteralFormula.h
+++ b/src/logic/BooleanLiteralFormula.h
@ -18,6 +18,7 @@ namespace storm {
            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;
            
--- a/src/logic/BoundedUntilFormula.cpp
+++ b/src/logic/BoundedUntilFormula.cpp
@ -38,6 +38,10 @@ namespace storm {
            return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
        }
        
+        bool BoundedUntilFormula::isPctlWithConditionalPathFormula() const {
+            return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlWithConditionalStateFormula() && this->getRightSubformula().isPctlWithConditionalStateFormula();
+        }
+        
        bool BoundedUntilFormula::isCslPathFormula() const {
            return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula();
        }
--- a/src/logic/BoundedUntilFormula.h
+++ b/src/logic/BoundedUntilFormula.h
@ -23,6 +23,7 @@ namespace storm {
            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;

--- a/src/logic/ConditionalPathFormula.cpp
+++ b/src/logic/ConditionalPathFormula.cpp
@ -2,7 +2,7 @@

 namespace storm {
    namespace logic {
-        ConditionalPathFormula::ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula) {
+        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.
        }
        
@ -14,6 +14,18 @@ namespace storm {
            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));
        }
--- a/src/logic/ConditionalPathFormula.h
+++ b/src/logic/ConditionalPathFormula.h
@ -7,18 +7,24 @@ namespace storm {
    namespace logic {
        class ConditionalPathFormula : public BinaryPathFormula {
        public:
-            ConditionalPathFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula);
+            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;
        };
    }
 }
--- a/src/logic/CumulativeRewardFormula.cpp
+++ b/src/logic/CumulativeRewardFormula.cpp
@ -10,6 +10,10 @@ namespace storm {
            // Intentionally left empty.
        }
        
+        bool CumulativeRewardFormula::isRewardPathFormula() const {
+            return true;
+        }
+        
        bool CumulativeRewardFormula::isCumulativeRewardFormula() const {
            return true;
        }
--- a/src/logic/CumulativeRewardFormula.h
+++ b/src/logic/CumulativeRewardFormula.h
@ -17,6 +17,7 @@ namespace storm {
                // Intentionally left empty.
            }
            
+            virtual bool isRewardPathFormula() const override;
            virtual bool isCumulativeRewardFormula() const override;
            virtual bool isValidRewardPathFormula() const override;

--- a/src/logic/EventuallyFormula.cpp
+++ b/src/logic/EventuallyFormula.cpp
@ -2,7 +2,7 @@

 namespace storm {
    namespace logic {
-        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula) {
+        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, bool isRewardFormula) : UnaryPathFormula(subformula), isRewardFormula(isRewardFormula) {
            // Intentionally left empty.
        }
        
@ -10,12 +10,16 @@ namespace storm {
            return true;
        }
        
+        bool EventuallyFormula::isRewardPathFormula() const {
+            return isRewardFormula;
+        }
+        
        bool EventuallyFormula::isValidProbabilityPathFormula() const {
-            return true;
+            return !isRewardFormula;
        }
        
        bool EventuallyFormula::isValidRewardPathFormula() const {
-            return true;
+            return isRewardFormula;
        }
        
        std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
--- a/src/logic/EventuallyFormula.h
+++ b/src/logic/EventuallyFormula.h
@ -7,13 +7,14 @@ namespace storm {
    namespace logic {
        class EventuallyFormula : public UnaryPathFormula {
        public:
-            EventuallyFormula(std::shared_ptr<Formula const> const& subformula);
+            EventuallyFormula(std::shared_ptr<Formula const> const& subformula, bool isRewardFormula = false);
            
            virtual ~EventuallyFormula() {
                // Intentionally left empty.
            }
            
            virtual bool isEventuallyFormula() const override;
+            virtual bool isRewardPathFormula() const override;
            virtual bool isValidProbabilityPathFormula() const override;
            virtual bool isValidRewardPathFormula() const override;

@ -21,6 +22,8 @@ namespace storm {
            
            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;

+        private:
+            bool isRewardFormula;
        };
    }
 }
--- a/src/logic/ExpectedTimeOperatorFormula.cpp
+++ b/src/logic/ExpectedTimeOperatorFormula.cpp
@ -26,6 +26,10 @@ namespace storm {
            return this->getSubformula().isPctlStateFormula();
        }
        
+        bool ExpectedTimeOperatorFormula::isPctlWithConditionalStateFormula() const {
+            return this->getSubformula().isPctlWithConditionalStateFormula();
+        }
+        
        bool ExpectedTimeOperatorFormula::containsProbabilityOperator() const {
            return this->getSubformula().containsProbabilityOperator();
        }
--- a/src/logic/ExpectedTimeOperatorFormula.h
+++ b/src/logic/ExpectedTimeOperatorFormula.h
@ -20,6 +20,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;
            
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@ -111,6 +111,22 @@ namespace storm {
            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;
        }
@ -119,6 +135,14 @@ namespace storm {
            return false;
        }
        
+        bool Formula::isPctlWithConditionalPathFormula() const {
+            return false;
+        }
+        
+        bool Formula::isPctlWithConditionalStateFormula() const {
+            return false;
+        }
+        
        bool Formula::isCslPathFormula() const {
            return this->isPctlPathFormula();
        }
@ -127,6 +151,14 @@ namespace storm {
            return this->isPctlStateFormula();
        }
        
+        bool Formula::isRewardPathFormula() const {
+            return false;
+        }
+        
+        bool Formula::isRewardStateFormula() const {
+            return false;
+        }
+        
        bool Formula::isPltlFormula() const {
            return false;
        }
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@ -79,10 +79,18 @@ namespace storm {
            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;
--- a/src/logic/InstantaneousRewardFormula.cpp
+++ b/src/logic/InstantaneousRewardFormula.cpp
@ -18,6 +18,10 @@ namespace storm {
            return true;
        }
        
+        bool InstantaneousRewardFormula::isRewardPathFormula() const {
+            return true;
+        }
+        
        bool InstantaneousRewardFormula::hasDiscreteTimeBound() const {
            return timeBound.which() == 0;
        }
--- a/src/logic/InstantaneousRewardFormula.h
+++ b/src/logic/InstantaneousRewardFormula.h
@ -17,6 +17,7 @@ namespace storm {
                // Intentionally left empty.
            }
            
+            virtual bool isRewardPathFormula() const override;
            virtual bool isInstantaneousRewardFormula() const override;
            virtual bool isValidRewardPathFormula() const override;

--- a/src/logic/LongRunAverageOperatorFormula.cpp
+++ b/src/logic/LongRunAverageOperatorFormula.cpp
@ -26,6 +26,10 @@ namespace storm {
            return this->getSubformula().isPctlStateFormula();
        }
        
+        bool LongRunAverageOperatorFormula::isPctlWithConditionalStateFormula() const {
+            return this->getSubformula().isPctlWithConditionalStateFormula();
+        }
+        
        bool LongRunAverageOperatorFormula::containsProbabilityOperator() const {
            return this->getSubformula().containsProbabilityOperator();
        }
--- a/src/logic/LongRunAverageOperatorFormula.h
+++ b/src/logic/LongRunAverageOperatorFormula.h
@ -20,6 +20,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;
            
--- a/src/logic/LongRunAverageRewardFormula.cpp
+++ b/src/logic/LongRunAverageRewardFormula.cpp
@ -14,6 +14,10 @@ namespace storm {
            return true;
        }
        
+        bool LongRunAverageRewardFormula::isRewardPathFormula() const {
+            return true;
+        }
+        
        std::shared_ptr<Formula> LongRunAverageRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
            return std::shared_ptr<Formula>(new LongRunAverageRewardFormula());
        }
--- a/src/logic/LongRunAverageRewardFormula.h
+++ b/src/logic/LongRunAverageRewardFormula.h
@ -13,6 +13,7 @@ namespace storm {
                // Intentionally left empty.
            }
            
+            virtual bool isRewardPathFormula() const override;
            virtual bool isLongRunAverageRewardFormula() const override;
            virtual bool isValidRewardPathFormula() const override;

--- a/src/logic/ProbabilityOperatorFormula.cpp
+++ b/src/logic/ProbabilityOperatorFormula.cpp
@ -26,6 +26,10 @@ namespace storm {
            return this->getSubformula().isPctlPathFormula();
        }
        
+        bool ProbabilityOperatorFormula::isPctlWithConditionalStateFormula() const {
+            return this->getSubformula().isPctlWithConditionalPathFormula();
+        }
+        
        bool ProbabilityOperatorFormula::isCslStateFormula() const {
            return this->getSubformula().isCslPathFormula();
        }
--- a/src/logic/ProbabilityOperatorFormula.h
+++ b/src/logic/ProbabilityOperatorFormula.h
@ -18,6 +18,7 @@ namespace storm {
            }
            
            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;
--- a/src/logic/RewardOperatorFormula.cpp
+++ b/src/logic/RewardOperatorFormula.cpp
@ -22,9 +22,8 @@ namespace storm {
            return true;
        }
        
-        bool RewardOperatorFormula::isPctlStateFormula() const {
-            Formula const& subformula = this->getSubformula();
-            return subformula.isEventuallyFormula() || subformula.isCumulativeRewardFormula() || subformula.isInstantaneousRewardFormula();
+        bool RewardOperatorFormula::isRewardStateFormula() const {
+            return this->getSubformula().isRewardPathFormula();
        }
        
        bool RewardOperatorFormula::containsRewardOperator() const {
--- a/src/logic/RewardOperatorFormula.h
+++ b/src/logic/RewardOperatorFormula.h
@ -19,8 +19,8 @@ namespace storm {
            }
            
            virtual bool isRewardOperatorFormula() const override;
+            virtual bool isRewardStateFormula() const override;

-            virtual bool isPctlStateFormula() const override;
            virtual bool containsRewardOperator() const override;
            virtual bool containsNestedRewardOperators() const override;
            
--- a/src/logic/UnaryPathFormula.cpp
+++ b/src/logic/UnaryPathFormula.cpp
@ -14,6 +14,10 @@ namespace storm {
            return this->getSubformula().isPctlStateFormula();
        }
        
+        bool UnaryPathFormula::isPctlWithConditionalPathFormula() const {
+            return this->getSubformula().isPctlWithConditionalStateFormula();
+        }
+        
        bool UnaryPathFormula::isLtlFormula() const {
            return this->getSubformula().isLtlFormula();
        }
--- a/src/logic/UnaryPathFormula.h
+++ b/src/logic/UnaryPathFormula.h
@ -18,6 +18,7 @@ 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;
--- a/src/logic/UnaryStateFormula.cpp
+++ b/src/logic/UnaryStateFormula.cpp
@ -18,6 +18,10 @@ namespace storm {
            return this->getSubformula().isPctlStateFormula();
        }
        
+        bool UnaryStateFormula::isPctlWithConditionalStateFormula() const {
+            return this->getSubformula().isPctlWithConditionalStateFormula();
+        }
+
        bool UnaryStateFormula::isLtlFormula() const {
            return this->getSubformula().isLtlFormula();
        }
--- a/src/logic/UnaryStateFormula.h
+++ b/src/logic/UnaryStateFormula.h
@ -16,6 +16,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;
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
@ -25,7 +25,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.isCslStateFormula() || formula.isCslPathFormula();
+            return formula.isCslFormula() || formula.isRewardFormula();
        }
                
        template<storm::dd::DdType DdType, class ValueType>
--- a/src/parser/FormulaParser.cpp
+++ b/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>(), Skipper> conditionalFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> eventuallyFormula;
+            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>(), 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, 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, bool reward, 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) const;
+            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::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 | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula;
+            rewardPathFormula = eventuallyFormula(true) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula(true);
            rewardPathFormula.name("reward path formula");
            
            expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
@ -277,7 +277,7 @@ namespace storm {
            notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
            notStateFormula.name("negation formula");
            
-            eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
            eventuallyFormula.name("eventually formula");
            
            globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
@ -286,19 +286,19 @@ namespace storm {
            nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
            nextFormula.name("next formula");
            
-            pathFormulaWithoutUntil = eventuallyFormula | globallyFormula | nextFormula | stateFormula;
+            pathFormulaWithoutUntil = eventuallyFormula(false) | 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)];
            untilFormula.name("until formula");
            
-            conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)];
+            conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
            conditionalFormula.name("conditional formula");
            
            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;
+            pathFormula = conditionalFormula(false);
            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 > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            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.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, 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, bool reward, 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));
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula, reward));
            }
        }
        
@ -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) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula));
+        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::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 {