From caf5a0e50bb6513bb39fc3d86f78bd7de516b228 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sun, 31 Aug 2014 21:19:32 +0000
Subject: [PATCH] Bugfix: statistical model checking of discrete-time bounded
 untils with strict bounds (from Joachim Klein).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9163 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../sampler/SamplerBoundedUntilDisc.java      | 34 +++++++++++++++++--
 1 file changed, 31 insertions(+), 3 deletions(-)

diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java
index 43c61616..c58b8368 100644
--- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java
+++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java
@@ -2,7 +2,8 @@
 //	
 //	Copyright (c) 2002-
 //	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -51,8 +52,35 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 			throw new PrismException("Error creating Sampler");
 		left = expr.getOperand1();
 		right = expr.getOperand2();
-		lb = expr.getLowerBound() == null ? 0 : expr.getLowerBound().evaluateInt();
-		ub = expr.getUpperBound() == null ? Integer.MAX_VALUE : expr.getUpperBound().evaluateInt();
+		// Lower bound
+		if (expr.getLowerBound() != null) {
+			lb = expr.getLowerBound().evaluateInt();
+			if (expr.lowerBoundIsStrict()) {
+				// Convert to non-strict bound:  >lb  <=>  >=lb+1
+				lb = lb + 1;
+			}
+		} else {
+			// No lower bound
+			lb = 0;
+		}
+		if (lb < 0) {
+			throw new PrismException("Invalid lower bound in "+expr);
+		}
+		// Upper bound
+		if (expr.getUpperBound() != null) {
+			ub = expr.getUpperBound().evaluateInt();
+			if (expr.upperBoundIsStrict()) {
+				// Convert to non-strict bound:  <ub  <=>  <=ub-1
+				ub = ub - 1;
+			}
+		} else {
+			// No upper bound
+			ub = Integer.MAX_VALUE;
+		}
+		if (ub < 0) {
+			throw new PrismException("Invalid upper bound in "+expr);
+		}
+
 		// Initialise sampler info
 		reset();
 		resetStats();