For production code, only call the SanityJDD methods if SanityJDD.enabled is true.
While developing, it makes sense to call SanityJDD checks without having to globally
enable sanity checks.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11456 bbc10eb1-c90d-0410-af57-cb519fbb1720
The order of the content of the prism/include/DebugJDD.h header (auto-generated
by javah) sometimes changes nondeterministically. This seems to be due to the
combination of JNI methods and internal classes in DebugJDD.
We move the two DebugJDD JNI methods to JDD instead and remove the
prism/include/DebugJDD.h header, as well as the generation in the Makefile.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11455 bbc10eb1-c90d-0410-af57-cb519fbb1720
When debugging is enabled, wrap the return of getThen() and getElse()
in "light-weight" DebugJDDNodes.
Allow copy() on such light-weight nodes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11393 bbc10eb1-c90d-0410-af57-cb519fbb1720
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
The DebugJDD class provides Java-side reference counting for
JDDNodes and tries to detect problems with the reference counting,
such as to many derefs (can lead to crashes during garbage collection)
or too few derefs (leads to memory leakage and a warning when exiting
PRISM).
When debugging is enabled, each JDDNode is assigned a unique, sequential
ID that should be stable across runs of PRISM with the same command-line
arguments, in contrast to the underlying CUDD DDNode pointers, which can
and do change with each invokation.
A tracing mechanism allows to print all the ref/deref events for a particular
JDDNode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10506 bbc10eb1-c90d-0410-af57-cb519fbb1720
Analyze the BDD and return the implied number of external references per node
in a map (node -> count). Only return nodes with non-zero external references.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10505 bbc10eb1-c90d-0410-af57-cb519fbb1720
For DD functions that return a DdNode*, errors can be reported by returning NULL.
Functions that have no return value (printing, etc) or a data value (double, etc)
should set the flag, which can be converted into an CuddOutOfMemoryException on
the PRISM side using JDD.checkForCuddError()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10474 bbc10eb1-c90d-0410-af57-cb519fbb1720
Normally, we should catch the construction of JDDNodes with NULL pointers
beforehand, but for robustness we make sure that we do not call Cudd_Ref
and Cudd_Deref for a NULL DdNode*, as that leads to SIGSEGV crashes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10473 bbc10eb1-c90d-0410-af57-cb519fbb1720
The native DD/CuDD methods return NULL to indicate that
an out-of-memory error in CuDD has occurred. Before, we
constructed a JDDNode for this NULL ptr, which would lead
to a SIGSEGV crash the next time any operation
(ref, deref, etc) would be performed on that JDDNode.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10472 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein