Browse Source

SimulatorEngine: fix broken display of updates a path (GUI, regression) [with Linda Leuschner]

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
master
Joachim Klein 10 years ago
parent
commit
73a4ccf44f
  1. 2
      prism/src/simulator/SimulatorEngine.java

2
prism/src/simulator/SimulatorEngine.java

@ -482,7 +482,7 @@ public class SimulatorEngine extends PrismComponent
{
updater.calculateTransitions(state, transitionList);
transitionListBuilt = true;
transitionListState = null;
transitionListState = state;
}
// ------------------------------------------------------------------------------

Loading…
Cancel
Save