jdd.JDD: add sanity checks (SanityJDD framework)

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

prism/src/jdd/JDD.java

@@ -380,6 +380,9 @@ public class JDD
 	 */
 	public static JDDNode Not(JDDNode dd)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd);
+		}
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_Not(dd.ptr()));
@@ -391,6 +394,10 @@ public class JDD
 	 */
 	public static JDDNode Or(JDDNode dd1, JDDNode dd2)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd1);
+			SanityJDD.checkIsZeroOneMTBDD(dd2);
+		}
 		if (DebugJDD.debugEnabled) {
 			DebugJDD.DD_Method_Argument(dd1);
 			DebugJDD.DD_Method_Argument(dd2);
@@ -428,6 +435,10 @@ public class JDD
 	 */
 	public static JDDNode And(JDDNode dd1, JDDNode dd2)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd1);
+			SanityJDD.checkIsZeroOneMTBDD(dd2);
+		}
 		if (DebugJDD.debugEnabled) {
 			DebugJDD.DD_Method_Argument(dd1);
 			DebugJDD.DD_Method_Argument(dd2);
@@ -466,6 +477,10 @@ public class JDD
 	 */
 	public static JDDNode Xor(JDDNode dd1, JDDNode dd2)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd1);
+			SanityJDD.checkIsZeroOneMTBDD(dd2);
+		}
 		if (DebugJDD.debugEnabled) {
 			DebugJDD.DD_Method_Argument(dd1);
 			DebugJDD.DD_Method_Argument(dd2);
@@ -581,6 +596,9 @@ public class JDD
 	 */
 	public static JDDNode Restrict(JDDNode dd, JDDNode cube)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd);
+		}
 		if (DebugJDD.debugEnabled) {
 			DebugJDD.DD_Method_Argument(dd);
 			DebugJDD.DD_Method_Argument(cube);
@@ -594,6 +612,9 @@ public class JDD
 	 */
 	public static JDDNode ITE(JDDNode dd1, JDDNode dd2, JDDNode dd3)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd1);
+		}
 		if (DebugJDD.debugEnabled) {
 			DebugJDD.DD_Method_Argument(dd1);
 			DebugJDD.DD_Method_Argument(dd2);
@@ -608,6 +629,10 @@ public class JDD
 	 */
 	public static boolean AreIntersecting(JDDNode dd1, JDDNode dd2)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd1);
+			SanityJDD.checkIsZeroOneMTBDD(dd2);
+		}
 		JDDNode tmp;
 		boolean res;
 		JDD.Ref(dd1);
@@ -624,6 +649,10 @@ public class JDD
 	 */
 	public static boolean IsContainedIn(JDDNode dd1, JDDNode dd2)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd1);
+			SanityJDD.checkIsZeroOneMTBDD(dd2);
+		}
 		JDDNode tmp;
 		boolean res;
 		JDD.Ref(dd1);
@@ -713,6 +742,9 @@ public class JDD
 	 */
 	public static JDDNode ThereExists(JDDNode dd, JDDVars vars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd);
+		}
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_ThereExists(dd.ptr(), vars.array(), vars.n()));
@@ -724,6 +756,9 @@ public class JDD
 	 */
 	public static JDDNode ForAll(JDDNode dd, JDDVars vars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd);
+		}
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_ForAll(dd.ptr(), vars.array(), vars.n()));
@@ -998,6 +1033,11 @@ public class JDD
 	 */
 	public static boolean isSingleton(JDDNode dd, JDDVars vars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsZeroOneMTBDD(dd);
+			SanityJDD.checkVarsAreSorted(vars);
+		}
+		
 		int i=0;
 		while (!dd.isConstant()) {
 			int index = dd.getIndex();
@@ -1167,6 +1207,9 @@ public class JDD
 	 */
 	public static JDDNode SetVectorElement(JDDNode dd, JDDVars vars, long index, double value)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+		}
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_SetVectorElement(dd.ptr(), vars.array(), vars.n(), index, value));
@@ -1178,6 +1221,9 @@ public class JDD
 	 */
 	public static JDDNode SetMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, long rindex, long cindex, double value)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+		}
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_SetMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), rindex, cindex, value));
@@ -1189,6 +1235,9 @@ public class JDD
 	 */
 	public static JDDNode Set3DMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, JDDVars lvars, long rindex, long cindex, long lindex, double value)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars, lvars);
+		}
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_Set3DMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), lvars.array(), lvars.n(), rindex, cindex, lindex, value));
@@ -1200,6 +1249,9 @@ public class JDD
 	 */
 	public static double GetVectorElement(JDDNode dd, JDDVars vars, long index)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+		}
 		double rv = DD_GetVectorElement(dd.ptr(), vars.array(), vars.n(), index);
 		checkForCuddError();
 		return rv;
