Add SanityJDD: Framework for performing basic sanity checks on the symbolic MTBDD operations

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

prism/src/jdd/SanityJDD.java

@@ -0,0 +1,186 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package jdd;
+
+/**
+ * Helper class for doing sanity checks in the symbolic engines.
+ * <br>
+ * As the sanity checks perform various MTBDD operations, which
+ * can be costly and can lead to a significant slow-down, the
+ * sanity checks should only be enabled for debugging purposes.
+ * <br>
+ * The sanity checks are enabled by setting the
+ * {@code static boolean enabled} to true.
+ * <br>
+ * In your code, check this variable before calling one
+ * of the check methods.
+ */
+public class SanityJDD
+{
+	/** Global flag: is sanity checking enabled? */
+	public static boolean enabled = false;
+
+	/**
+	 * Perform sanity check: Is a contained in b?
+	 * <br>
+	 * a and b have to be 0/1 MTBDDs.
+	 * <br>
+	 * Throws a RuntimeException if the test fails.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static void checkIsContainedIn(JDDNode a, JDDNode b)
+	{
+		if (!enabled)
+			return;
+
+		checkIsZeroOneMTBDD(a);
+		checkIsZeroOneMTBDD(b);
+
+		if (!JDD.IsContainedIn(a, b)) {
+			error("a is not contained in b");
+		}
+	}
+
+	/**
+	 * Perform sanity check:
+	 * Is node a 0/1-MTBDD, i.e., has only 0 and 1 as constants.
+	 * <br>
+	 * Throws a RuntimeException if the test fails.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static void checkIsZeroOneMTBDD(JDDNode node)
+	{
+		if (!enabled)
+			return;
+
+		if (!JDD.IsZeroOneMTBDD(node)) {
+			error("MTBDD is not a 0/1-MTBDD");
+		}
+	}
+
+	/**
+	 * Perform sanity check:
+	 * Are the variable indizes for the vars vector
+	 * in increasing order?
+	 * <br>
+	 * This is an assumption for various methods
+	 * taking a list of variables as argument.
+	 * <br>
+	 * Throws a RuntimeException if the test fails.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static void checkVarsAreSorted(JDDVars vars)
+	{
+		if (!enabled)
+			return;
+
+		int lastIndex = -1;
+		for (JDDNode var : vars) {
+			int index = var.getIndex();
+			if (index < lastIndex) {
+				error("JDDVars are not sorted: " + vars);
+			}
+			lastIndex = index;
+		}
+	}
+
+	/**
+	 * Perform sanity check:
+	 * Ensure that node has no relevant variables outside of the allowedVars.
+	 * <br>
+	 * Throws a RuntimeException if the test fails.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static void checkIsDDOverVars(JDDNode node, JDDVars... allowedVars)
+	{
+		if (!enabled)
+			return;
+
+		JDDNode cube = null;
+		JDDNode support = null;
+		JDDNode combined = null;
+
+		try {
+			// cube of the combined JDDVars
+			cube = JDD.Constant(1);
+			for (JDDVars vars : allowedVars) {
+				cube = JDD.And(cube, vars.toCubeSet());
+			}
+
+			// the support of the node, a cube as well
+			support = JDD.GetSupport(node);
+			// If all variables in the support of node are also
+			// variables in the cube, ANDing them will not change
+			// the cube. If this is not the case, then there are
+			// variables in the support that are not in the cube
+			combined = JDD.And(support.copy(), cube.copy());
+			if (!combined.equals(cube)) {
+				error("MTBDD has unexpected essential variables");
+			}
+		} finally {
+			if (support != null)
+				JDD.Deref(support);
+			if (cube != null)
+				JDD.Deref(cube);
+			if (combined != null)
+				JDD.Deref(combined);
+		}
+	}
+	
+	/**
+	 * Perform sanity check:
+	 * Ensure that node is a state set over the given state variables.
+	 * <br>
+	 * Throws a RuntimeException if the test fails.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static void checkIsStateSet(JDDNode node, JDDVars vars)
+	{
+		if (!enabled)
+			return;
+
+		checkIsZeroOneMTBDD(node);
+		checkIsDDOverVars(node, vars);
+	}
+
+	/** Generic check method, raise error with the given message if value is false */
+	public static void check(boolean value, String message)
+	{
+		if (!enabled)
+			return;
+
+		if (!value) {
+			error(message);
+		}
+	}
+
+	/** Throw error */
+	private static void error(String message)
+	{
+		throw new RuntimeException(message);
+	}
+}