Simulation query does not deadlock for models with deadlock

[magoorden]

Describe the bug The SMC simulate query does not 'show' (with an error message, in the plot, some other way) that a model contains deadlock. Therefore, a user might get the impression that the model is fine while there is a problem.

To Reproduce Steps to reproduce the behavior:

1. Open newspaper.xml from the demo/stratego folder.
2. Go to the verifier tab and synthesize the strategy Travel.
3. Verify that the sytem is not deadlock free with `A[] not deadlock under Travel' (this query fails).
4. Perform SMC simulations with simulate [<=100; 100] {time} under Travel. This query succeeds.
5. Open the resulting graph and observe that the value of time reaches 100.
6. (Optionally) Verify that no trace exists longer than 65 time units with E<> time >= 65 under Travel
7. (Optionally) Run the concrete simulator with the synthesized strategy Travel using the Stochastic button and observe the deadlock error message.

Expected behavior The SMC simulator let's the user know that a deadlock occured, for example with an error message (maybe too strong) or only showing results up to the deadlock.

Version(s) of UPPAAL tested Uppaal Stratego 10 beta 6, MacOS app version.

Desktop (please complete the following information):

• Version: UPPAAL 4.1.20-stratego-10-beta6 (rev. 506E575E613DA347), June 2022
• OS, Java version: MacOS.

[mikucionisaau]

I think the issue is with the semantics of deadlock: A[] not deadlock uses symbolic semantics, where every symbolic state should have an edge-successor, meanwhile SMC queries use concrete semantics: it needs to be able to progress and an unbounded delay-transition is enough. The newspaper.xml example has a "deadlock" in the final state, but that state is not blocking time, thus SMC queries can simply delay -- not an issue.

[mikucionisaau]

Hm.. E<> time>60 under Travel yields false, because strategy Travel = control: A<> Kim.Done && time <= 60 actually limits the time, meaning that the time is actually stopped under Travel. And that should be consistent in SMC queries, i.e. SMC queries beyond 60 should report time lock.

[petergjoel]

SMC queries beyond 60 should report time lock.

No, it is quite the opposite.

A strategy must propose an action for the player when one is possible. SMC follows this semantics, and normal symbolic model-checking does also -- but only to some extend.

So after "Kim.Done" is reached within "time <= 60", the strategy is free to allow any action (but must propose at least one).

This follows from the definition of strategies.

[magoorden]

A strategy must propose an action for the player when one is possible. SMC follows this semantics, and normal symbolic model-checking does also -- but only to some extend.

So Peter, are you trying to say that the queries A[] not deadlock under Travel and E<> time >= 65 under Travel fail because they don't follow the intended semantics?

[petergjoel]

So Peter, are you trying to say that the queries A[] not deadlock under Travel and E<> time >= 65 under Travel fail because they don't follow the intended semantics?

A not deadlock does not hold in the model initially, so I am not too surprised that it does not hold under the strategy. It seems that the state where all processes are in "Done" is considered deadlocked.

E<> time >= 65 under Travel should def. hold.

[magoorden]

Something else that might be related. When you synthesize the Travel strategy and simulate it with the concrete simulator using the Stochastic option, a deadlock is detected when time passes 60 time units. But, when you dismiss the error popup, you can continue the simulation as Marius is still able to perform a transition.

[mikucionisaau]

@magoorden Could you attach that trace you have in that last post? I cannot reproduce via stochastic random simulation.

[magoorden]

Here is a trace that indicated a deadlock problem while there are still transitions possible. NewspaperConcreteSimulatorDeadlockTrace.uctr.txt