Created attachment 333 [details] Uppaal model of scheduling system I have a query on the form Pr[<=time](<> ERROR) to see the probability of a scheduling system to enter an error state. If no trace is asked for, there are no problems. I get a probability. However, if I ask for some trace, then the GUI responds with the error message "Index 2048 out of bounds for length 2048" and the trace is not loaded. I have tested with version 4.1.20-3 and the trace loads correctly there. I have attached the model that I use. The query is in the XML file.
Confirmed. I also tested the model with 4.1.22 and it does not have this issue, so it must be something with stratego GUI.