Reputation: 11
I currently have information of time in the form of a distribution as shown in the image below.
I want to provide this time information(which is in the form of a distribution) as invariant in a location and/or a guard in a transition in UPPAAL SMC(Statistical Model Checking). However, I see that in an invariant you can only provide two possible data: 1) Time data by using clock variables in Invariant and 2) By using Rate of Exponential (Attached an image of options in invariant). . In both these cases, we cannot provide a time distribution data (as shown in the above image) since invariant doesn't provide any other means to provide this data as a condition. It is also not possible to provide this time distribution data in Guard condition in a transition as far as I am aware.
I understand that UPPAAL SMC provides results(Output) in the form of distribution when you right click on the query in the Verifier. However, I am not able to understand how I can provide the same as an input to Locations in UPPAAL. So, could someone please let me know if this is possible to do in UPPAAL SMC? If so, could you please let me know on how we can do this?
Upvotes: 0
Views: 14