diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java index 1f8c9c28..3ff7f3d5 100644 --- a/prism/src/jdd/DebugJDD.java +++ b/prism/src/jdd/DebugJDD.java @@ -37,6 +37,43 @@ import java.util.Map; import java.util.Map.Entry; import java.util.TreeMap; + +/** + * Framework for debugging JDDNode and CUDD reference counting. + *
+ * If DebugJDD is enabled (via calling DebugJDD.enabled()), + * instead of normal JDDNodes, DebugJDDNodes are used. These + * track the balance of referencing and dereferencing, etc and + * throw errors or provide warnings if something problematic + * occurs. + *
+ * In addition, each DebugJDDNode carries a unique ID, which + * is persistent over multiple invocations of PRISM, in contrast + * to the DdNode pointers of CUDD, which are raw C/C++ pointers + * and can differ between multiple PRISM runs, making tracking + * more difficult. + *
+ * You can enable tracing for a particular ID, which will print + * status messages for each event for this particular JDDNode, + * e.g., whenever the node is referenced, dereferenced, consumed + * in a JDD method, copied, etc. + *
+ * In the end, if there are reference leaks, a list of potential + * JDDNode IDs is printed. These can then be used for tracing + * the referencing and dereferencing of these nodes in a subsequent + * run of PRISM to debug the reference leak. + *
+ * Note: For the JDDNodes that are returned by JDDNode.getThen() and + * JDDNode.getElse(), a different handling applies. As these are + * generally only used for traversing an MTBDD and are not referenced + * (beyond the internal CUDD references that are there due to the + * fact that they are internal nodes of some MTBDD), they are not + * wrapped in a DebugJDDNode. They are not fully functional and + * should never be used for JDD.Ref, JDD.Deref, JDDNode.copy() or + * as the argument of a JDD method, except to compare for equality, + * getting the variable index, getThen() and getElse() and obtaining + * constant value of a terminal node. + */ public class DebugJDD { private static native int DebugJDD_GetRefCount(long dd); @@ -61,16 +98,22 @@ public class DebugJDD private static long nextId = 0; /** - * The ID for this JDDNode. In contrast with the DdNode* ptr, this will be - * stable across PRISM invocations and can thus be used for tracing. + * The ID for this JDDNode. In contrast with the CUDD DdNode* ptr, + * this will be stable across PRISM invocations and can thus be + * used for tracing. */ private long id; - /** The balance of reference/dereference calls this specific JDDNode */ + /** + * The balance of reference and dereference calls for + * this specific JDDNode object. + */ private int nodeRefs = 0; /** * Constructor, with DdNode* ptr. + *
+ * Registers the node with the DebugJDD infrastructure. * @param ptr the DdNode pointer in CUDD * @param isReferenced Does this JDDNode already have a reference * (like for ptrToNode) or not (like for getThen / getElse) @@ -82,11 +125,9 @@ public class DebugJDD // generate and store globally unique ID id = nextId++; // the initial number of references for this JDDNode - nodeRefs = (isReferenced ? 1 : 0); + nodeRefs = 0; if (isReferenced) { - // increase javaRefs counter for this ptr - int jrefs = getJavaRefCount(ptr()); - javaRefs.put(ptr(), jrefs+1); + incRef(); } // store to keep track of this DebugJDDNode DebugJDD.addToSet(this); @@ -98,7 +139,7 @@ public class DebugJDD return id; } - /** Increment the reference count for this JDDNode */ + /** Increment the reference count for this DebugJDDNode */ public void incRef() { // increment count for node @@ -108,7 +149,7 @@ public class DebugJDD javaRefs.put(ptr(), jrefs + 1); } - /** Decrement the reference count for this JDDNode */ + /** Decrement the reference count for this DebugJDDNode */ public void decRef() { // decrement count for node @@ -120,15 +161,15 @@ public class DebugJDD // Checks: // (1) There is a negative number of Java references for the DdNode pointer if (jrefs < 0) { - throw new RuntimeException("DebugJDD: The number of Java references is negative for ptr=0x"+Long.toHexString(ptr())+", ID="+getID()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr())); + throw new RuntimeException("DebugJDD: The number of Java references is negative for\n " + toStringVerbose()); } - // (2) There are more Java references than Cudd references + // (2) There are more Java references than CUDD references if (jrefs > DebugJDD_GetRefCount(ptr())) { - throw new RuntimeException("DebugJDD: More Java refs than CUDD refs for ptr=0x"+Long.toHexString(ptr())+", ID="+getID()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr())); + throw new RuntimeException("DebugJDD: More Java refs than CUDD refs for\n " + toStringVerbose()); } // (3) This node has more refs than there are Java refs in total if (jrefs < getNodeRefs()) { - throw new RuntimeException("DebugJDD: JDDNode has more refs than Java refs in total?! ID="+getID()+", refs = "+getNodeRefs()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr())); + throw new RuntimeException("DebugJDD: JDDNode has more refs than Java refs in total?!\n " + toStringVerbose()); } } @@ -137,13 +178,57 @@ public class DebugJDD { return nodeRefs; } + + public String toStringVerbose() + { + return "ID = " + getID() + + ", CUDD ptr = " + ptrAsHex() + + ", refs for this JDDNode = " + getNodeRefs() + + ", refs from Java = " + getJavaRefCount(ptr()) + + ", refs from CUDD (including internal MTBDD refs) = "+DebugJDD_GetRefCount(ptr()); + } + + public String ptrAsHex() + { + return "0x"+Long.toHexString(ptr()); + } } + /* ----- Settings ------ */ + /** * Flag, determines if the debugging of JDD nodes is enabled. + * Default off. */ public static boolean debugEnabled = false; + /** + * Flag, determines if all nodes should be traced (in contrast to only those + * specified using enableTracingForID(). + * Default off. + */ + public static boolean traceAll = false; + + /** + * Flag, determines if copies of traced nodes should be traced as well. + * Default off. + */ + public static boolean traceFollowCopies = false; + + /** + * Flag, determines if warnings should be promoted to + * errors, i.e., throwing an exception. + * Default off. + */ + public static boolean warningsAreFatal = false; + + /** + * Flag, determines if warnings should be suppressed. + * Default off. + */ + public static boolean warningsOff = false; + + /** * Map from DebugJDDNode IDs to DebugJDDNode. * LinkedHashMap to ensure that iterating over the map returns the @@ -162,67 +247,46 @@ public class DebugJDD { debugEnabled = true; } + /** Activate tracing for the DebugJDDNode with ID id */ - public static void enableTracingForID(long id) { + public static void enableTracingForID(long id) + { if (traceIDs == null) { traceIDs = new HashSet(); } traceIDs.add(id); - System.out.println("DebugJDD: Enable tracing for "+id); + System.out.println("DebugJDD: Enable tracing for ID "+id); enable(); // tracing implies debugging } - /** Store a DebugJDDNode for tracking of the references */ - protected static void addToSet(DebugJDDNode node) - { - if (nodes.put(node.getID(), node) != null) { - // implementation error, should not happen - throw new RuntimeException("DebugJDD: Adding the same JDDNode multiple times, ID="+node.getID()); - } - if (traceIDs != null && traceIDs.contains(node.id)) { - trace("create", node); - } - } - /** Notification from JDD.Deref(node) */ - protected static void decrement(JDDNode node) + /** Returns true if this node should be traced */ + private static boolean isTraced(DebugJDDNode dNode) { - if (!(node instanceof DebugJDDNode)) { - // deref of a node that is not wrapped in a DebugJDDNode - // -> probably came from JDDNode.getThen()/getElse(), should not be derefed - throw new RuntimeException("DebugJDD: Trying to Deref a plain JDDNode (obtained from getThen()/getElse()?)"); + if (traceAll) { + return true; } - DebugJDDNode dNode = (DebugJDDNode) node; - if (dNode.getNodeRefs() == 0) { - // This is only a warning as currently there are places - // where referencing / derefencing happens across multiple JDDNodes - System.out.println("Warning, DebugJDD: Deref of a JDDNode that has 0 references, ID = "+dNode.getID()); - printStack(0); - } - dNode.decRef(); - int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); - if (cuddRefCount <= 0) { - throw new RuntimeException("DebugJDD: Trying to deref a JDDNode with a non-positive CUDD ref count, ptr=0x"+Long.toHexString(dNode.ptr())+", ID = "+dNode.getID()+", Java ref = "+getJavaRefCount(dNode.ptr())+", CUDD refs = "+cuddRefCount); - } - if (traceIDs != null && traceIDs.contains(dNode.id)) { - trace("deref", dNode); + + if (traceIDs != null && traceIDs.contains(dNode.getID())) { + return true; } + return false; } - /** Notification from JDD.Ref(node) */ - protected static void increment(JDDNode node) + /** Store a DebugJDDNode for tracking of the references */ + private static void addToSet(DebugJDDNode node) { - if (!(node instanceof DebugJDDNode)) { - // ref of a node that is not wrapped in a DebugJDDNode - // -> probably came from JDDNode.getThen()/getElse(), should not be refed - throw new RuntimeException("DebugJDD: Trying to Ref a plain JDDNode (obtained from getThen()/getElse()?)"); - } - DebugJDDNode dNode = (DebugJDDNode) node; - dNode.incRef(); - if (traceIDs != null && traceIDs.contains(dNode.id)) { - trace("ref", dNode); + if (nodes.put(node.getID(), node) != null) { + // implementation error, should not happen + throw new RuntimeException("DebugJDD: Internal error, adding the same JDDNode multiple times, ID="+node.getID()); } } + /** + * Called when CUDD is shutdown. + *
+ * Analyzes the reference counting situation + * and prints diagnostics in case of a leak. + */ public static void endLifeCycle() { // Get the external reference count from CUDD @@ -253,15 +317,20 @@ public class DebugJDD if (posRewNodes.size() > 0) { System.out.println(" Candidates:"); for (DebugJDDNode node : posRewNodes) { - System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references"); + System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references (" + node.toStringVerbose() + ")"); } } else { System.out.println(" No candidates, here are all JDDNodes for that DdNode:"); for (DebugJDDNode node : matchingNodes) { - System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references"); + System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references (" + node.toStringVerbose() + ")"); } } } + + if (warningsAreFatal) { + throw new RuntimeException("DebugJDD: Leaked references"); + } + } /** Get the CUDD reference count for the pointer of the JDDNode */ @@ -270,7 +339,7 @@ public class DebugJDD } /** Get the number of DebugJDDNodes that reference the pointer */ - private static int getJavaRefCount(long ptr) { + public static int getJavaRefCount(long ptr) { Integer jrefs = javaRefs.get(ptr); if (jrefs == null) return 0; return jrefs; @@ -306,7 +375,7 @@ public class DebugJDD /** Log information about the action performed on the DebugJDDNode */ private static void trace(String action, DebugJDDNode dNode) { - System.out.println("\ntrace("+action+",ID="+dNode.getID()+") = "+dNode.getNodeRefs()+" refs (total = "+DebugJDD_GetRefCount(dNode.ptr())+", local="+javaRefs.get(dNode.ptr())+")"); + System.out.println("\ntrace("+action+", ID="+dNode.getID()+") => " + dNode.getNodeRefs() + " refs for this JDDNode\n " + dNode.toStringVerbose()); printStack(0); } @@ -341,4 +410,187 @@ public class DebugJDD System.out.flush(); } + /** + * DebugJDD implementation of JDD.Ref. + *
+ * Increments both the CUDD reference counter and the reference counter for the JDDNode. + */ + protected static void Ref(JDDNode node) + { + if (!(node instanceof DebugJDDNode)) { + // ref of a node that is not wrapped in a DebugJDDNode + // -> probably came from JDDNode.getThen()/getElse(), should not be refed + throw new RuntimeException("DebugJDD: Illegal operation, trying to Ref a plain JDDNode (obtained from getThen()/getElse()?)"); + } + DebugJDDNode dNode = (DebugJDDNode) node; + + // increment reference in DebugJDD + dNode.incRef(); + // increment reference in CUDD + JDD.DD_Ref(node.ptr()); + + if (isTraced(dNode)) { + trace("Ref", dNode); + } + } + + /** + * DebugJDD implementation of JDD.Deref. + *
+ * Decrements both the CUDD reference counter and the reference counter for the JDDNode, + * performing a variety of sanity checks. + */ + protected static void Deref(JDDNode node) + { + if (!(node instanceof DebugJDDNode)) { + // deref of a node that is not wrapped in a DebugJDDNode + // -> probably came from JDDNode.getThen()/getElse(), should not be derefed + throw new RuntimeException("DebugJDD: Illegal operation, trying to Deref a plain JDDNode (obtained from getThen()/getElse()?)"); + } + DebugJDDNode dNode = (DebugJDDNode) node; + if (dNode.getNodeRefs() <= 0 && getJavaRefCount(node.ptr()) > 0) { + // This is only a warning as currently there are places + // where referencing / dereferencing happens across multiple JDDNodes, + // which is not pretty but not necessarily problematic, as long as + // the total number of references from Java remains positive + String warning = "DebugJDD: Deref of a JDDNode with non-positive ref count:\n " + dNode.toStringVerbose(); + if (!warningsOff && !warningsAreFatal) { + System.out.println("Warning, " + warning); + printStack(0); + } else if (!warningsOff && warningsAreFatal) { + throw new RuntimeException(warning); + } + } + + if (getJavaRefCount(node.ptr()) <= 0) { + throw new RuntimeException("DebugJDD: Trying to Deref a JDDNode with non-positive Java ref count:\n " + dNode.toStringVerbose()); + } + + int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); + if (cuddRefCount <= 0) { + throw new RuntimeException("DebugJDD: Trying to Deref a JDDNode with a non-positive CUDD ref count\n " + dNode.toStringVerbose()); + } + + // decrement reference in DebugJDD + dNode.decRef(); + // decrement reference in CUDD + JDD.DD_Deref(node.ptr()); + + if (isTraced(dNode)) { + trace("Deref", dNode); + } + } + + /** + * DebugJDD implementation of JDDNode.copy(). + *
+ * Increments the reference count for the copy and handles tracing. + */ + protected static JDDNode Copy(JDDNode node) + { + if (!(node instanceof DebugJDDNode)) { + // copy of a node that is not wrapped in a DebugJDDNode + // -> probably came from JDDNode.getThen()/getElse(), should not be copied + throw new RuntimeException("DebugJDD: Illegal operation, trying to copy a plain JDDNode (obtained from getThen()/getElse()?)"); + } + + DebugJDDNode dNode = (DebugJDDNode) node; + + if (dNode.getNodeRefs() <= 0) { + throw new RuntimeException("DebugJDD: Trying to copy a JDDNode with non-positive ref count:\n " + dNode.toStringVerbose()); + } + + if (getRefCount(dNode) <= 0) { + throw new RuntimeException("DebugJDD: Trying to copy a JDDNode with non-positive CUDD ref count:\n " + dNode.toStringVerbose()); + } + + DebugJDDNode result = new DebugJDD.DebugJDDNode(dNode.ptr(), false); + JDD.Ref(result); + + if (isTraced(dNode)) { + trace("Copy to "+result.getID(), dNode); + } + + if (!traceAll && traceFollowCopies && isTraced(dNode)) { + // if we are not tracing everything anyway and we should follow copies: + // enable tracing for the copy if the original node is traced + enableTracingForID(result.getID()); + } + + if (isTraced(result)) { + trace("Copied", result); + } + + return result; + } + + /** + * DebugJDD implementation of JDD.ptrToNode, i.e., + * converting a (referenced) DdNode ptr returned by + * the DD_* CUDD abstraction layer into a proper JDDNode. + */ + protected static JDDNode ptrToNode(long ptr) + { + DebugJDDNode dNode = new DebugJDD.DebugJDDNode(ptr, true); + + if (isTraced(dNode)) { + trace("ptrToNode", dNode); + } + + return dNode; + } + + /** + * DebugJDD handling of passing JDDNodes as arguments to the + * DD_* layer, where they will be ultimately dereferenced. + *
+ * As the actual dereferencing in CUDD will only happen + * after the given MTBDD method is finished, we only + * decrement the reference counter on the DebugJDD side. + */ + protected static void DD_Method_Argument(JDDNode node) + { + if (!(node instanceof DebugJDDNode)) { + // using a node that is not wrapped in a DebugJDDNode in a DD_* method call + // -> probably came from JDDNode.getThen()/getElse(), should not be used like this + throw new RuntimeException("DebugJDD: Illegal operation, trying to use a plain JDDNode (obtained from getThen()/getElse()?) in a method call"); + } + + DebugJDDNode dNode = (DebugJDDNode) node; + if (dNode.getNodeRefs() <= 0 && getJavaRefCount(node.ptr()) > 0) { + // This is only a warning as currently there are places + // where referencing / dereferencing happens across multiple JDDNodes, + // which is not pretty but not necessarily problematic, as long as + // the total number of references from Java remains positive + String warning = "DebugJDD: Trying to use a JDDNode with non-positive ref count:\n " + dNode.toStringVerbose(); + if (!warningsOff && !warningsAreFatal) { + System.out.println("Warning, " + warning); + printStack(0); + } else if (!warningsOff && warningsAreFatal) { + throw new RuntimeException(warning); + } + } + + if (getJavaRefCount(node.ptr()) <= 0) { + throw new RuntimeException("DebugJDD: Trying to use a JDDNode with non-positive Java ref count in a method call:\n " + dNode.toStringVerbose()); + } + + int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); + if (cuddRefCount <= 0) { + throw new RuntimeException("DebugJDD: Trying to use a JDDNode with a non-positive CUDD ref count in a method call:\n " + dNode.toStringVerbose()); + } + + // decrement reference in DebugJDD + dNode.decRef(); + // ... but don't dereference in CUDD yet. This will + // be done in the DD_* methods after the actual + // processing has happened and the result is referenced, + // as then this argument does not have to be protected + // anymore + + if (isTraced(dNode)) { + trace("Deref (as method argument)", dNode); + } + } + } diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index b9c444d4..7fea7a34 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -274,9 +274,11 @@ public class JDD if (ptr == 0) { throw new CuddOutOfMemoryException(); } - if (DebugJDD.debugEnabled) - DebugJDD.increment(dd); - DD_Ref(ptr); + if (DebugJDD.debugEnabled) { + DebugJDD.Ref(dd); + } else { + DD_Ref(ptr); + } } /** @@ -293,9 +295,11 @@ public class JDD if (ptr == 0) { throw new CuddOutOfMemoryException(); } - if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); - DD_Deref(ptr); + if (DebugJDD.debugEnabled) { + DebugJDD.Deref(dd); + } else { + DD_Deref(ptr); + } } /** @@ -376,7 +380,7 @@ public class JDD public static JDDNode Not(JDDNode dd) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_Not(dd.ptr())); } @@ -387,8 +391,8 @@ public class JDD public static JDDNode Or(JDDNode dd1, JDDNode dd2) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); } return ptrToNode(DD_Or(dd1.ptr(), dd2.ptr())); } @@ -424,8 +428,8 @@ public class JDD public static JDDNode And(JDDNode dd1, JDDNode dd2) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); } return ptrToNode(DD_And(dd1.ptr(), dd2.ptr())); @@ -462,8 +466,8 @@ public class JDD public static JDDNode Xor(JDDNode dd1, JDDNode dd2) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); } return ptrToNode(DD_Xor(dd1.ptr(), dd2.ptr())); } @@ -475,8 +479,8 @@ public class JDD public static JDDNode Implies(JDDNode dd1, JDDNode dd2) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); } return ptrToNode(DD_Implies(dd1.ptr(), dd2.ptr())); } @@ -497,8 +501,8 @@ public class JDD public static JDDNode Apply(int op, JDDNode dd1, JDDNode dd2) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); } return ptrToNode(DD_Apply(op, dd1.ptr(), dd2.ptr())); } @@ -566,7 +570,7 @@ public class JDD public static JDDNode MonadicApply(int op, JDDNode dd) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_MonadicApply(op, dd.ptr())); } @@ -577,8 +581,8 @@ public class JDD public static JDDNode Restrict(JDDNode dd, JDDNode cube) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd); - DebugJDD.decrement(cube); + DebugJDD.DD_Method_Argument(dd); + DebugJDD.DD_Method_Argument(cube); } return ptrToNode(DD_Restrict(dd.ptr(), cube.ptr())); } @@ -590,9 +594,9 @@ public class JDD public static JDDNode ITE(JDDNode dd1, JDDNode dd2, JDDNode dd3) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); - DebugJDD.decrement(dd3); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); + DebugJDD.DD_Method_Argument(dd3); } return ptrToNode(DD_ITE(dd1.ptr(), dd2.ptr(), dd3.ptr())); } @@ -640,7 +644,7 @@ public class JDD public static JDDNode PermuteVariables(JDDNode dd, JDDVars old_vars, JDDVars new_vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_PermuteVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n())); } @@ -651,7 +655,7 @@ public class JDD public static JDDNode SwapVariables(JDDNode dd, JDDVars old_vars, JDDVars new_vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_SwapVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n())); } @@ -709,7 +713,7 @@ public class JDD public static JDDNode ThereExists(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_ThereExists(dd.ptr(), vars.array(), vars.n())); } @@ -720,7 +724,7 @@ public class JDD public static JDDNode ForAll(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_ForAll(dd.ptr(), vars.array(), vars.n())); } @@ -731,7 +735,7 @@ public class JDD public static JDDNode SumAbstract(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_SumAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -742,7 +746,7 @@ public class JDD public static JDDNode ProductAbstract(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_ProductAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -753,7 +757,7 @@ public class JDD public static JDDNode MinAbstract(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_MinAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -764,7 +768,7 @@ public class JDD public static JDDNode MaxAbstract(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_MaxAbstract(dd.ptr(), vars.array(), vars.n())); } @@ -777,7 +781,7 @@ public class JDD public static JDDNode GreaterThan(JDDNode dd, double threshold) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_GreaterThan(dd.ptr(), threshold)); } @@ -788,7 +792,7 @@ public class JDD public static JDDNode GreaterThanEquals(JDDNode dd, double threshold) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_GreaterThanEquals(dd.ptr(), threshold)); } @@ -799,7 +803,7 @@ public class JDD public static JDDNode LessThan(JDDNode dd, double threshold) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_LessThan(dd.ptr(), threshold)); } @@ -810,7 +814,7 @@ public class JDD public static JDDNode LessThanEquals(JDDNode dd, double threshold) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_LessThanEquals(dd.ptr(), threshold)); } @@ -821,7 +825,7 @@ public class JDD public static JDDNode Equals(JDDNode dd, double value) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_Equals(dd.ptr(), value)); } @@ -832,7 +836,7 @@ public class JDD public static JDDNode Interval(JDDNode dd, double lower, double upper) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_Interval(dd.ptr(), lower, upper)); } @@ -843,7 +847,7 @@ public class JDD public static JDDNode RoundOff(JDDNode dd, int places) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_RoundOff(dd.ptr(), places)); } @@ -887,7 +891,7 @@ public class JDD public static JDDNode RestrictToFirst(JDDNode dd, JDDVars vars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_RestrictToFirst(dd.ptr(), vars.array(), vars.n())); } @@ -1154,7 +1158,7 @@ public class JDD public static JDDNode SetVectorElement(JDDNode dd, JDDVars vars, long index, double value) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_SetVectorElement(dd.ptr(), vars.array(), vars.n(), index, value)); } @@ -1165,7 +1169,7 @@ public class JDD public static JDDNode SetMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, long rindex, long cindex, double value) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_SetMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), rindex, cindex, value)); } @@ -1176,7 +1180,7 @@ public class JDD public static JDDNode Set3DMatrixElement(JDDNode dd, JDDVars rvars, JDDVars cvars, JDDVars lvars, long rindex, long cindex, long lindex, double value) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_Set3DMatrixElement(dd.ptr(), rvars.array(), rvars.n(), cvars.array(), cvars.n(), lvars.array(), lvars.n(), rindex, cindex, lindex, value)); } @@ -1207,7 +1211,7 @@ public class JDD public static JDDNode Transpose(JDDNode dd, JDDVars rvars, JDDVars cvars) { if (DebugJDD.debugEnabled) - DebugJDD.decrement(dd); + DebugJDD.DD_Method_Argument(dd); return ptrToNode(DD_Transpose(dd.ptr(), rvars.array(), cvars.array(), rvars.n())); } @@ -1218,8 +1222,8 @@ public class JDD public static JDDNode MatrixMultiply(JDDNode dd1, JDDNode dd2, JDDVars vars, int method) { if (DebugJDD.debugEnabled) { - DebugJDD.decrement(dd1); - DebugJDD.decrement(dd2); + DebugJDD.DD_Method_Argument(dd1); + DebugJDD.DD_Method_Argument(dd2); } return ptrToNode(DD_MatrixMultiply(dd1.ptr(), dd2.ptr(), vars.array(), vars.n(), method)); } @@ -1553,9 +1557,10 @@ public class JDD throw new CuddOutOfMemoryException(); } if (DebugJDD.debugEnabled) { - return new DebugJDD.DebugJDDNode(ptr, true); + return DebugJDD.ptrToNode(ptr); + } else { + return new JDDNode(ptr); } - return new JDDNode(ptr); } /** diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java index 3d48d4bd..1c3583ac 100644 --- a/prism/src/jdd/JDDNode.java +++ b/prism/src/jdd/JDDNode.java @@ -141,14 +141,13 @@ public class JDDNode */ public JDDNode copy() { - JDDNode result; if (DebugJDD.debugEnabled) { - result = new DebugJDD.DebugJDDNode(ptr, false); + return DebugJDD.Copy(this); } else { - result = new JDDNode(ptr()); + JDDNode result = new JDDNode(ptr()); + JDD.Ref(result); + return result; } - JDD.Ref(result); - return result; } } diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index c4ae4b20..589ce6a7 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1127,9 +1127,23 @@ public class PrismCL implements PrismModelListener test = true; testExitsOnFail = false; } + + // DD Debugging options else if (sw.equals("dddebug")) { jdd.DebugJDD.enable(); } + else if (sw.equals("ddtraceall")) { + jdd.DebugJDD.traceAll = true; + } + else if (sw.equals("ddtracefollowcopies")) { + jdd.DebugJDD.traceFollowCopies = true; + } + else if (sw.equals("dddebugwarnfatal")) { + jdd.DebugJDD.warningsAreFatal = true; + } + else if (sw.equals("dddebugwarnoff")) { + jdd.DebugJDD.warningsOff = true; + } else if (sw.equals("ddtrace")) { if (i < args.length - 1) { String idString = args[++i];