From 93d028bde5571e72b6a54b892a76eb43be3a1315 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 1 Nov 2010 21:48:51 +0000
Subject: [PATCH] Added unbounded check to Zone classes (+ API tweak).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2216 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/DBM.java     | 27 +++++++++++++++++++++++++--
 prism/src/pta/DBMList.java | 36 ++++++++++++++++++++++++++++++++----
 prism/src/pta/Zone.java    | 14 ++++++++++++--
 3 files changed, 69 insertions(+), 8 deletions(-)

diff --git a/prism/src/pta/DBM.java b/prism/src/pta/DBM.java
index d97ecbff..f6a57f0f 100644
--- a/prism/src/pta/DBM.java
+++ b/prism/src/pta/DBM.java
@@ -292,7 +292,7 @@ public class DBM extends Zone
 	/**
 	 * Get the minimum value of a clock. 
 	 */
-	public int getMin(int x)
+	public int getClockMin(int x)
 	{
 		return -DB.getSignedDiff(d[0][x]);
 	}
@@ -300,11 +300,34 @@ public class DBM extends Zone
 	/**
 	 * Get the maximum value of a clock. 
 	 */
-	public int getMax(int x)
+	public int getClockMax(int x)
 	{
 		return DB.getSignedDiff(d[x][0]);
 	}
 	
+	/**
+	 * Check if a clock is unbounded (can be infinite).
+	 */
+	public boolean clockIsUnbounded(int x)
+	{
+		return DB.isInfty(d[x][0]);
+	}
+	
+	/**
+	 * Check if all clocks are unbounded (can be infinite).
+	 */
+	public boolean allClocksAreUnbounded()
+	{
+		int i, n;
+		n = pta.numClocks;
+		for (i = 0; i < n + 1; i++) {
+			if (!DB.isInfty(d[i][0])) {
+				return false;
+			}
+		}
+		return true;
+	}
+	
 	// Misc
 	
 	/**
diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java
index 73dcbc89..1a6bde71 100644
--- a/prism/src/pta/DBMList.java
+++ b/prism/src/pta/DBMList.java
@@ -310,12 +310,12 @@ public class DBMList extends NCZone
 	/**
 	 * Get the minimum value of a clock. 
 	 */
-	public int getMin(int x)
+	public int getClockMin(int x)
 	{
 		// Take min across all DBMs
 		int min = Integer.MAX_VALUE;
 		for (DBM dbm : list) {
-			min = Math.min(min, dbm.getMin(x));
+			min = Math.min(min, dbm.getClockMin(x));
 		}
 		return min;
 	}
@@ -323,16 +323,44 @@ public class DBMList extends NCZone
 	/**
 	 * Get the maximum value of a clock. 
 	 */
-	public int getMax(int x)
+	public int getClockMax(int x)
 	{
 		// Take max across all DBMs
 		int max = Integer.MIN_VALUE;
 		for (DBM dbm : list) {
-			max = Math.max(max, dbm.getMax(x));
+			max = Math.max(max, dbm.getClockMax(x));
 		}
 		return max;
 	}
 	
+	/**
+	 * Check if a clock is unbounded (can be infinite).
+	 */
+	public boolean clockIsUnbounded(int x)
+	{
+		// Clock is unbounded if is in any DBM
+		for (DBM dbm : list) {
+			if (dbm.clockIsUnbounded(x))
+				return true;
+		}
+		return false;
+	}
+	
+	/**
+	 * Check if all clocks are unbounded (can be infinite).
+	 */
+	public boolean allClocksAreUnbounded()
+	{
+		int i, n;
+		n = pta.numClocks;
+		for (i = 0; i < n + 1; i++) {
+			if (!clockIsUnbounded(i)) {
+				return false;
+			}
+		}
+		return true;
+	}
+	
 	// Methods required for NCZone interface
 	
 	/**
diff --git a/prism/src/pta/Zone.java b/prism/src/pta/Zone.java
index 5baeeba5..6c80204e 100644
--- a/prism/src/pta/Zone.java
+++ b/prism/src/pta/Zone.java
@@ -131,12 +131,22 @@ public abstract class Zone
 	/**
 	 * Get the minimum value of a clock. 
 	 */
-	public abstract int getMin(int x);
+	public abstract int getClockMin(int x);
 	
 	/**
 	 * Get the maximum value of a clock. 
 	 */
-	public abstract int getMax(int x);
+	public abstract int getClockMax(int x);
+	
+	/**
+	 * Check if a clock is unbounded (can be infinite).
+	 */
+	public abstract boolean clockIsUnbounded(int x);
+	
+	/**
+	 * Check if all clocks are unbounded (can be infinite).
+	 */
+	public abstract boolean allClocksAreUnbounded();
 	
 	// Misc