From 73a4ccf44fdf4c8f05032c1bb41801985f40087f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 1 Apr 2016 10:31:15 +0000 Subject: [PATCH] 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 --- prism/src/simulator/SimulatorEngine.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 05639541..13b9da57 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -482,7 +482,7 @@ public class SimulatorEngine extends PrismComponent { updater.calculateTransitions(state, transitionList); transitionListBuilt = true; - transitionListState = null; + transitionListState = state; } // ------------------------------------------------------------------------------