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
Without formula simplifications, jltl2ba will produce an APSet L0, L1, ...
With formula simplifications (upcoming commit), some APs can be missing
in the NBA (when irrelevant) or reordered (due to formula simplification).
We handle edge label construction as elsewhere in PRISM for DA, to take
this into account.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11186 bbc10eb1-c90d-0410-af57-cb519fbb1720
This is currently caught elsewhere as well, but provides defense-in-depth
for the situation that time bounds in LTL are supported later on.
Bounds on temporal operators don't have the same semantics in CTMCs
as for discrete-time models.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11178 bbc10eb1-c90d-0410-af57-cb519fbb1720
If the expected result specified via // RESULT
is an error, we treat a PrismNotSupportedException just
as any other ordinary exception. This allows verifying
the content of a PrismNotSupportedException error message.
Otherwise, we do the usual special handling as before.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11173 bbc10eb1-c90d-0410-af57-cb519fbb1720
There's actually JDK library functionality for a hash map that
uses object identity instead of .equals(), making PlainObjectReference
unnecessary. Use IdentityHashMap instead.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11169 bbc10eb1-c90d-0410-af57-cb519fbb1720
Previously, subformulas were computed by a DTMCModelChecker
in the embedded DTMC, yielding wrong results. Now, maximal
state subformulas are checked via the CTMCModelChecker and
replaced by labels before calling the LTL model checking
routine on the embedded DTMC.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11168 bbc10eb1-c90d-0410-af57-cb519fbb1720
Dave Parker