diff --git a/prism/src/pta/DBM.java b/prism/src/pta/DBM.java
index 98e4eda9..d97ecbff 100644
--- a/prism/src/pta/DBM.java
+++ b/prism/src/pta/DBM.java
@@ -57,7 +57,7 @@ public class DBM extends Zone
 		return pta;
 	}
 
-	/* Zone operations */
+	// Zone operations (modify the zone)
 
 	/**
 	 * Conjunction: add constraint x-y db
@@ -225,6 +225,35 @@ public class DBM extends Zone
 		canonicalise();
 	}
 
+	// Zone operations (create new zone)
+	
+	/**
+	 * Complement this DBM; creates a new DBM list as result.
+	 */
+	public DBMList createComplement()
+	{
+		DBMList list = new DBMList(pta);
+		DBM dbmNew;
+		int i, j, n;
+		n = d.length - 1;
+		for (i = 0; i < n + 1; i++) {
+			for (j = 0; j < n + 1; j++) {
+				if (i == j)
+					continue;
+				if (DB.isInfty(d[i][j]))
+					continue;
+				dbmNew = (DBM) new DBMFactory().createTrue(pta);
+				dbmNew.addConstraint(j, i, DB.dual(d[i][j]));
+				if (!dbmNew.isEmpty()) {
+					list.addDBM(dbmNew);
+				}
+			}
+		}
+		return list;
+	}
+
+	// Zone queries (do not modify the zone)
+	
 	/**
 	 * Is this zone empty (i.e. inconsistent)?
 	 */
@@ -276,31 +305,8 @@ public class DBM extends Zone
 		return DB.getSignedDiff(d[x][0]);
 	}
 	
-	/**
-	 * Complement this DBM; creates a new DBM list as result.
-	 */
-	public DBMList createComplement()
-	{
-		DBMList list = new DBMList(pta);
-		DBM dbmNew;
-		int i, j, n;
-		n = d.length - 1;
-		for (i = 0; i < n + 1; i++) {
-			for (j = 0; j < n + 1; j++) {
-				if (i == j)
-					continue;
-				if (DB.isInfty(d[i][j]))
-					continue;
-				dbmNew = (DBM) new DBMFactory().createTrue(pta);
-				dbmNew.addConstraint(j, i, DB.dual(d[i][j]));
-				if (!dbmNew.isEmpty()) {
-					list.addDBM(dbmNew);
-				}
-			}
-		}
-		return list;
-	}
-
+	// Misc
+	
 	/**
 	 * Clone this zone
 	 */
@@ -318,6 +324,14 @@ public class DBM extends Zone
 		return copy;
 	}
 
+	/**
+	 * Get storage info string
+	 */
+	public String storageInfo()
+	{
+		return "DBM with " + pta.numClocks + " clocks";
+	}
+
 	// Standard Java methods
 
 	public int hashCode()
@@ -415,14 +429,6 @@ public class DBM extends Zone
 		return s;
 	}
 
-	/**
-	 * Get storage info string
-	 */
-	public String storageInfo()
-	{
-		return "DBM with " + pta.numClocks + " clocks";
-	}
-
 	/* Private utility methods */
 
 	/**
diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java
index 3655013c..73dcbc89 100644
--- a/prism/src/pta/DBMList.java
+++ b/prism/src/pta/DBMList.java
@@ -125,7 +125,7 @@ public class DBMList extends NCZone
 		return pta;
 	}
 
-	/* Zone operations */
+	// Zone operations (modify the zone)
 
 	/**
 	 * Conjunction: add constraint x-y db
@@ -181,20 +181,6 @@ public class DBMList extends NCZone
 		list = listNew.list;
 	}
 
-	/**
-	 * Conjunction: with complement of another zone
-	 */
-	public void intersectComplement(Zone z)
-	{
-		if (z instanceof DBM)
-			z = new DBMList((DBM) z);
-		DBMList dbml = (DBMList) z;
-		for (DBM dbm : dbml.list) {
-			DBMList listTmp = dbm.createComplement();
-			intersect(listTmp);
-		}
-	}
-
 	/**
 	 * Up, i.e. let time elapse, subject to some constraints
 	 */
@@ -269,6 +255,8 @@ public class DBMList extends NCZone
 		throw new RuntimeException("Not implemented yet");
 	}
 
+	// Zone operations (create new zone)
+	
 	/**
 	 * Complement
 	 * Creates non-convex zone so creates new one,
@@ -281,33 +269,8 @@ public class DBMList extends NCZone
 		return dbml;
 	}
 
-	/**
-	 * Complement
-	 */
-	public void complement()
-	{
-		DBMList listNew, res;
-		res = null;
-		// Special case: complement of empty DBM list is True
-		if (list.size() == 0)
-			addDBM(DBM.createTrue(pta));
-		// The complement of a list of DBMs is the intersection
-		// of the complement of each DBM (and the complement of
-		// of a DBM is a DBM list).
-		for (DBM dbm : list) {
-			listNew = dbm.createComplement();
-			if (res == null)
-				res = listNew;
-			else {
-				res.intersect(listNew);
-			}
-			// Stop early if res already empty
-			if (res.list.size() == 0)
-				break;
-		}
-		list = res.list;
-	}
-
+	// Zone queries (do not modify the zone)
+	
 	/**
 	 * Is this zone empty (i.e. inconsistent)?
 	 */
@@ -344,6 +307,75 @@ public class DBMList extends NCZone
 		return false;
 	}
 
+	/**
+	 * Get the minimum value of a clock. 
+	 */
+	public int getMin(int x)
+	{
+		// Take min across all DBMs
+		int min = Integer.MAX_VALUE;
+		for (DBM dbm : list) {
+			min = Math.min(min, dbm.getMin(x));
+		}
+		return min;
+	}
+	
+	/**
+	 * Get the maximum value of a clock. 
+	 */
+	public int getMax(int x)
+	{
+		// Take max across all DBMs
+		int max = Integer.MIN_VALUE;
+		for (DBM dbm : list) {
+			max = Math.max(max, dbm.getMax(x));
+		}
+		return max;
+	}
+	
+	// Methods required for NCZone interface
+	
+	/**
+	 * Conjunction: with complement of another zone
+	 */
+	public void intersectComplement(Zone z)
+	{
+		if (z instanceof DBM)
+			z = new DBMList((DBM) z);
+		DBMList dbml = (DBMList) z;
+		for (DBM dbm : dbml.list) {
+			DBMList listTmp = dbm.createComplement();
+			intersect(listTmp);
+		}
+	}
+
+	/**
+	 * Complement
+	 */
+	public void complement()
+	{
+		DBMList listNew, res;
+		res = null;
+		// Special case: complement of empty DBM list is True
+		if (list.size() == 0)
+			addDBM(DBM.createTrue(pta));
+		// The complement of a list of DBMs is the intersection
+		// of the complement of each DBM (and the complement of
+		// of a DBM is a DBM list).
+		for (DBM dbm : list) {
+			listNew = dbm.createComplement();
+			if (res == null)
+				res = listNew;
+			else {
+				res.intersect(listNew);
+			}
+			// Stop early if res already empty
+			if (res.list.size() == 0)
+				break;
+		}
+		list = res.list;
+	}
+
 	/**
 	 * Clone this zone
 	 */
diff --git a/prism/src/pta/Zone.java b/prism/src/pta/Zone.java
index d5705642..5baeeba5 100644
--- a/prism/src/pta/Zone.java
+++ b/prism/src/pta/Zone.java
@@ -34,7 +34,7 @@ public abstract class Zone
 
 	public abstract PTA getPTA();
 
-	/* Zone operations */
+	// Zone operations (modify the zone)
 
 	/**
 	 * Conjunction: add constraint x-y db
@@ -102,6 +102,8 @@ public abstract class Zone
 	 */
 	public abstract void cClosure(int c);
 
+	// Zone operations (create new zone)
+	
 	/**
 	 * Complement
 	 * Creates non-convex zone so creates new one,
@@ -109,6 +111,8 @@ public abstract class Zone
 	 */
 	public abstract NCZone createComplement();
 
+	// Zone queries (do not modify the zone)
+	
 	/**
 	 * Is this zone empty (i.e. inconsistent)?
 	 */
@@ -125,12 +129,22 @@ public abstract class Zone
 	public abstract boolean includes(DBM dbm);
 	
 	/**
-	 * Clone this zone
+	 * Get the minimum value of a clock. 
 	 */
-	public abstract Zone deepCopy();
+	public abstract int getMin(int x);
+	
+	/**
+	 * Get the maximum value of a clock. 
+	 */
+	public abstract int getMax(int x);
 	
 	// Misc
 	
+	/**
+	 * Clone this zone
+	 */
+	public abstract Zone deepCopy();
+	
 	/**
 	 * Get storage info string
 	 */