SamplerBoundedUntilDisc: tweak handling of absent upper bound

We now explicitly remember if there was an upper bound instead of
relying on an upper bound of Integer.MAX_VALUE in the case of an
absent bound.

Statistical MC, P[F]/P[U] in discrete time setting with time bounds.

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -38,6 +38,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 	private Expression right;
 	private int lb;
 	private int ub;
+	private boolean haveUpperBound;
 
 	/**
 	 * Construct a sampler for a (discrete-time) bounded until property.
@@ -68,17 +69,19 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 		}
 		// Upper bound
 		if (expr.getUpperBound() != null) {
+			haveUpperBound = true;
 			ub = expr.getUpperBound().evaluateInt();
 			if (expr.upperBoundIsStrict()) {
 				// Convert to non-strict bound:  <ub  <=>  <=ub-1
 				ub = ub - 1;
 			}
+
+			if (ub < 0) {
+				throw new PrismException("Invalid upper bound in "+expr);
+			}
 		} else {
 			// No upper bound
-			ub = Integer.MAX_VALUE;
-		}
-		if (ub < 0) {
-			throw new PrismException("Invalid upper bound in "+expr);
+			haveUpperBound = false;
 		}
 
 		// Initialise sampler info
@@ -95,7 +98,7 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 		
 		long pathSize = path.size();
 		// Upper bound exceeded
-		if (pathSize > ub) {
+		if (haveUpperBound && pathSize > ub) {
 			valueKnown = true;
 			value = false;
 		}