From 30977ed356a0bb61dedeb5cceb0b55edff9b9f1f Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 9 Sep 2020 15:26:48 +0200
Subject: [PATCH] Added some utility methods to reward path formulas

---
 src/storm/logic/CumulativeRewardFormula.cpp     | 10 +++++++++-
 src/storm/logic/CumulativeRewardFormula.h       |  3 +++
 src/storm/logic/LongRunAverageRewardFormula.cpp |  4 ++++
 src/storm/logic/LongRunAverageRewardFormula.h   |  3 ++-
 src/storm/logic/TotalRewardFormula.cpp          |  4 ++++
 src/storm/logic/TotalRewardFormula.h            |  1 +
 6 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index 33633b319..ccafab82c 100644
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/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 {
diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h
index cccd1ac9e..80924865a 100644
--- a/src/storm/logic/CumulativeRewardFormula.h
+++ b/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;
             
diff --git a/src/storm/logic/LongRunAverageRewardFormula.cpp b/src/storm/logic/LongRunAverageRewardFormula.cpp
index c36dab8a9..294c8de95 100644
--- a/src/storm/logic/LongRunAverageRewardFormula.cpp
+++ b/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);
         }
diff --git a/src/storm/logic/LongRunAverageRewardFormula.h b/src/storm/logic/LongRunAverageRewardFormula.h
index 03f1c3684..45bbe3de5 100644
--- a/src/storm/logic/LongRunAverageRewardFormula.h
+++ b/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;
diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp
index 4d1df7e0d..fb6f60873 100644
--- a/src/storm/logic/TotalRewardFormula.cpp
+++ b/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);
         }
diff --git a/src/storm/logic/TotalRewardFormula.h b/src/storm/logic/TotalRewardFormula.h
index a11fb3b03..1fa366723 100644
--- a/src/storm/logic/TotalRewardFormula.h
+++ b/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;