Added new constraint methods and size for DBMList

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7197 bbc10eb1-c90d-0410-af57-cb519fbb1720

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));
+	}
 }

prism/src/pta/DBMList.java

@@ -530,6 +530,10 @@ public class DBMList extends NCZone
 		}
 	}
 	
+	public int size() {
+		return list.size();
+	}
+
 	// Test program for complementing big DBM lists
 	
 	public static void main(String args[])