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
Currently, properties that contain an undefined property constant are not displayed.
In the future it might be nice for the user to be asked to specify these constants,
preferably in an unobstrusive way, so that these path formulae can be displayed and
evaluated as well.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11444 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
Previously, a derefed JDDNode would be used (not necessarily
problematic, as the reference lived on a another node). Fixes a
warning by DebugJDD.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11376 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
When a path is loaded in the simulator view of the GUI, selecting any step
but the last step can produce erroneous display of the update in the
"Manual exploration" field. The problem is that the updates are computed for
display relative to the variables values of the last state of the whole path
instead of relative to the state where the step originates.
This fix keeps the information about the correct state available for computing
the update display. This was a regression, introduced in SVN 10939 and should only
affect the GUI display, not computations.
To reproduce, use e.g.:
dtmc
module one
x: [0..3] init 0;
[] true -> (x' = min(3, x+1));
endmodule
Simulate for a few steps. The update information for the non-last steps of the path will
display incorrect values. This also occurs for display of CTL counterexamples.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11281 bbc10eb1-c90d-0410-af57-cb519fbb1720
For the non-fair case, the restriction is indeed done
by the ECComputer, but for the fair case, the restriction
of candidateStates to states_Li_not is required.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11243 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein