diff --git a/prism/src/pta/Constraint.java b/prism/src/pta/Constraint.java
index d0b242fb..d8f4388e 100644
--- a/prism/src/pta/Constraint.java
+++ b/prism/src/pta/Constraint.java
@@ -41,7 +41,7 @@ public class Constraint
 	 * @param y Right clock
 	 * @param db Difference bound encoded as an integer
 	 */
-	public Constraint(int x, int y, int db)
+	private Constraint(int x, int y, int db)
 	{
 		this.x = x;
 		this.y = y;
@@ -170,4 +170,36 @@ public class Constraint
 	{
 		return new Constraint(y, x, DB.createLt(0));
 	}
+	
+	/**
+	 * Build constraint x - y <= v.
+	 */
+	public static Constraint buildXYLeq(int x, int y, int v)
+	{
+		return new Constraint(x, y, DB.createLeq(v));
+	}
+
+	/**
+	 * Build constraint x - y < v.
+	 */
+	public static Constraint buildXYLt(int x, int y, int v)
+	{
+		return new Constraint(x, y, DB.createLt(v));
+	}
+
+	/**
+	 * Build constraint x - y >= v.
+	 */
+	public static Constraint buildXYGeq(int x, int y, int v)
+	{
+		return new Constraint(y, x, DB.createLeq(-v));
+	}
+
+	/**
+	 * Build constraint x - y > v.
+	 */
+	public static Constraint buildXYGt(int x, int y, int v)
+	{
+		return new Constraint(y, x, DB.createLt(-v));
+	}
 }
diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java
index ec7eacf5..7a0b2048 100644
--- a/prism/src/pta/DBMList.java
+++ b/prism/src/pta/DBMList.java
@@ -529,6 +529,10 @@ public class DBMList extends NCZone
 				list.remove(i);
 		}
 	}
+	
+	public int size() {
+		return list.size();
+	}
 
 	// Test program for complementing big DBM lists