removed reward path formulas. reward path formulas are now just path formulas. this allows some invalid formulas to be constructed, so this now has to be checked dynamically

Former-commit-id: c8527c8e9a

src/logic/BoundedUntilFormula.cpp

@@ -30,6 +30,10 @@ namespace storm {
             return bounds.which() == 0;
         }
         
+        bool BoundedUntilFormula::isValidProbabilityPathFormula() const {
+            return true;
+        }
+        
         bool BoundedUntilFormula::isPctlPathFormula() const {
             return this->hasDiscreteTimeBound() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
         }

src/logic/BoundedUntilFormula.h

@@ -22,6 +22,7 @@ namespace storm {
             std::pair<double, double> const& getIntervalBounds() const;
             uint_fast64_t getDiscreteTimeBound() const;
             
+            virtual bool isValidProbabilityPathFormula() const override;
             virtual bool isPctlPathFormula() const override;
             virtual bool isCslPathFormula() const override;
 

src/logic/ConditionalPathFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool ConditionalPathFormula::isValidProbabilityPathFormula() const {
+            return true;
+        }
+        
         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));
         }

src/logic/ConditionalPathFormula.h

@@ -14,7 +14,8 @@ namespace storm {
             }
             
             virtual bool isConditionalPathFormula() const override;
-            
+            virtual bool isValidProbabilityPathFormula() const override;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;

src/logic/CumulativeRewardFormula.cpp

@@ -14,6 +14,10 @@ namespace storm {
             return true;
         }
         
+        bool CumulativeRewardFormula::isValidRewardPathFormula() const {
+            return true;
+        }
+        
         bool CumulativeRewardFormula::hasDiscreteTimeBound() const {
             return timeBound.which() == 0;
         }

src/logic/CumulativeRewardFormula.h

@@ -3,11 +3,11 @@
 
 #include <boost/variant.hpp>
 
