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

Bug 662 - 4.1.20-stratego-5 Trace not loaded in Pr[] query
Summary: 4.1.20-stratego-5 Trace not loaded in Pr[] query
Status: ASSIGNED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.1.20-5
Hardware: PC Linux
: P5 normal
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2019-05-09 08:41 CEST by Martin Kristjansen
Modified: 2019-05-09 08:53 CEST (History)
0 users

See Also:
Architecture:

Attachments
Uppaal model of scheduling system (14.56 KB, text/xml)
2019-05-09 08:41 CEST, Martin Kristjansen 		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 Martin Kristjansen 2019-05-09 08:41:26 CEST 
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.
Comment 1 Marius Mikučionis 2019-05-09 08:47:49 CEST 
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.