Invariant problem

[Toni CESAR]

Good afternoon, first time writing here.

I'm quite new in Uppaal but I really need some help with an issue.

I'm creating a system that updates variables values and only evolves when certain constraints (via guards and invariants are met). I'm struggling quite hard on finding why this system reaches an state with an invalid invariant (based on the variables, not the clocks), as when using the simulator it runs well, but when trying query verification it fails.

I leave a photograph of the system here. Hope you can help me.

[Marius Mikučionis]

Hi,

Could you enable Diagnostic trace in Options and then inspect the trace in the simulator?

It should show you the state and variable values that break the invariant, then hopefully you can back-trace to the real cause of the issue.

You can enable the trace as a default option for all the queries from the menu:

Or on the specific query only by using the cog next to the query:

(once the query-specific options are used, Uppaal will remember them by showing the yellow plus and ignore the defaults in the menu)

Symbolic simulator usually displays multiple (symbolic) transitions available: when a specific transition is selected, the constrains show when that transition is available. If you have a deadlock "transition", then the constrains will show when exactly the system is in deadlock (or a timelock).

If you still have issues, please share the model (and a trace if it takes long time), hopefully we can pin-point it to you.

Best regards,
Marius