From 3729d85d37a1791ebd538ffccb2cf29728f17c1c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 6 Jun 2016 09:35:21 +0000 Subject: [PATCH] DebugJDD: Improve source formatting git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11389 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jdd/DebugJDD.java | 85 +++++++++++++++++++------------------ 1 file changed, 43 insertions(+), 42 deletions(-) diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java index 5eebe395..c8e16d5c 100644 --- a/prism/src/jdd/DebugJDD.java +++ b/prism/src/jdd/DebugJDD.java @@ -42,7 +42,6 @@ import prism.PrismException; import prism.PrismFileLog; import prism.PrismLog; - /** * Framework for debugging JDDNode and CUDD reference counting. *
@@ -82,6 +81,7 @@ import prism.PrismLog; public class DebugJDD { private static native int DebugJDD_GetRefCount(long dd); + private static native long[] DebugJDD_GetExternalRefCounts(); static { @@ -97,7 +97,8 @@ public class DebugJDD * A DebugJDDNode extends a JDDNode with additional information * useful for tracking refs/derefs and tracing. */ - protected static class DebugJDDNode extends JDDNode { + protected static class DebugJDDNode extends JDDNode + { /** A static counter that is used to provide a unique ID for each JDDNode */ private static long nextId = 0; @@ -186,16 +187,17 @@ public class DebugJDD 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()); + 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()); + return "0x" + Long.toHexString(ptr()); } } @@ -233,7 +235,6 @@ public class DebugJDD */ public static boolean warningsOff = false; - /** * Map from DebugJDDNode IDs to DebugJDDNode. * LinkedHashMap to ensure that iterating over the map returns the @@ -260,8 +261,8 @@ public class DebugJDD traceIDs = new HashSet(); } traceIDs.add(id); - System.out.println("DebugJDD: Enable tracing for ID "+id); - enable(); // tracing implies debugging + System.out.println("DebugJDD: Enable tracing for ID " + id); + enable(); // tracing implies debugging } /** Returns true if this node should be traced */ @@ -282,7 +283,7 @@ public class DebugJDD { 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()); + throw new RuntimeException("DebugJDD: Internal error, adding the same JDDNode multiple times, ID=" + node.getID()); } } @@ -318,16 +319,17 @@ public class DebugJDD } } - System.out.println("DdNode ptr=0x" + Long.toHexString(ptr)+", "+nodeInfo(ptr)+" has "+extRef.getValue()+" remaining external references."); + System.out.println("DdNode ptr=0x" + Long.toHexString(ptr) + + ", " + nodeInfo(ptr) + " has " + extRef.getValue() + " remaining external references."); if (posRewNodes.size() > 0) { System.out.println(" Candidates:"); for (DebugJDDNode node : posRewNodes) { - System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references (" + node.toStringVerbose() + ")"); + 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 (" + node.toStringVerbose() + ")"); + System.out.println(" ID=" + node.getID() + " with " + node.getNodeRefs() + " references (" + node.toStringVerbose() + ")"); } } } @@ -337,21 +339,24 @@ public class DebugJDD javaRefs.clear(); // reset ID counter DebugJDDNode.nextId = 0; - + if (warningsAreFatal) { throw new RuntimeException("DebugJDD: Leaked references"); } } /** Get the CUDD reference count for the pointer of the JDDNode */ - public static int getRefCount(JDDNode n) { + public static int getRefCount(JDDNode n) + { return DebugJDD_GetRefCount(n.ptr()); } /** Get the number of DebugJDDNodes that reference the pointer */ - public static int getJavaRefCount(long ptr) { + public static int getJavaRefCount(long ptr) + { Integer jrefs = javaRefs.get(ptr); - if (jrefs == null) return 0; + if (jrefs == null) + return 0; return jrefs; } @@ -361,10 +366,10 @@ public class DebugJDD Map result = new TreeMap(); // Array consists of (pointer, count) pairs long[] externalRefCounts = DebugJDD_GetExternalRefCounts(); - int i=0; - while (i " + dNode.getNodeRefs() + " refs for this JDDNode\n " + dNode.toStringVerbose()); + System.out.println("\ntrace(" + action + + ", ID=" + dNode.getID() + ") => " + dNode.getNodeRefs() + + " refs for this JDDNode\n " + dNode.toStringVerbose()); printStack(0); } @@ -518,7 +525,7 @@ public class DebugJDD JDD.DD_Ref(result.ptr()); if (isTraced(dNode)) { - trace("Copy to "+result.getID(), dNode); + trace("Copy to " + result.getID(), dNode); } if (!traceAll && traceFollowCopies && isTraced(dNode)) { @@ -528,7 +535,7 @@ public class DebugJDD } if (isTraced(result)) { - trace("Copied from " +dNode.getID(), result); + trace("Copied from " + dNode.getID(), result); } return result; @@ -661,7 +668,7 @@ public class DebugJDD JDD.Deref(t); vars.derefAll(); } - + private static void usage() { System.out.println("\nUsage: PRISM_MAINCLASS=jdd.DebugJDD prism [arguments] [test cases]"); @@ -676,7 +683,7 @@ public class DebugJDD System.out.println(" -ddtrace n Trace JDDNode with ID=n"); System.out.println("\nFor the test cases, look at the source code in jdd/DebugJDD.java"); } - + private static void errorAndExit(String error) { System.out.println(error); @@ -710,20 +717,15 @@ public class DebugJDD // DD Debugging options if (sw.equals("dddebug")) { jdd.DebugJDD.enable(); - } - else if (sw.equals("ddtraceall")) { + } else if (sw.equals("ddtraceall")) { jdd.DebugJDD.traceAll = true; - } - else if (sw.equals("ddtracefollowcopies")) { + } else if (sw.equals("ddtracefollowcopies")) { jdd.DebugJDD.traceFollowCopies = true; - } - else if (sw.equals("dddebugwarnfatal")) { + } else if (sw.equals("dddebugwarnfatal")) { jdd.DebugJDD.warningsAreFatal = true; - } - else if (sw.equals("dddebugwarnoff")) { + } else if (sw.equals("dddebugwarnoff")) { jdd.DebugJDD.warningsOff = true; - } - else if (sw.equals("ddtrace")) { + } else if (sw.equals("ddtrace")) { if (i < args.length - 1) { String idString = args[++i]; try { @@ -735,8 +737,7 @@ public class DebugJDD } else { errorAndExit("The -" + sw + " switch requires an additional argument (JDDNode ID)"); } - } - else { + } else { errorAndExit("Unknown switch: -" + sw); } } else { @@ -788,7 +789,7 @@ public class DebugJDD } mainLog.println("\n[Closing down PRISM/CUDD]\n"); - + // clear up and close down prism.closeDown(true);