Summary: | 4.1.20-stratego-5 Trace not loaded in Pr[] query | ||
---|---|---|---|
Product: | UPPAAL Stratego | Reporter: | Martin Kristjansen <mk> |
Component: | GUI | Assignee: | Marius Mikučionis <marius> |
Status: | ASSIGNED --- | ||
Severity: | normal | ||
Priority: | P5 | ||
Version: | 4.1.20-5 | ||
Hardware: | PC | ||
OS: | Linux | ||
Architecture: | |||
Attachments: | Uppaal model of scheduling system |
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. |
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.