s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Joachim Klein 10 years ago
parent
b2e4a120be
commit
861883963c
4 changed files with 383 additions and 113 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 374
      prism/src/jdd/DebugJDD.java
  2. 99
      prism/src/jdd/JDD.java
  3. 9
      prism/src/jdd/JDDNode.java
  4. 14
      prism/src/prism/PrismCL.java

374
prism/src/jdd/DebugJDD.java
View File

@ -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.
* <br>
* 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.
* <br>
* 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.
* <br>
* 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.
* <br>
* 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.
* <br>
* 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.
* <br>
* 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<Long>();
}
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.
* <br>
* 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.
* <br>
* 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.
* <br>
* 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().
* <br>
* 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.
* <br>
* 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);
}
}
}

99
prism/src/jdd/JDD.java
View File

@ -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);
}
/**

9
prism/src/jdd/JDDNode.java
View File

@ -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;
}
}

14
prism/src/prism/PrismCL.java
View File

@ -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];

Write Preview
Loading…
Cancel
Save