Finding strategies enforcing "until" (AU) formulas is bugged

[NicEastvillage]

Describe the bug
The query control: A[ .. U .. ] fails to find an obvious strategy involving a single discrete action.

This bug was reported by Sibylle Schupp.

To Reproduce

1. Make this template with just two locations, Init and Goal, with a controllable edge between them:

2. Instantiate the template as P.
3. Run the query control: A[ P.Init U P.Goal ]
   • Result is FALSE even though there is an obvious strategy satisfying the query; Just activate the controllable edge!

See: AU bug.xml

Expected behavior
The query should return TRUE.

Version(s) of UPPAAL tested
Uppaal v5.0.0

Additional Context
The semantics of AU for timed systems are usually:

Note the disjunction that is needed due to the denseness of time. Without it, it would not be valid to delay into phi_2 as you would always be able to find a smaller delay that lands in the clock valuation between the clock valuations where phi_1 hold and the clock valuation where phi_2 holds. HOWEVER, this should not affect the bug reported here, as only discrete actions are required to recreate this bug.

[NicEastvillage]

I have located the issue in Tiga's forward filter. It is indeed implemented as if A[phi1 U phi2] means A[phi1 U (phi1 and phi2)] as Sibylle suspected. The git message mentions a fix to Büchi mode identifying too many winning states. Maybe this fix to Büchi mode messed up the normal mode.

[NicEastvillage]

The Büchi mode is used in the ECDAR extension, and according to https://docs.uppaal.org/extensions/ecdar/ the "wrong" semantics for AU are intended in ECDAR. The semantics of AU described at https://docs.uppaal.org/language-reference/query-syntax/controller_synthesis/ is slightly ambiguous.