UPPAAL 4.1.26 - 64bit: Index out of bounds

[sschivo]

Dear all,
I have been teaching UPPAAL and timed automata in a course for a while, and both I and my students enjoy using it.
However, we may have run into a bug in the latest versions of UPPAAL (4.1.24 and 4.1.26, 64bit, both under Windows and MacOS, as far as we could test). After modifying a template, if we click on the "Simulator" tab, then confirm that we want to reload the model, we get a java.lang.ArrayIndexOutOfBounds exception. I have played a little bit, and found that this may have something to do with the use of arrays of channels, and having a synchronisation on such a channel as available transition in the initial state. I am not sure whether this is actually the case, but I have procedure that allows to see the exception:

• start UPPAAL
• under declarations, add an array of channels. I used this code:
  const int N = 3; typedef int[0,N-1] myType; chan c[N];
• modify the existing template so that it can send an output on channel c. I added a self-loop transition, with a select i : myType and a synchronisation c[i]!
• add a second template (and declare it in "System declarations") that has a similar self-loop transition, but with an input instead of an output
• click on the "Simulator" tab
• the following exception appears:

I will be happy to contribute some more information if needed

Best regards

Stefano

[mikucionisaau]

I believe this is an interaction bug when modifying the model (like changing the number of processes) and switching back and forth between Editor and Simulator. The concrete sequence of actions is difficult to reproduce.