| Summary: | NullPointerException in simulator, does not update state information afterwards | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | GUI | Assignee: | Gerd Behrmann <behrmann> |
| Status: | RESOLVED FIXED | ||
| Severity: | normal | ||
| Priority: | P2 | ||
| Version: | 4.0.1 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: |
model to reproduce an exception in simulator
Smaller test case |
||
Created attachment 107 [details]
model to reproduce an exception in simulator
*** This bug has been marked as a duplicate of 333 *** 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. Created attachment 110 [details]
Smaller test case
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. Fixed on the 4.0 branch from rev. 2483 and on the trunk from rev. 2482. |
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