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

Bug 417 - Crash when loading a trace file from the simulator
Summary: Crash when loading a trace file from the simulator
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.0.6
Hardware: PC Linux
: P2 normal
Assignee: Alexandre David
Depends on:
Reported: 2007-05-14 16:46 CEST by Ludovic Apvrille
Modified: 2008-06-12 17:07 CEST (History)
1 user (show)

See Also:

UPPAAL model (66.29 KB, text/xml)
2007-05-14 16:46 CEST, Ludovic Apvrille
Query file - quite basic (93 bytes, application/octet-stream)
2007-05-14 16:47 CEST, Ludovic Apvrille
Trace file generated by verifyta (32 bytes, text/plain)
2007-05-14 16:48 CEST, Ludovic Apvrille

Note You need to log in before you can comment on or make changes to this bug.
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.