From 861883963c87c69298876d6cb018a573f7a80ed3 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 30 May 2016 09:25:39 +0000 Subject: [PATCH] DebugJDD: Improved ref count debugging for JDD, new options This is an improved version of the DebugJDD functionality, allowing the debugging of the reference counting for JDDNodes. DebugJDD now closely tracks the various "events" for a JDDNode, i.e., referencing (JDD.Ref), dereferencing (JDD.Deref), returning a pointer from DD_* methods (JDD.ptrToNode), copying (JDDNode.copy) and using of a node as a DD_* method argument. This finer-grained tracking allows to catch some more situations and provide better diagnostics than the previous version. Additional command-line options are: -ddtraceall: Trace all JDDNode IDs -ddtracefollowcopies: Automatically trace all JDDNode IDs that result from a copy of a traced node -dddebugwarnfatal: Treat warnings as errors -dddebugwarnoff: Turn of warnings git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11374 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/DebugJDD.java | 374 +++++++++++++++++++++++++++++------ prism/src/jdd/JDD.java | 99 +++++----- prism/src/jdd/JDDNode.java | 9 +- prism/src/prism/PrismCL.java | 14 ++ 4 files changed, 383 insertions(+), 113 deletions(-) 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];