Verifying liveness properties in UPPAAL

[KanzieOpVakantie]

Hello,
I am currently working on an academic report where the goal is to model and verify a specific system in UPPAAL. After I finished modeling, I ran into an issue while trying to verify the model.

Currently I have simplified my model to the following:

The model contains an operator that controls a gate with "open_gate"and "close_gate" binary channels. When the operator starts opening or closing the gate, the gate can either, at some point, become fully opened or closed, or the operator can interrupt this by reversing the direction of opening and closing.

Note: my actual model contains many more interacting templates.

The liveness property that I want to verify on this model is the following:

• For all states, there exists some future path where the can barrier become closed.

This means that from all existing states in the model there exists atleast one execution path where BAR.CLosed should be reachable.

I do not want to check that all states eventually lead to a closed barrier as it should be possible that operator keeps partially closing the barrier and opening it again.

I’ve tried a number of different queries to verify this property, but I have not found a solution yet.

My question is thus: is checking this property indeed not possible in UPPAAL, or is there some workaround such that checking this property is possible?

Thank you in advance!

[mikucionisaau]

I think there is a confusion in this statement:

For all states, there exists some future path where the can barrier become closed.

In CTL, the first quantifier relates to path and the second to the states.
Please see: Potentially Always

If I rephrase your statement like this:

There exists some path where the barrier is always closed.

Then the query would be like this:

E[] Gate1.Closed