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

Bug 417

Summary: Crash when loading a trace file from the simulator
Product: UPPAAL Reporter: Ludovic Apvrille <ludovic.apvrille>
Component: GUIAssignee: Alexandre David <adavid>
Severity: normal CC: ludovic.apvrille
Priority: P2    
Version: 4.0.6   
Hardware: PC   
OS: Linux   
Attachments: UPPAAL model
Query file - quite basic
Trace file generated by verifyta

Description Ludovic Apvrille 2007-05-14 16:46:09 CEST
I have generated a trace file using the following command line:
verifyta -u -t1 -f toto spec.xml q01.q
When I open the trace file (i.e. toto-1.xtr) with the UPPAAL simulator (OPEN button), I get:
        at com.uppaal.engine.Parser.locationVector(
        at com.uppaal.engine.Parser.parseState(
        at com.uppaal.engine.Parser.parseXTRTrace(
        at z.a(Unknown Source)
        at com.uppaal.gui.simulator.Simulator.h(Unknown Source)
        at com.uppaal.gui.simulator.Simulator.g(Unknown Source)
        at E.actionPerformed(Unknown Source)
        at javax.swing.AbstractButton.fireActionPerformed(
        at javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.jav
        at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel
        at javax.swing.DefaultButtonModel.setPressed(
        at javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonL
        at java.awt.AWTEventMulticaster.mouseReleased(
        at java.awt.Component.processMouseEvent(
        at javax.swing.JComponent.processMouseEvent(
        at java.awt.Component.processEvent(
        at java.awt.Container.processEvent(
        at java.awt.Component.dispatchEventImpl(
        at java.awt.Container.dispatchEventImpl(
        at java.awt.Component.dispatchEvent(
        at java.awt.LightweightDispatcher.retargetMouseEvent(
        at java.awt.LightweightDispatcher.processMouseEvent(
        at java.awt.LightweightDispatcher.dispatchEvent(
        at java.awt.Container.dispatchEventImpl(
        at java.awt.Window.dispatchEventImpl(
        at java.awt.Component.dispatchEvent(
        at java.awt.EventQueue.dispatchEvent(
        at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThre
        at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.
        at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThre
        at java.awt.EventDispatchThread.pumpEvents(
        at java.awt.EventDispatchThread.pumpEvents(
Comment 1 Ludovic Apvrille 2007-05-14 16:46:50 CEST
Created attachment 153 [details]
UPPAAL model
Comment 2 Ludovic Apvrille 2007-05-14 16:47:08 CEST
Created attachment 154 [details]
Query file - quite basic
Comment 3 Ludovic Apvrille 2007-05-14 16:48:55 CEST
Created attachment 155 [details]
Trace file generated by verifyta
Comment 4 Gerd Behrmann 2007-05-15 17:43:37 CEST
I cannot reproduce this problem. I have loaded your model in UPPAAL 4.0.6 and loaded the XTR file in the simulator. It loads without any errors. I also tried regenerating the trace, both from inside the GUI and with verifyta. In both cases I did not have a problem.

Could you please check that you can reproduce the problem with the files attached to this bug. The problem you describe *could* be triggered when loading a trace file for a different model than the one currently loaded in the simulator. Could you please check that this is not the case here.
Comment 5 Ludovic Apvrille 2007-05-15 18:16:20 CEST
I've rebooted my machine, restarted UPPAAL, and use the file I provide... and effectively, it works. Well, I am going to try my best to reproduce this bug!
Comment 6 Alexandre David 2008-06-12 17:07:21 CEST
If after more than a year the bug could not be reproduced, it was certainly due to a mismatch between the model and the trace. We are planning to tight together traces and models to avoid this problem in the future.

Revision 3779 contains a work-around to detect trace mismatch.