SanityJDD: check for 'isVar', use in JDDVars.addVar

prism/src/jdd/JDDVars.java

@@ -78,7 +78,11 @@ public class JDDVars implements Iterable<JDDNode>
 	 */
 	public void addVar(JDDNode var)
 	{
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsVar(var);
+		}
 		vars.addElement(var);
+
 		if (arrayBuilt) DDV_FreeArray(array);
 		arrayBuilt = false;
 	}

prism/src/jdd/SanityJDD.java

@@ -154,6 +154,23 @@ public class SanityJDD
 		checkIsDDOverVars(node, vars);
 	}
 
+	/**
+	 * Perform sanity check:
+	 * Ensure that node is a variable node, i.e., a projection function for a single variable.
+	 * <br>
+	 * Throws a RuntimeException if the test fails.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static void checkIsVar(JDDNode node)
+	{
+		if (node.isConstant()) {
+			error("MTBDD is not a variable, but a constant");
+		}
+		if (!(node.getThen().equals(JDD.ONE) && node.getElse().equals(JDD.ZERO))) {
+			error("MTBDD is not a variable, but a complex function");
+		}
+	}
+
 	/** Generic check method, raise error with the given message if value is false */
 	public static void check(boolean value, String message)
 	{