From d6447a56f0235287187d6c472d0b967bf30a11d0 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 6 Jul 2017 19:07:15 +0200
Subject: [PATCH] minor fixes for reward bounded formulas

---
 src/storm/logic/BoundedUntilFormula.cpp | 14 +++++++++++++-
 src/storm/logic/BoundedUntilFormula.h   |  2 ++
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index b954d4720..ff5df2d2a 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -27,6 +27,15 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
+        void BoundedUntilFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            if (this->getTimeBoundReference().isRewardBound()) {
+                referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
+            }
+            this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
+            this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
+        }
+        
+        
         TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const {
             return timeBoundReference;
         }
@@ -92,7 +101,7 @@ namespace storm {
         template <>
         storm::RationalNumber BoundedUntilFormula::getUpperBound() const {
             checkNoVariablesInBound(this->getUpperBound());
-            storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
+            storm::RationalNumber bound = this->getUpperBound().evaluateAsRational();
             STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return bound;
         }
@@ -139,6 +148,9 @@ namespace storm {
             this->getLeftSubformula().writeToStream(out);
             
             out << " U";
+            if (this->getTimeBoundReference().isRewardBound()) {
+                out << "{\"" << this->getTimeBoundReference().getRewardName() << "\"}";
+            }
             if (this->hasLowerBound()) {
                 if (this->hasUpperBound()) {
                     if (this->isLowerBoundStrict()) {
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index 754d94cdf..5ff571d84 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -20,6 +20,8 @@ namespace storm {
             
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
+            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            
             TimeBoundReference const& getTimeBoundReference() const;