Added some utility methods to reward path formulas

src/storm/logic/CumulativeRewardFormula.cpp

@@ -136,6 +136,10 @@ namespace storm {
             }
         }
         
+        std::vector<TimeBound> const& CumulativeRewardFormula::getBounds() const {
+            return bounds;
+        }
+        
         void CumulativeRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }
@@ -149,8 +153,12 @@ namespace storm {
         }
         
         
+        std::shared_ptr<CumulativeRewardFormula const> CumulativeRewardFormula::stripRewardAccumulation() const {
+            return std::make_shared<CumulativeRewardFormula const>(bounds, timeBoundReferences);
+        }
+        
         std::shared_ptr<CumulativeRewardFormula const> CumulativeRewardFormula::restrictToDimension(unsigned i) const {
-            return std::make_shared<CumulativeRewardFormula const>(bounds.at(i), getTimeBoundReference(i));
+            return std::make_shared<CumulativeRewardFormula const>(bounds.at(i), getTimeBoundReference(i), rewardAccumulation);
         }
         
         std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {

src/storm/logic/CumulativeRewardFormula.h

@@ -48,8 +48,11 @@ namespace storm {
             template <typename ValueType>
             ValueType getNonStrictBound() const;
             
+            std::vector<TimeBound> const& getBounds() const;
+            
             bool hasRewardAccumulation() const;
             RewardAccumulation const& getRewardAccumulation() const;
+            std::shared_ptr<CumulativeRewardFormula const> stripRewardAccumulation() const;
             
             std::shared_ptr<CumulativeRewardFormula const> restrictToDimension(unsigned i) const;
             

src/storm/logic/LongRunAverageRewardFormula.cpp

@@ -24,6 +24,10 @@ namespace storm {
             return rewardAccumulation.get();
         }
         
+        std::shared_ptr<LongRunAverageRewardFormula const> LongRunAverageRewardFormula::stripRewardAccumulation() const {
+            return std::make_shared<LongRunAverageRewardFormula>();
+        }
+        
         boost::any LongRunAverageRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }

src/storm/logic/LongRunAverageRewardFormula.h

@@ -19,7 +19,8 @@ namespace storm {
             virtual bool isRewardPathFormula() const override;
             bool hasRewardAccumulation() const;
             RewardAccumulation const& getRewardAccumulation() const;
-
+            std::shared_ptr<LongRunAverageRewardFormula const> stripRewardAccumulation() const;
+            
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/storm/logic/TotalRewardFormula.cpp

@@ -24,6 +24,10 @@ namespace storm {
             return rewardAccumulation.get();
         }
         
+       std::shared_ptr<TotalRewardFormula const> TotalRewardFormula::stripRewardAccumulation() const {
+            return std::make_shared<TotalRewardFormula>();
+        }
+        
         boost::any TotalRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }

src/storm/logic/TotalRewardFormula.h

@@ -20,6 +20,7 @@ namespace storm {
             virtual bool isRewardPathFormula() const override;
             bool hasRewardAccumulation() const;
             RewardAccumulation const& getRewardAccumulation() const;
+            std::shared_ptr<TotalRewardFormula const> stripRewardAccumulation() const;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;