| Summary: | java exception upon openning/saving customized Uppaal models | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | GUI | Assignee: | Gerd Behrmann <behrmann> |
| Status: | RESOLVED FIXED | ||
| Severity: | enhancement | ||
| Priority: | P1 | ||
| Version: | 4.0.3 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: | Uppaal-TK created model specification | ||
Created attachment 126 [details]
Uppaal-TK created model specification
Agreed. However I relabel the bug as "enhancement", since technically it is not an error not to be able to read "broken" files. Fixed on the 4.0 branch from rev. 2885. Fixed on the trunk from rev. 2886. |
I have an experimental Uppaal branch for TK project (call it uppaal-tk). The uppaal-tk created documents have two extra labels on edges (and perhaps smth more). The problem is that original Uppaal chokes upon such documents when opening and trying to save later by throwing the following exceptions: java.lang.NullPointerException at com.uppaal.model.core2.Property.getPrototypeFromParent(Property.java:72) at com.uppaal.model.core2.Element.importInto(Element.java:340) at com.uppaal.model.core2.Element.setPrototype(Element.java:353) at com.uppaal.model.core2.Element.importInto(Element.java:340) at com.uppaal.model.core2.Element.setPrototype(Element.java:353) at com.uppaal.model.core2.Node.setPrototype(Node.java:179) at com.uppaal.model.core2.Element.importInto(Element.java:340) at com.uppaal.model.core2.Node.setPrototype(Node.java:182) at com.uppaal.model.core2.Element.importInto(Element.java:340) at com.uppaal.model.core2.Node.setPrototype(Node.java:182) at com.uppaal.gui.SystemInspector.a(Unknown Source) at com.uppaal.gui.SystemInspector.f(Unknown Source) at com.uppaal.gui.SystemInspector.a(Unknown Source) at com.uppaal.gui.Main.b(Unknown Source) at com.uppaal.gui.Main.a(Unknown Source) at cs.run(Unknown Source) at java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:209) at java.awt.EventQueue.dispatchEvent(EventQueue.java:598) at java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:273) at java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:183) at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.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) I would expect that original Uppaal would ignore (and remove) the additional labels and work as usual, or at least not to throw exceptions and refuse to save. Anyway, I think there could be more such problems in the future so I'm attaching a sample document to reproduce the problem.