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
Parsing a HOA automaton, if a state has an acceptance signature that
contains an acceptance set that is not actually referenced in the
acceptance condition, we simply skip these entries, as they are not
relevant for acceptance.
This commit fixes the handling for this situation:
Acceptance: 2 Inf(0)
...
State: 1 {1}
I.e., when the acceptance set index is valid but larger than the
largest used one. Previously, would throw an IndexOutOfBoundsException
trying to access a non-existant set.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11218 bbc10eb1-c90d-0410-af57-cb519fbb1720
The compilation wrapper 'ccc' of lpsolve tries to determine
whether the isnan macro is defined. The test program calls
isnan(0), i.e., with an integer argument. On current Arch Linux,
GCC uses _builtin_isnan, which leads to an error due to the integer
argument and the 'ccc' wrapper assumes that isnan is not defined.
This leads to compilation issues later on.
The fix replaces the isnan(0) test call with isnan(0.0).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11216 bbc10eb1-c90d-0410-af57-cb519fbb1720
When translating the module state variables to locations, probabilities in
commands were not translated. If the probability expression contains a reference
to the state variables, e.g.,
(s=0 ? 0.5 : 0.75)
then the variable reference persists, which leads to an exception when
updating variable information of the module later on, as the state variable
is no longer defined in the translated module.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11215 bbc10eb1-c90d-0410-af57-cb519fbb1720
Add handling for ExpressionITE to Simplify.
Incidentally, this fixes a bug in PTA handling, where guards with an
ITE operation where not properly simplified and thus unsupported, e.g.,
s=0 ? true : false
as guard.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11214 bbc10eb1-c90d-0410-af57-cb519fbb1720
The routines in LTL2RabinLibrary for generating DA for
simple path formulas with time bounds have been adapted
to deal with negated labels. This makes the special
preprocessing for such formulas unnecessary and we remove it.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11199 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein