Describe the bug
When generating a strategy Goal for a timed game with reachability goal Main.Win, I would like to verify that it works by using the query A<> Main.Win under Goal. This should by definition always be true if a winning strategy was generated. However, it sometimes is not. It seems that when an UPPAAL strategy is generated there is an underlying assumption that actions are taken as soon as possible, so if I must wait until 2<=x<=10 to do a then I should do a at exactly x=2 otherwise the strategy is not guaranteed to work. However, in the under <strategy query this is not how it works - here it will assume that the action is taken anywhere between 2 and 10 (symbolically). I present two examples (MNWEs.zip) where this incorrect application of a strategy causes the verifying query to fail:
A model that has a trivial winning strategy, simply go to the winning state between 2 <= x <= 10 (but do it as fast as possible).
In this model the verifying query is false, because there exists runs where the action is taken after 3, where an uncontrollable action can cause us to deadlock. This will never be the case if the strategy is applied correctly though.
filename: strategy_example_MNWE
A model that has a bit more complex winning strategy. Essentially here when we reach L2 (x can at most be 2 on arrival), we should take the transition to Win ASAP (now). But the verifying query is false, because there exists runs where the action is taken after x=3, where the uncontrollable action will move us back to L1 and this repeats infinitely often, invalidating the A<> Main.Win.
filename: strategy_example_MNWE_loop
To Reproduce
Steps to reproduce the behavior:
Open the first example.
Run the first query to generate strategy and watch it successfully generate one (green)
Run the second query to verify the strategy and watch it fail (red)
Repeat 1-3 for the second example.
Expected behavior
When successfully generating a winning strategy Goal for a timed game with reachability goal Main.Win I expect that the query A<> Main.Win under Goal will always be true.
Version(s) of UPPAAL tested
5.0.0
Screenshots
Screenshots of both models:
Deadlock:
Loop:
Desktop (please complete the following information):
Describe the bug When generating a strategy
Goalfor a timed game with reachability goalMain.Win, I would like to verify that it works by using the queryA<> Main.Win under Goal. This should by definition always be true if a winning strategy was generated. However, it sometimes is not. It seems that when an UPPAAL strategy is generated there is an underlying assumption that actions are taken as soon as possible, so if I must wait until2<=x<=10to doathen I should doaat exactlyx=2otherwise the strategy is not guaranteed to work. However, in theunder <strategyquery this is not how it works - here it will assume that the action is taken anywhere between 2 and 10 (symbolically). I present two examples (MNWEs.zip) where this incorrect application of a strategy causes the verifying query to fail:A model that has a trivial winning strategy, simply go to the winning state between
2 <= x <= 10(but do it as fast as possible). In this model the verifying query is false, because there exists runs where the action is taken after 3, where an uncontrollable action can cause us to deadlock. This will never be the case if the strategy is applied correctly though. filename:strategy_example_MNWEA model that has a bit more complex winning strategy. Essentially here when we reach L2 (x can at most be 2 on arrival), we should take the transition to Win ASAP (now). But the verifying query is false, because there exists runs where the action is taken after x=3, where the uncontrollable action will move us back to L1 and this repeats infinitely often, invalidating the
A<> Main.Win. filename:strategy_example_MNWE_loopTo Reproduce Steps to reproduce the behavior:
Expected behavior When successfully generating a winning strategy
Goalfor a timed game with reachability goalMain.WinI expect that the queryA<> Main.Win under Goalwill always be true.Version(s) of UPPAAL tested 5.0.0
Screenshots Screenshots of both models: Deadlock:
Loop:
Desktop (please complete the following information):
Additional context This bug has been discussed with @mikucionisaau in an online video call.