I am using UPPAAL 4.1.24 for modeling a simple system composed of 1 main process and 3 observer processes. The main process uses a broadcast channel which is listened to by the observer processes. I have enabled Options -> Diagnostic Trace -> Some.
Now every time I check for a property by a query from the verifier, I can see the trace and replay it in the Trace box under the Simulator tab. However, it only works for the properties which are getting satisfied. If a property given by a query is not satisfied then the Trace does not get updated and I can not see the trace for that 'Not Satisfied" property.
Any idea?