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
Fatal error: null
The server connection has been killed.
Futhermore, ArrayIndexOutOfBoundsException and NullPointerException are thrown.
Created attachment 31 [details]
Created attachment 32 [details]
The bug cannot be recreated in version 3.5.4 on windows (which narrows the
possible location of the bug).
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.
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.