@@ -1211,6 +1263,9 @@ public class JDD
 	 */
 	public static JDDNode Identity(JDDVars rvars, JDDVars cvars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.check(rvars.n() == cvars.n(), "Mismatch of JDDVars sizes");
+		}
 		return ptrToNode(DD_Identity(rvars.array(), cvars.array(), rvars.n()));
 	}
 	
@@ -1220,6 +1275,10 @@ public class JDD
 	 */
 	public static JDDNode Transpose(JDDNode dd, JDDVars rvars, JDDVars cvars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+		}
+
 		if (DebugJDD.debugEnabled)
 			DebugJDD.DD_Method_Argument(dd);
 		return ptrToNode(DD_Transpose(dd.ptr(), rvars.array(), cvars.array(), rvars.n()));
@@ -1392,6 +1451,9 @@ public class JDD
 	 */
 	public static void PrintVector(JDDNode dd, JDDVars vars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+		}
 		DD_PrintVector(dd.ptr(), vars.array(), vars.n(), NORMAL);
 	}
 	
@@ -1401,6 +1463,9 @@ public class JDD
 	 */
 	public static void PrintVector(JDDNode dd, JDDVars vars, int accuracy)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+		}
 		DD_PrintVector(dd.ptr(), vars.array(), vars.n(), accuracy);
 	}
 	
@@ -1410,6 +1475,9 @@ public class JDD
 	 */
 	public static void PrintMatrix(JDDNode dd, JDDVars rvars, JDDVars cvars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+		}
 		DD_PrintMatrix(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), NORMAL);
 	}
 	
@@ -1419,6 +1487,9 @@ public class JDD
 	 */
 	public static void PrintMatrix(JDDNode dd, JDDVars rvars, JDDVars cvars, int accuracy)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+		}
 		DD_PrintMatrix(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), accuracy);
 	}
 	
@@ -1428,6 +1499,10 @@ public class JDD
 	 */
 	public static void PrintVectorFiltered(JDDNode dd, JDDNode filter, JDDVars vars)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+			SanityJDD.checkIsDDOverVars(filter, vars);
+		}
 		DD_PrintVectorFiltered(dd.ptr(), filter.ptr(), vars.array(), vars.n(), NORMAL);
 	}
 	
@@ -1437,6 +1512,10 @@ public class JDD
 	 */
 	public static void PrintVectorFiltered(JDDNode dd, JDDNode filter, JDDVars vars, int accuracy)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+			SanityJDD.checkIsDDOverVars(filter, vars);
+		}
 		DD_PrintVectorFiltered(dd.ptr(), filter.ptr(), vars.array(), vars.n(), accuracy);
 	}
 	
@@ -1446,6 +1525,9 @@ public class JDD
 	 */
 	public static void TraverseVector(JDDNode dd, JDDVars vars, JDDVectorConsumer vc, int code)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, vars);
+		}
 		TraverseVectorRec(dd, vars, 0, 0, vc, code);
 	}
 	
@@ -1505,6 +1587,10 @@ public class JDD
 	 */
 	public static void ExportMatrixToPPFile(JDDNode dd, JDDVars rvars, JDDVars cvars, String filename)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+			SanityJDD.check(rvars.n() == cvars.n(), "Mismatch of JDDVars sizes");
+		}
 		DD_ExportMatrixToPPFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), filename);
 	}
 	
@@ -1535,6 +1621,10 @@ public class JDD
 	 */
 	public static void Export3dMatrixToPPFile(JDDNode dd, JDDVars rvars, JDDVars cvars, JDDVars nvars, String filename)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars, nvars);
+			SanityJDD.check(rvars.n() == cvars.n(), "Mismatch of JDDVars sizes");
+		}
 		DD_Export3dMatrixToPPFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), nvars.array(), nvars.n(), filename);
 	}
 
@@ -1544,6 +1634,10 @@ public class JDD
 	 */
 	public static void ExportMatrixToMatlabFile(JDDNode dd, JDDVars rvars, JDDVars cvars, String name, String filename)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+			SanityJDD.check(rvars.n() == cvars.n(), "Mismatch of JDDVars sizes");
+		}
 		DD_ExportMatrixToMatlabFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), name, filename);
 	}
 
@@ -1553,6 +1647,10 @@ public class JDD
 	 */
 	public static void ExportMatrixToSpyFile(JDDNode dd, JDDVars rvars, JDDVars cvars, int depth, String filename)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(dd, rvars, cvars);
+			SanityJDD.check(rvars.n() == cvars.n(), "Mismatch of JDDVars sizes");
+		}
 		DD_ExportMatrixToSpyFile(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), depth, filename);
 	}