From 6eabed4f09c83f14c502f5dd3a85af2ebc61b4c4 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:24:48 +0200
Subject: [PATCH] SanityJDD: check for 'isVar', use in JDDVars.addVar

---
 prism/src/jdd/JDDVars.java   |  4 ++++
 prism/src/jdd/SanityJDD.java | 17 +++++++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/prism/src/jdd/JDDVars.java b/prism/src/jdd/JDDVars.java
index bf040fcf..87136fdd 100644
--- a/prism/src/jdd/JDDVars.java
+++ b/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;
 	}
diff --git a/prism/src/jdd/SanityJDD.java b/prism/src/jdd/SanityJDD.java
index 1628ad08..0ef59717 100644
--- a/prism/src/jdd/SanityJDD.java
+++ b/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)
 	{