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: java.lang.NullPointerException at com.uppaal.engine.Parser.locationVector(Parser.java:78) at com.uppaal.engine.Parser.parseState(Parser.java:69) at com.uppaal.engine.Parser.parseXTRTrace(Parser.java:308) 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(AbstractButton.java:19 95) at javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.jav a:2318) at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel .java:387) at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:242 ) at javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonL istener.java:236) at java.awt.AWTEventMulticaster.mouseReleased(AWTEventMulticaster.java:2 72) at java.awt.Component.processMouseEvent(Component.java:6038) at javax.swing.JComponent.processMouseEvent(JComponent.java:3260) at java.awt.Component.processEvent(Component.java:5803) at java.awt.Container.processEvent(Container.java:2058) at java.awt.Component.dispatchEventImpl(Component.java:4410) at java.awt.Container.dispatchEventImpl(Container.java:2116) at java.awt.Component.dispatchEvent(Component.java:4240) at java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4322 ) at java.awt.LightweightDispatcher.processMouseEvent(Container.java:3986) at java.awt.LightweightDispatcher.dispatchEvent(Container.java:3916) at java.awt.Container.dispatchEventImpl(Container.java:2102) at java.awt.Window.dispatchEventImpl(Window.java:2429) at java.awt.Component.dispatchEvent(Component.java:4240) at java.awt.EventQueue.dispatchEvent(EventQueue.java:599) at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThre ad.java:273) at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread. java:183) at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThre ad.java:173) at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:168) at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:160) at java.awt.EventDispatchThread.run(EventDispatchThread.java:121)
Created attachment 153 [details] UPPAAL model
Created attachment 154 [details] Query file - quite basic
Created attachment 155 [details] Trace file generated by verifyta
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.
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!
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.