|Summary:||NullPointerException in simulator, does not update state information afterwards|
|Product:||UPPAAL||Reporter:||Marius Mikučionis <marius>|
|Component:||GUI||Assignee:||Gerd Behrmann <behrmann>|
model to reproduce an exception in simulator
Smaller test case
Description Marius Mikučionis 2006-07-12 19:21:48 CEST
to reproduce: 1) load database.xml model 2) go to verifier 3) set the diagnostic trace to shortest 4) ask to verify "A<> present==table", property is not satisfied, get the trace. 5) go to simulator 6) click on the second last line in the trace, or traverse through red steps 7) boom: java.lang.NullPointerException at com.uppaal.gui.simulator.ChoiceModel.a(Unknown Source) at com.uppaal.gui.simulator.Simulator.p(Unknown Source) at com.uppaal.gui.simulator.Simulator.l(Unknown Source) at ce.run(Unknown Source) at java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:209) at java.awt.EventQueue.dispatchEvent(EventQueue.java:461) at java.awt.EventDispatchThread.pumpOneEventForHierarchy(EventDispatchThread.java:242) at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:163) at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:157) at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:149) at java.awt.EventDispatchThread.run(EventDispatchThread.java:110) 8) simulator does not update the state information anymore
Comment 1 Marius Mikučionis 2006-07-12 19:23:01 CEST
Created attachment 107 [details] model to reproduce an exception in simulator
Comment 2 Gerd Behrmann 2006-07-13 10:22:27 CEST
*** This bug has been marked as a duplicate of 333 ***
Comment 3 Gerd Behrmann 2006-07-31 20:33:57 CEST
The behaviour described above does not depend on selecting 'shortest trace' (in contrast to what one might expect when the report explicitly states selecting 'shortest trace') - 'some trace' will also do. Thus the problem is unrelated to bug 333.
Comment 5 Gerd Behrmann 2006-08-01 13:10:47 CEST
I have attached a test case. The liveness checker does not need to be involved. Indeed, the trace does not need to come from the model checker to reproduce the problem. In the attached model, take the enabled transition and click on that transition in the trace: Boom! The bug is in the function which selects the transition in the list of enabled transitions when clicking on a transition in the trace: The function does not deal correctly with transitions with target states not satisfying the invariant.
Comment 6 Gerd Behrmann 2006-08-01 16:44:07 CEST
Fixed on the 4.0 branch from rev. 2483 and on the trunk from rev. 2482.