From f1556562823f43bd48dd86bc84cc289ab5819e96 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 22 Dec 2016 16:25:57 +0000
Subject: [PATCH] JDDVars: add method allZero() for obtaining a cubeset with
 all the variables negated

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11940 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/jdd/JDDVars.java | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/prism/src/jdd/JDDVars.java b/prism/src/jdd/JDDVars.java
index d1c70b40..bf040fcf 100644
--- a/prism/src/jdd/JDDVars.java
+++ b/prism/src/jdd/JDDVars.java
@@ -372,6 +372,21 @@ public class JDDVars implements Iterable<JDDNode>
 		return result;
 	}
 
+	/**
+	 * Constructs a 0/1-ADD that is the conjunction of
+	 * the negated variables, i.e.,
+	 * And(Not(v_1), Not(v_2), ..., Not(v_n))
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public JDDNode allZero()
+	{
+		JDDNode result = JDD.Constant(1);
+		for (JDDNode var : vars) {
+			result = JDD.And(result, JDD.Not(var.copy()));
+		}
+		return result;
+	}
+
 	/** Sort the variables in this container by their variable index. */
 	public void sortByIndex()
 	{