From 4d672db58b39bf36a4a18f04027fc0cdff63516a Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:24:51 +0200
Subject: [PATCH] PrismSparse.exportMDP: sanity check

---
 prism/src/sparse/PrismSparse.java | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java
index 41429007..74937210 100644
--- a/prism/src/sparse/PrismSparse.java
+++ b/prism/src/sparse/PrismSparse.java
@@ -32,6 +32,7 @@ import java.util.List;
 import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
+import jdd.SanityJDD;
 import odd.ODDNode;
 import prism.NativeIntArray;
 import prism.OpsAndBoundsList;
@@ -600,6 +601,9 @@ public class PrismSparse
 	public static void ExportMDP(JDDNode mdp, JDDNode transActions, List<String> synchs, String name, JDDVars rows, JDDVars cols, JDDVars nondet, ODDNode odd, int exportType, String filename) throws FileNotFoundException, PrismException
 	{
 		checkNumStates(odd);
+		if (SanityJDD.enabled) {
+			SanityJDD.checkIsDDOverVars(mdp, rows, cols, nondet);
+		}
 
 		int res = PS_ExportMDP(mdp.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, name, rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), odd.ptr(), exportType, filename);
 		if (res == -1) {