From 6f1408812eaae0f190c4f34804c7364064ab3ff1 Mon Sep 17 00:00:00 2001
From: Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk>
Date: Wed, 31 Jul 2013 00:37:42 +0000
Subject: [PATCH] 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 | 34 +++++++++++++++++++++++++++++++++-
 prism/src/pta/DBMList.java    |  4 ++++
 2 files changed, 37 insertions(+), 1 deletion(-)

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