From ae44dd8180ef4230971c13cb1bee9ec85576f394 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:25:48 +0200
Subject: [PATCH] imported patch
 rewardcounter-IntegerBound.fromTemporalOperatorBound.patch

---
 prism/src/prism/IntegerBound.java | 42 +++++++++++++++++++++++--------
 1 file changed, 32 insertions(+), 10 deletions(-)

diff --git a/prism/src/prism/IntegerBound.java b/prism/src/prism/IntegerBound.java
index 29b76f34..f9d746da 100644
--- a/prism/src/prism/IntegerBound.java
+++ b/prism/src/prism/IntegerBound.java
@@ -64,9 +64,13 @@ public class IntegerBound
 	/**
 	 * Extract the bounds from an {@code ExpressionTemporal} expression
 	 * and create the corresponding {@code IntegerBound}.
-	 *
+	 * <br>
+	 * This only works if there is a single bound. Additionally, this
+	 * assumes that we are in the discrete-time setting, i.e., that
+	 * step and time bounds coincide.
+	 * <br>
 	 * Expects that constants for the upper and lower bounds have already been resolved.
-	 *
+	 * <br>
 	 * If {@code check} is {@code true}, throws an exception for negative or empty bounds.
 	 *
 	 * @param expression the expression
@@ -94,23 +98,41 @@ public class IntegerBound
 	 */
 	public static IntegerBound fromExpressionTemporal(ExpressionTemporal expression, Values constantValues, boolean check) throws PrismException
 	{
-		TemporalOperatorBound eBound = expression.getBounds().getStepBoundForDiscreteTime();
+		TemporalOperatorBound bound = expression.getBounds().getStepBoundForDiscreteTime();
+		return fromTemporalOperatorBound(bound, constantValues, check);
+	}
+
+	/**
+	 * Extract the bounds from a {@code TemporalOperatorBound}
+	 * and create the corresponding {@code IntegerBound}, resolving constants
+	 * via {@code constantValues}.
+	 *
+	 * If {@code check} is {@code true}, throws an exception for negative or empty bounds.
+	 *
+	 * @param bound the TemporalOperatorBounds
+	 * @param constantValues the values for constants (may be {@code null})
+	 * @param check check for non-negative bounds / non-emptiness?
+	 * @return the {@code IntegerBound} for the bound
+	 * @throws PrismException
+	 */
+	public static IntegerBound fromTemporalOperatorBound(TemporalOperatorBound bound, Values constantValues, boolean check) throws PrismException
+	{
 		IntegerBound bounds;
-		if (eBound == null) {
+		if (bound == null) {
 			bounds = new IntegerBound(null, false, null, false);
 		} else {
-			bounds =  new IntegerBound(eBound.getLowerBound() == null ? null : eBound.getLowerBound().evaluateInt(constantValues),
-		                                eBound.lowerBoundIsStrict(),
-		                                eBound.getUpperBound() == null ? null : eBound.getUpperBound().evaluateInt(constantValues),
-		                                eBound.upperBoundIsStrict());
+			bounds =  new IntegerBound(bound.getLowerBound() == null ? null : bound.getLowerBound().evaluateInt(constantValues),
+		                                bound.lowerBoundIsStrict(),
+		                                bound.getUpperBound() == null ? null : bound.getUpperBound().evaluateInt(constantValues),
+		                                bound.upperBoundIsStrict());
 		}
 
 		if (check) {
 			if (bounds.hasNegativeBound()) {
-				throw new PrismException("Negative bound in "+expression.toString());
+				throw new PrismException("Negative bound in "+bound);
 			}
 			if (bounds.isEmpty()) {
-				throw new PrismException("Empty bound in "+expression.toString());
+				throw new PrismException("Empty bound in "+bound);
 			}
 		}