-#include "src/logic/RewardPathFormula.h"
+#include "src/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {
-        class CumulativeRewardFormula : public RewardPathFormula {
+        class CumulativeRewardFormula : public PathFormula {
         public:
             CumulativeRewardFormula(uint_fast64_t timeBound);
             
@@ -18,7 +18,8 @@ namespace storm {
             }
             
             virtual bool isCumulativeRewardFormula() const override;
-            
+            virtual bool isValidRewardPathFormula() const override;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             bool hasDiscreteTimeBound() const;

src/logic/EventuallyFormula.cpp

@@ -10,6 +10,14 @@ namespace storm {
             return true;
         }
         
+        bool EventuallyFormula::isValidProbabilityPathFormula() const {
+            return true;
+        }
+        
+        bool EventuallyFormula::isValidRewardPathFormula() const {
+            return true;
+        }
+        
         std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return std::make_shared<EventuallyFormula>(this->getSubformula().substitute(substitution));
         }

src/logic/EventuallyFormula.h

@@ -14,7 +14,9 @@ namespace storm {
             }
             
             virtual bool isEventuallyFormula() 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;

src/logic/Formula.cpp

@@ -87,10 +87,6 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isRewardPathFormula() const {
-            return false;
-        }
-        
         bool Formula::isCumulativeRewardFormula() const {
             return false;
         }
@@ -99,10 +95,6 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isReachabilityRewardFormula() const {
-            return false;
-        }
-        
         bool Formula::isLongRunAverageRewardFormula() const {
             return false;
         }
@@ -147,6 +139,14 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isValidProbabilityPathFormula() const {
+            return false;
+        }
+        
+        bool Formula::isValidRewardPathFormula() const {
+            return false;
+        }
+        
         bool Formula::containsBoundedUntilFormula() const {
             return false;
         }
@@ -327,14 +327,6 @@ namespace storm {
             return dynamic_cast<ExpectedTimeOperatorFormula const&>(*this);
         }
         
-        RewardPathFormula& Formula::asRewardPathFormula() {
-            return dynamic_cast<RewardPathFormula&>(*this);
-        }
-        
-        RewardPathFormula const& Formula::asRewardPathFormula() const {
-            return dynamic_cast<RewardPathFormula const&>(*this);
-        }
-        
         CumulativeRewardFormula& Formula::asCumulativeRewardFormula() {
             return dynamic_cast<CumulativeRewardFormula&>(*this);
         }
@@ -350,15 +342,7 @@ namespace storm {
         InstantaneousRewardFormula const& Formula::asInstantaneousRewardFormula() const {
             return dynamic_cast<InstantaneousRewardFormula const&>(*this);
         }
-        
-        ReachabilityRewardFormula& Formula::asReachabilityRewardFormula() {
-            return dynamic_cast<ReachabilityRewardFormula&>(*this);
-        }
-        
-        ReachabilityRewardFormula const& Formula::asReachabilityRewardFormula() const {
-            return dynamic_cast<ReachabilityRewardFormula const&>(*this);
-        }
-        
+                
         LongRunAverageRewardFormula& Formula::asLongRunAverageRewardFormula() {
             return dynamic_cast<LongRunAverageRewardFormula&>(*this);
         }

src/logic/Formula.h

@@ -31,10 +31,8 @@ namespace storm {
         class NextFormula;
         class LongRunAverageOperatorFormula;
         class ExpectedTimeOperatorFormula;
-        class RewardPathFormula;
         class CumulativeRewardFormula;
         class InstantaneousRewardFormula;
-        class ReachabilityRewardFormula;
         class LongRunAverageRewardFormula;
         class ProbabilityOperatorFormula;
         class RewardOperatorFormula;
@@ -74,10 +72,8 @@ namespace storm {
             virtual bool isNextFormula() const;
             virtual bool isLongRunAverageOperatorFormula() const;
             virtual bool isExpectedTimeOperatorFormula() const;
-            virtual bool isRewardPathFormula() const;
             virtual bool isCumulativeRewardFormula() const;
             virtual bool isInstantaneousRewardFormula() const;
-            virtual bool isReachabilityRewardFormula() const;
             virtual bool isLongRunAverageRewardFormula() const;
             virtual bool isProbabilityOperatorFormula() const;
             virtual bool isRewardOperatorFormula() const;
@@ -90,6 +86,8 @@ namespace storm {
             virtual bool isPltlFormula() const;
             virtual bool isLtlFormula() const;
             virtual bool isPropositionalFormula() const;
+            virtual bool isValidProbabilityPathFormula() const;
+            virtual bool isValidRewardPathFormula() const;
             virtual bool containsBoundedUntilFormula() const;
             virtual bool containsNextFormula() const;
             virtual bool containsProbabilityOperator() const;
@@ -156,18 +154,12 @@ namespace storm {
             ExpectedTimeOperatorFormula& asExpectedTimeOperatorFormula();
             ExpectedTimeOperatorFormula const& asExpectedTimeOperatorFormula() const;
             
-            RewardPathFormula& asRewardPathFormula();
-            RewardPathFormula const& asRewardPathFormula() const;
-            
             CumulativeRewardFormula& asCumulativeRewardFormula();
             CumulativeRewardFormula const& asCumulativeRewardFormula() const;
             
             InstantaneousRewardFormula& asInstantaneousRewardFormula();
             InstantaneousRewardFormula const& asInstantaneousRewardFormula() const;
             
-            ReachabilityRewardFormula& asReachabilityRewardFormula();
-            ReachabilityRewardFormula const& asReachabilityRewardFormula() const;
-
             LongRunAverageRewardFormula& asLongRunAverageRewardFormula();
             LongRunAverageRewardFormula const& asLongRunAverageRewardFormula() const;
             

src/logic/Formulas.h

@@ -12,10 +12,8 @@
 #include "src/logic/InstantaneousRewardFormula.h"
 #include "src/logic/NextFormula.h"
 #include "src/logic/PathFormula.h"
-#include "src/logic/RewardPathFormula.h"
 #include "src/logic/OperatorFormula.h"
 #include "src/logic/ProbabilityOperatorFormula.h"
-#include "src/logic/ReachabilityRewardFormula.h"
 #include "src/logic/LongRunAverageRewardFormula.h"
 #include "src/logic/RewardOperatorFormula.h"
 #include "src/logic/StateFormula.h"

src/logic/GloballyFormula.cpp

@@ -9,7 +9,11 @@ namespace storm {
         bool GloballyFormula::isGloballyFormula() const {
             return true;
         }
-        
+
+        bool GloballyFormula::isValidProbabilityPathFormula() const {
+            return true;
+        }
+
         std::shared_ptr<Formula> GloballyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return std::make_shared<GloballyFormula>(this->getSubformula().substitute(substitution));
         }

src/logic/GloballyFormula.h

@@ -14,7 +14,8 @@ namespace storm {
             }
             
             virtual bool isGloballyFormula() const override;
-            
+            virtual bool isValidProbabilityPathFormula() const override;
+
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/InstantaneousRewardFormula.cpp

@@ -14,6 +14,10 @@ namespace storm {
             return true;
         }
         
+        bool InstantaneousRewardFormula::isValidRewardPathFormula() const {
+            return true;
+        }
+        
         bool InstantaneousRewardFormula::hasDiscreteTimeBound() const {
             return timeBound.which() == 0;
         }

src/logic/InstantaneousRewardFormula.h

@@ -3,11 +3,11 @@
 
 #include <boost/variant.hpp>
 
-#include "src/logic/RewardPathFormula.h"
+#include "src/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {
-        class InstantaneousRewardFormula : public RewardPathFormula {
+        class InstantaneousRewardFormula : public PathFormula {
         public:
             InstantaneousRewardFormula(uint_fast64_t timeBound);
             
@@ -18,7 +18,8 @@ namespace storm {
             }
             
             virtual bool isInstantaneousRewardFormula() const override;
-            
+            virtual bool isValidRewardPathFormula() const override;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             bool hasDiscreteTimeBound() const;

src/logic/LongRunAverageRewardFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool LongRunAverageRewardFormula::isValidRewardPathFormula() 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());
         }

src/logic/LongRunAverageRewardFormula.h

@@ -1,14 +1,11 @@
 #ifndef STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_
 #define STORM_LOGIC_LONGRUNAVERAGEREWARDFORMULA_H_
 
-#include <memory>
-
-#include "src/logic/RewardPathFormula.h"
-
+#include "src/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {
-        class LongRunAverageRewardFormula : public RewardPathFormula {
+        class LongRunAverageRewardFormula : public PathFormula {
         public:
             LongRunAverageRewardFormula();
             
@@ -17,7 +14,8 @@ namespace storm {
             }
             
             virtual bool isLongRunAverageRewardFormula() const override;
-            
+            virtual bool isValidRewardPathFormula() const override;
+
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/NextFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool NextFormula::isValidProbabilityPathFormula() const {
+            return true;
+        }
+        
         bool NextFormula::containsNextFormula() const {
             return true;
         }

src/logic/NextFormula.h

@@ -14,7 +14,8 @@ namespace storm {
             }
             
             virtual bool isNextFormula() const override;
-            
+            virtual bool isValidProbabilityPathFormula() const override;
+
             virtual bool containsNextFormula() const override;
             
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;

src/logic/ReachabilityRewardFormula.cpp

@@ -1,35 +0,0 @@
-#include "src/logic/ReachabilityRewardFormula.h"
-
-namespace storm {
-    namespace logic {
-        ReachabilityRewardFormula::ReachabilityRewardFormula(std::shared_ptr<Formula const> const& subformula) : subformula(subformula) {
-            // Intentionally left empty.
-        }
-        
-        bool ReachabilityRewardFormula::isReachabilityRewardFormula() const {
-            return true;
-        }
-        
-        Formula const& ReachabilityRewardFormula::getSubformula() const {
-            return *subformula;
-        }
-        
-        void ReachabilityRewardFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
-            this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
-        }
-        
-        void ReachabilityRewardFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
-            this->getSubformula().gatherAtomicLabelFormulas(atomicLabelFormulas);
-        }
-        
-        std::shared_ptr<Formula> ReachabilityRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ReachabilityRewardFormula>(this->getSubformula().substitute(substitution));
-        }
-        
-        std::ostream& ReachabilityRewardFormula::writeToStream(std::ostream& out) const {
-            out << "F ";
-            this->getSubformula().writeToStream(out);
-            return out;
-        }
-    }
-}

src/logic/ReachabilityRewardFormula.h

@@ -1,36 +0,0 @@
-#ifndef STORM_LOGIC_REACHABILITYREWARDFORMULA_H_
-#define STORM_LOGIC_REACHABILITYREWARDFORMULA_H_
-
-#include <memory>
-
-#include "src/logic/RewardPathFormula.h"
-
-
-namespace storm {
-    namespace logic {
-        class ReachabilityRewardFormula : public RewardPathFormula {
-        public:
-            ReachabilityRewardFormula(std::shared_ptr<Formula const> const& subformula);
-            
-            virtual ~ReachabilityRewardFormula() {
-                // Intentionally left empty.
-            }
-            
-            virtual bool isReachabilityRewardFormula() const override;
-            
-            Formula const& getSubformula() const;
-            
-            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
-            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
-            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
-        private:
-            std::shared_ptr<Formula const> subformula;
-        };
-    }
-}
-
-#endif /* STORM_LOGIC_REACHABILITYREWARDFORMULA_H_ */

src/logic/RewardOperatorFormula.cpp

@@ -23,7 +23,8 @@ namespace storm {
         }
         
         bool RewardOperatorFormula::isPctlStateFormula() const {
-            return this->getSubformula().isRewardPathFormula();
+            Formula const& subformula = this->getSubformula();
+            return subformula.isEventuallyFormula() || subformula.isCumulativeRewardFormula() || subformula.isInstantaneousRewardFormula();
         }
         
         bool RewardOperatorFormula::containsRewardOperator() const {

src/logic/RewardPathFormula.cpp

@@ -1,9 +0,0 @@
-#include "src/logic/RewardPathFormula.h"
-
-namespace storm {
-    namespace logic {
-        bool RewardPathFormula::isRewardPathFormula() const {
-            return true;
-        }
-    }
-}

src/logic/RewardPathFormula.h

@@ -1,19 +0,0 @@
-#ifndef STORM_LOGIC_PATHREWARDFORMULA_H_
-#define STORM_LOGIC_PATHREWARDFORMULA_H_
-
-#include "src/logic/PathFormula.h"
-
-namespace storm {
-    namespace logic {
-        class RewardPathFormula : public Formula {
-        public:
-            virtual ~RewardPathFormula() {
-                // Intentionally left empty.
-            }
-            
-            virtual bool isRewardPathFormula() const override;
-        };
-    }
-}
-
-#endif /* STORM_LOGIC_PATHREWARDFORMULA_H_ */

src/logic/UntilFormula.cpp

@@ -10,6 +10,10 @@ namespace storm {
             return true;
         }
         
+        bool UntilFormula::isValidProbabilityPathFormula() const {
+            return true;
+        }
+        
         std::shared_ptr<Formula> UntilFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return std::make_shared<UntilFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
         }

src/logic/UntilFormula.h

@@ -14,7 +14,8 @@ namespace storm {
             }
             
             virtual bool isUntilFormula() const override;
-            
+            virtual bool isValidProbabilityPathFormula() const override;
+
             virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/modelchecker/AbstractModelChecker.cpp

@@ -15,11 +15,13 @@ namespace storm {
             storm::logic::Formula const& formula = checkTask.getFormula();
             STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
             if (formula.isStateFormula()) {
-                return this->checkStateFormula(checkTask.replaceFormula(formula.asStateFormula()));
+                return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula()));
             } else if (formula.isPathFormula()) {
-                return this->computeProbabilities(checkTask.replaceFormula(formula.asPathFormula()));
-            } else if (formula.isRewardPathFormula()) {
-                return this->computeRewards(checkTask.replaceFormula(formula.asRewardPathFormula()));
+                if (checkTask.computeProbabilities()) {
+                    return this->computeProbabilities(checkTask.substituteFormula(formula.asPathFormula()));
+                } else if (checkTask.computeRewards()) {
+                    return this->computeRewards(checkTask.substituteFormula(formula.asPathFormula()));
+                }
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }
@@ -27,17 +29,17 @@ namespace storm {
         std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(CheckTask<storm::logic::PathFormula> const& checkTask) {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
             if (pathFormula.isBoundedUntilFormula()) {
-                return this->computeBoundedUntilProbabilities(checkTask.replaceFormula(pathFormula.asBoundedUntilFormula()));
+                return this->computeBoundedUntilProbabilities(checkTask.substituteFormula(pathFormula.asBoundedUntilFormula()));
             } else if (pathFormula.isConditionalPathFormula()) {
-                return this->computeConditionalProbabilities(checkTask.replaceFormula(pathFormula.asConditionalPathFormula()));
+                return this->computeConditionalProbabilities(checkTask.substituteFormula(pathFormula.asConditionalPathFormula()));
             } else if (pathFormula.isEventuallyFormula()) {
-                return this->computeEventuallyProbabilities(checkTask.replaceFormula(pathFormula.asEventuallyFormula()));
+                return this->computeEventuallyProbabilities(checkTask.substituteFormula(pathFormula.asEventuallyFormula()));
             } else if (pathFormula.isGloballyFormula()) {
-                return this->computeGloballyProbabilities(checkTask.replaceFormula(pathFormula.asGloballyFormula()));
+                return this->computeGloballyProbabilities(checkTask.substituteFormula(pathFormula.asGloballyFormula()));
             } else if (pathFormula.isUntilFormula()) {
-                return this->computeUntilProbabilities(checkTask.replaceFormula(pathFormula.asUntilFormula()));
+                return this->computeUntilProbabilities(checkTask.substituteFormula(pathFormula.asUntilFormula()));
             } else if (pathFormula.isNextFormula()) {
-                return this->computeNextProbabilities(checkTask.replaceFormula(pathFormula.asNextFormula()));
+                return this->computeNextProbabilities(checkTask.substituteFormula(pathFormula.asNextFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << pathFormula << "' is invalid.");
         }
@@ -53,7 +55,7 @@ namespace storm {
         std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
             storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
-            return this->computeUntilProbabilities(checkTask.replaceFormula(newFormula));
+            return this->computeUntilProbabilities(checkTask.substituteFormula(newFormula));
         }
         
         std::unique_ptr<CheckResult> AbstractModelChecker::computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> const& checkTask) {
@@ -68,16 +70,16 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::RewardPathFormula> const& checkTask) {
-            storm::logic::RewardPathFormula const& rewardPathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(CheckTask<storm::logic::PathFormula> const& checkTask) {
+            storm::logic::PathFormula const& rewardPathFormula = checkTask.getFormula();
             if (rewardPathFormula.isCumulativeRewardFormula()) {
-                return this->computeCumulativeRewards(checkTask.replaceFormula(rewardPathFormula.asCumulativeRewardFormula()));
+                return this->computeCumulativeRewards(checkTask.substituteFormula(rewardPathFormula.asCumulativeRewardFormula()));
             } else if (rewardPathFormula.isInstantaneousRewardFormula()) {
-                return this->computeInstantaneousRewards(checkTask.replaceFormula(rewardPathFormula.asInstantaneousRewardFormula()));
-            } else if (rewardPathFormula.isReachabilityRewardFormula()) {
-                return this->computeReachabilityRewards(checkTask.replaceFormula(rewardPathFormula.asReachabilityRewardFormula()));
+                return this->computeInstantaneousRewards(checkTask.substituteFormula(rewardPathFormula.asInstantaneousRewardFormula()));
+            } else if (rewardPathFormula.isEventuallyFormula()) {
+                return this->computeReachabilityRewards(checkTask.substituteFormula(rewardPathFormula.asEventuallyFormula()));
             } else if (rewardPathFormula.isLongRunAverageRewardFormula()) {
-                return this->computeLongRunAverageRewards(checkTask.replaceFormula(rewardPathFormula.asLongRunAverageRewardFormula()));
+                return this->computeLongRunAverageRewards(checkTask.substituteFormula(rewardPathFormula.asLongRunAverageRewardFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << rewardPathFormula << "' is invalid.");
         }
@@ -90,7 +92,7 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
         }
         
@@ -109,25 +111,25 @@ namespace storm {
         std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(CheckTask<storm::logic::StateFormula> const& checkTask) {
             storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
             if (stateFormula.isBinaryBooleanStateFormula()) {
-                return this->checkBinaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asBinaryBooleanStateFormula()));
+                return this->checkBinaryBooleanStateFormula(checkTask.substituteFormula(stateFormula.asBinaryBooleanStateFormula()));
             } else if (stateFormula.isUnaryBooleanStateFormula()) {
-                return this->checkUnaryBooleanStateFormula(checkTask.replaceFormula(stateFormula.asUnaryBooleanStateFormula()));
+                return this->checkUnaryBooleanStateFormula(checkTask.substituteFormula(stateFormula.asUnaryBooleanStateFormula()));
             } else if (stateFormula.isBooleanLiteralFormula()) {
-                return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula()));
+                return this->checkBooleanLiteralFormula(checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
             } else if (stateFormula.isProbabilityOperatorFormula()) {
-                return this->checkProbabilityOperatorFormula(checkTask.replaceFormula(stateFormula.asProbabilityOperatorFormula()));
+                return this->checkProbabilityOperatorFormula(checkTask.substituteFormula(stateFormula.asProbabilityOperatorFormula()));
             } else if (stateFormula.isRewardOperatorFormula()) {
-                return this->checkRewardOperatorFormula(checkTask.replaceFormula(stateFormula.asRewardOperatorFormula()));
+                return this->checkRewardOperatorFormula(checkTask.substituteFormula(stateFormula.asRewardOperatorFormula()));
             } else if (stateFormula.isExpectedTimeOperatorFormula()) {
-                return this->checkExpectedTimeOperatorFormula(checkTask.replaceFormula(stateFormula.asExpectedTimeOperatorFormula()));
+                return this->checkExpectedTimeOperatorFormula(checkTask.substituteFormula(stateFormula.asExpectedTimeOperatorFormula()));
             } else if (stateFormula.isLongRunAverageOperatorFormula()) {
-                return this->checkLongRunAverageOperatorFormula(checkTask.replaceFormula(stateFormula.asLongRunAverageOperatorFormula()));
+                return this->checkLongRunAverageOperatorFormula(checkTask.substituteFormula(stateFormula.asLongRunAverageOperatorFormula()));
             } else if (stateFormula.isAtomicExpressionFormula()) {
-                return this->checkAtomicExpressionFormula(checkTask.replaceFormula(stateFormula.asAtomicExpressionFormula()));
+                return this->checkAtomicExpressionFormula(checkTask.substituteFormula(stateFormula.asAtomicExpressionFormula()));
             } else if (stateFormula.isAtomicLabelFormula()) {
-                return this->checkAtomicLabelFormula(checkTask.replaceFormula(stateFormula.asAtomicLabelFormula()));
+                return this->checkAtomicLabelFormula(checkTask.substituteFormula(stateFormula.asAtomicLabelFormula()));
             } else if (stateFormula.isBooleanLiteralFormula()) {
-                return this->checkBooleanLiteralFormula(checkTask.replaceFormula(stateFormula.asBooleanLiteralFormula()));
+                return this->checkBooleanLiteralFormula(checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
         }
@@ -136,7 +138,7 @@ namespace storm {
             storm::logic::AtomicExpressionFormula const& stateFormula = checkTask.getFormula();
             std::stringstream stream;
             stream << stateFormula.getExpression();
-            return this->checkAtomicLabelFormula(checkTask.replaceFormula(storm::logic::AtomicLabelFormula(stream.str())));
+            return this->checkAtomicLabelFormula(checkTask.substituteFormula(storm::logic::AtomicLabelFormula(stream.str())));
         }
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkAtomicLabelFormula(CheckTask<storm::logic::AtomicLabelFormula> const& checkTask) {
@@ -147,8 +149,8 @@ namespace storm {
             storm::logic::BinaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
             STORM_LOG_THROW(stateFormula.getLeftSubformula().isStateFormula() && stateFormula.getRightSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            std::unique_ptr<CheckResult> leftResult = this->check(checkTask.replaceFormula<storm::logic::Formula>(stateFormula.getLeftSubformula().asStateFormula()));
-            std::unique_ptr<CheckResult> rightResult = this->check(checkTask.replaceFormula<storm::logic::Formula>(stateFormula.getRightSubformula().asStateFormula()));
+            std::unique_ptr<CheckResult> leftResult = this->check(checkTask.substituteFormula<storm::logic::Formula>(stateFormula.getLeftSubformula().asStateFormula()));
+            std::unique_ptr<CheckResult> rightResult = this->check(checkTask.substituteFormula<storm::logic::Formula>(stateFormula.getRightSubformula().asStateFormula()));
             
             STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results.");
             
@@ -169,9 +171,9 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkProbabilityOperatorFormula(CheckTask<storm::logic::ProbabilityOperatorFormula> const& checkTask) {
             storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
-            STORM_LOG_THROW(stateFormula.getSubformula().isPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+            STORM_LOG_THROW(stateFormula.getSubformula().isValidProbabilityPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asPathFormula()));
+            std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula()));
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@@ -183,9 +185,9 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(CheckTask<storm::logic::RewardOperatorFormula> const& checkTask) {
             storm::logic::RewardOperatorFormula const& stateFormula = checkTask.getFormula();
-            STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+            STORM_LOG_THROW(stateFormula.getSubformula().isValidRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.replaceFormula(stateFormula.getSubformula().asRewardPathFormula()));
+            std::unique_ptr<CheckResult> result = this->computeRewards(checkTask.substituteFormula(stateFormula.getSubformula().asPathFormula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@@ -199,7 +201,7 @@ namespace storm {
             storm::logic::ExpectedTimeOperatorFormula const& stateFormula = checkTask.getFormula();
 			STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            std::unique_ptr<CheckResult> result = this->computeExpectedTimes(checkTask.replaceFormula(stateFormula.getSubformula().asEventuallyFormula()));
+            std::unique_ptr<CheckResult> result = this->computeExpectedTimes(checkTask.substituteFormula(stateFormula.getSubformula().asEventuallyFormula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@@ -213,7 +215,7 @@ namespace storm {
             storm::logic::LongRunAverageOperatorFormula const& stateFormula = checkTask.getFormula();
 			STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            std::unique_ptr<CheckResult> result = this->computeLongRunAverageProbabilities(checkTask.replaceFormula(stateFormula.getSubformula().asStateFormula()));
+            std::unique_ptr<CheckResult> result = this->computeLongRunAverageProbabilities(checkTask.substituteFormula(stateFormula.getSubformula().asStateFormula()));
             
             if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
@@ -225,7 +227,7 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(CheckTask<storm::logic::UnaryBooleanStateFormula> const& checkTask) {
             storm::logic::UnaryBooleanStateFormula const& stateFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> subResult = this->check(checkTask.replaceFormula<storm::logic::Formula>(stateFormula.getSubformula()));
+            std::unique_ptr<CheckResult> subResult = this->check(checkTask.substituteFormula<storm::logic::Formula>(stateFormula.getSubformula()));
             STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result.");
             if (stateFormula.isNot()) {
                 subResult->asQualitativeCheckResult().complement();

src/modelchecker/AbstractModelChecker.h

@@ -44,10 +44,10 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask);
             
             // The methods to compute the rewards for path formulas.
-            virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::RewardPathFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeRewards(CheckTask<storm::logic::PathFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask);
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(CheckTask<storm::logic::LongRunAverageRewardFormula> const& checkTask);
             
             // The methods to compute the long-run average and expected time.

src/modelchecker/CheckTask.h

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

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() || formula.isRewardPathFormula();
+            return formula.isCslStateFormula() || formula.isCslPathFormula();
         }
                 
         template<storm::dd::DdType DdType, class ValueType>
@@ -54,9 +54,9 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, class ValueType>
-        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+        std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
 
             return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);

src/modelchecker/csl/HybridCtmcCslModelChecker.h

@@ -23,7 +23,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(CheckTask<storm::logic::InstantaneousRewardFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(CheckTask<storm::logic::CumulativeRewardFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
         protected:

src/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -32,7 +32,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() || formula.isRewardPathFormula();
+            return formula.isCslStateFormula() || formula.isCslPathFormula();
         }
         
         template <typename SparseCtmcModelType>
@@ -91,9 +91,9 @@ namespace storm {
         }
                 
         template <typename SparseCtmcModelType>
-        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper<ValueType>::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);

src/modelchecker/csl/SparseCtmcCslModelChecker.h

@@ -26,7 +26,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
         private:

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -30,7 +30,7 @@ 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() || (formula.isRewardPathFormula() && formula.isReachabilityRewardFormula());
+            return formula.isCslStateFormula() || formula.isCslPathFormula();
         }
         
         template<typename SparseMarkovAutomatonModelType>
@@ -59,11 +59,11 @@ namespace storm {
         }
                 
         template<typename SparseMarkovAutomatonModelType>
-        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton.");
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
 
             std::vector<ValueType> result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper<ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);

src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@@ -23,7 +23,7 @@ namespace storm {
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeExpectedTimes(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp

@@ -36,7 +36,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() || formula.isRewardPathFormula();
+            return formula.isPctlStateFormula() || formula.isPctlPathFormula();
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>
@@ -91,9 +91,9 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+        std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
         }

src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h

@@ -24,7 +24,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
 
         protected:

src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@@ -30,11 +30,11 @@ 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() || formula.isRewardPathFormula()) {
+            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
                 return true;
             }
             if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
             }
             if (formula.isGloballyFormula()) {
                 return true;
@@ -100,10 +100,10 @@ namespace storm {
         }
                 
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             return storm::modelchecker::helper::HybridMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
         }

src/modelchecker/prctl/HybridMdpPrctlModelChecker.h

@@ -31,7 +31,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         protected:
             storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override;

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -34,14 +34,14 @@ 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() || formula.isRewardPathFormula()) {
+            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
                 return true;
             }
             if (formula.isGloballyFormula()) {
                 return true;
             }
             if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
             }
             if (formula.isConditionalPathFormula()) {
                 storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula();
@@ -111,9 +111,9 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -27,7 +27,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
             
         private:

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -39,11 +39,11 @@ 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() || formula.isRewardPathFormula()) {
+            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
                 return true;
             }
             if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
             }
             if (formula.isGloballyFormula()) {
                 return true;
@@ -140,10 +140,10 @@ namespace storm {
         }
                 
         template<typename SparseMdpModelType>
-        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = 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.");
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory);
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -25,7 +25,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(CheckTask<storm::logic::ConditionalPathFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;
             
         private:

src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -32,11 +32,11 @@ 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() || formula.isRewardPathFormula()) {
+            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
                 return true;
             }
             if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
             }
             if (formula.isGloballyFormula()) {
                 return true;
@@ -102,9 +102,9 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+        std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
             return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));

src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h

@@ -21,7 +21,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
         protected:
             storm::models::symbolic::Dtmc<DdType, ValueType> const& getModel() const override;

src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp

@@ -32,11 +32,11 @@ 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() || formula.isRewardPathFormula()) {
+            if (formula.isPctlStateFormula() || formula.isPctlPathFormula()) {
                 return true;
             }
             if (formula.isProbabilityOperatorFormula()) {
-                return this->canHandle(checkTask.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
             }
             if (formula.isGloballyFormula()) {
                 return true;
@@ -102,10 +102,10 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> SymbolicMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
             return storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory);
         }

src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h

@@ -23,7 +23,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula> 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::ReachabilityRewardFormula> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
             
             protected:
             storm::models::symbolic::Mdp<DdType, ValueType> const& getModel() const override;

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -83,9 +83,9 @@ namespace storm {
         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.replaceFormula(formula.asProbabilityOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asProbabilityOperatorFormula().getSubformula()));
             } else if (formula.isRewardOperatorFormula()) {
-                return this->canHandle(checkTask.replaceFormula(formula.asRewardOperatorFormula().getSubformula()));
+                return this->canHandle(checkTask.substituteFormula(formula.asRewardOperatorFormula().getSubformula()));
             } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
                 if (formula.isUntilFormula()) {
                     storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
@@ -103,11 +103,6 @@ namespace storm {
                 if (boundedUntilFormula.getLeftSubformula().isPropositionalFormula() && boundedUntilFormula.getRightSubformula().isPropositionalFormula()) {
                     return true;
                 }
-            } else if (formula.isReachabilityRewardFormula()) {
-                storm::logic::ReachabilityRewardFormula const& reachabilityRewardFormula = formula.asReachabilityRewardFormula();
-                if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) {
-                    return true;
-                }
             } else if (formula.isConditionalPathFormula()) {
                 storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula();
                 if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
@@ -579,11 +574,11 @@ namespace storm {
         }
         
         template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> const& checkTask) {
-            storm::logic::ReachabilityRewardFormula const& rewardPathFormula = checkTask.getFormula();
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeReachabilityRewards(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+            storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
             
             // Retrieve the appropriate bitvectors by model checking the subformulas.
-            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
             storm::storage::BitVector phiStates(this->getModel().getNumberOfStates(), true);
             storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
             

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h

@@ -26,7 +26,7 @@ namespace storm {
             virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
-            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(CheckTask<storm::logic::ReachabilityRewardFormula> 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> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula> const& checkTask) override;

src/parser/FormulaParser.cpp

@@ -129,7 +129,6 @@ namespace storm {
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardPathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> cumulativeRewardFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> reachabilityRewardFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> instantaneousRewardFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> longRunAverageRewardFormula;
             
@@ -139,7 +138,6 @@ namespace storm {
             // Methods that actually create the expression objects.
             std::shared_ptr<storm::logic::Formula> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
             std::shared_ptr<storm::logic::Formula> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
-            std::shared_ptr<storm::logic::Formula> createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const;
             std::shared_ptr<storm::logic::Formula> createLongRunAverageRewardFormula() const;
             std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
             std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;
@@ -255,10 +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");
             
-            reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)];
-            reachabilityRewardFormula.name("reachability reward formula");
-            
-            rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula;
+            rewardPathFormula = eventuallyFormula | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | conditionalFormula;
             rewardPathFormula.name("reward path formula");
             
             expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
@@ -382,7 +377,6 @@ namespace storm {
             qi::on_error<qi::fail>(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
-            qi::on_error<qi::fail>(reachabilityRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
         }
@@ -411,10 +405,6 @@ namespace storm {
             }
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ReachabilityRewardFormula(stateFormula));
-        }
-        
         std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageRewardFormula());
         }

src/storage/bisimulation/BisimulationDecomposition.cpp

@@ -122,11 +122,6 @@ namespace storm {
                 if (rightSubformula->isPropositionalFormula()) {
                     measureDrivenInitialPartition = true;
                 }
-            } else if (newFormula->isReachabilityRewardFormula()) {
-                rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer();
-                if (rightSubformula->isPropositionalFormula()) {
-                    measureDrivenInitialPartition = true;
-                }
             }
             
             if (measureDrivenInitialPartition) {