This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 339 - NullPointerException in simulator, does not update state information afterwards
Summary: NullPointerException in simulator, does not update state information afterwards
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.0.1
Hardware: PC Linux
: P2 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2006-07-12 19:21 CEST by Marius Mikučionis
Modified: 2006-08-01 16:44 CEST (History)
0 users

See Also:
Architecture:

Attachments
model to reproduce an exception in simulator (8.20 KB, application/xml)
2006-07-12 19:23 CEST, Marius Mikučionis 		Details
Smaller test case (886 bytes, text/xml)
2006-08-01 13:07 CEST, Gerd Behrmann 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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 4 Gerd Behrmann 2006-08-01 13:07:15 CEST 
Created attachment 110 [details]
Smaller test case
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.