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

Bug 148 - "Fatal error: null" when running a fastest diagnostic trace
Summary: "Fatal error: null" when running a fastest diagnostic trace
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.5.5
Hardware: PC Linux
: P2 normal
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2005-04-15 11:15 CEST by Lars T. Mikkelsen
Modified: 2005-04-24 20:01 CEST (History)
0 users

See Also:
Architecture:

Attachments
Uppaal model (2.86 KB, text/plain)
2005-04-15 11:16 CEST, Lars T. Mikkelsen 		Details
Stacktrace (3.77 KB, text/plain)
2005-04-15 11:17 CEST, Lars T. Mikkelsen 		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 Lars T. Mikkelsen 2005-04-15 11:15:13 CEST 
Steps to reproduce:
1. In the attached model, insert the following query:
E<> Girl1.knows_all and Girl2.knows_all and Girl3.knows_all and Girl4.knows_all
2. Select Options, Diagnostic Trace, Fastest from the menu
3. Press Check

Result:
Fatal error: null
The server connection has been killed.

Futhermore, ArrayIndexOutOfBoundsException and NullPointerException are thrown.
Comment 1 Lars T. Mikkelsen 2005-04-15 11:16:39 CEST 
Created attachment 31 [details]
Uppaal model
Comment 2 Lars T. Mikkelsen 2005-04-15 11:17:03 CEST 
Created attachment 32 [details]
Stacktrace
Comment 3 Robert Olesen 2005-04-23 11:51:39 CEST 
The bug cannot be recreated in version 3.5.4 on windows (which narrows the
possible location of the bug).
Comment 4 Gerd Behrmann 2005-04-24 19:40:13 CEST 
On Linux with UPPAAL 3.5.5 I do see the exceptions, although I do not loose the
server connection. I will investigate the problem further.
Comment 5 Gerd Behrmann 2005-04-24 20:01:34 CEST 
Turns out that this is a problem in the serialization method for symbolic
states: When finding the shortest trace, UPPAAL internally adds an extra clock
to the model to keep track of the length (in time) of the trace. Unfortunately,
the serialization method was not aware of this and as a result it also
serialized this additional clock.

A fix has been checked into CVS.