From bbafd095bfd673fbcc553b64e7d85db9ecf72050 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Thu, 20 Aug 2020 23:07:15 -0700
Subject: [PATCH] no lower bound is still a zero bound :-)

---
 src/storm/logic/BoundedUntilFormula.cpp | 22 ++++++++++++++++++++++
 src/storm/logic/BoundedUntilFormula.h   |  3 +++
 2 files changed, 25 insertions(+)

diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 1933db10e..572712257 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -164,6 +164,7 @@ namespace storm {
         
         bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const {
             assert(i < lowerBound.size());
+            if (!hasLowerBound(i)) { return false; }
             return lowerBound.at(i).get().isStrict();
         }
         
@@ -181,6 +182,7 @@ namespace storm {
         }
         
         bool BoundedUntilFormula::hasIntegerLowerBound(unsigned i) const {
+            if (!hasLowerBound(i)) { return true; }
             return lowerBound.at(i).get().getBound().hasIntegerType();
         }
 
@@ -215,6 +217,7 @@ namespace storm {
         
         template <>
         double BoundedUntilFormula::getLowerBound(unsigned i) const {
+            if (!hasLowerBound(i)) { return 0.0; }
             checkNoVariablesInBound(this->getLowerBound());
             double bound = this->getLowerBound(i).evaluateAsDouble();
             STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
@@ -231,6 +234,7 @@ namespace storm {
         
         template <>
         storm::RationalNumber BoundedUntilFormula::getLowerBound(unsigned i) const {
+            if (!hasLowerBound(i)) { return storm::utility::zero<storm::RationalNumber>(); }
             checkNoVariablesInBound(this->getLowerBound(i));
             storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational();
             STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
@@ -247,6 +251,7 @@ namespace storm {
         
         template <>
         uint64_t BoundedUntilFormula::getLowerBound(unsigned i) const {
+            if (!hasLowerBound(i)) { return 0; }
             checkNoVariablesInBound(this->getLowerBound(i));
             int_fast64_t bound = this->getLowerBound(i).evaluateAsInt();
             STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
@@ -278,6 +283,23 @@ namespace storm {
                 return bound;
             }
         }
+
+        template <>
+        double BoundedUntilFormula::getNonStrictLowerBound(unsigned i) const {
+            double bound = getLowerBound<double>(i);
+            STORM_LOG_THROW(!isLowerBoundStrict(i), storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict lower bound from strict lower-bound.");
+            return bound;
+        }
+
+        template <>
+        uint64_t BoundedUntilFormula::getNonStrictLowerBound(unsigned i) const {
+            int_fast64_t bound = getLowerBound<uint64_t>(i);
+            if (isLowerBoundStrict(i)) {
+                return bound + 1;
+            } else {
+                return bound;
+            }
+        }
         
         void BoundedUntilFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index 5ae10e8b5..df1ff92b5 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -62,6 +62,9 @@ namespace storm {
             template <typename ValueType>
             ValueType getNonStrictUpperBound(unsigned i = 0) const;
 
+            template<typename ValueType>
+            ValueType getNonStrictLowerBound(unsigned i = 0) const;
+
             std::shared_ptr<BoundedUntilFormula const> restrictToDimension(unsigned i) const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;