Missing documentation about the strategy synthesis assumptions. In particular, it is very easy to run into time-lock situation without further diagnostics even though the model itself does not have time-locks.
Further text is speculative.
Current strategy synthesis assumes that the controller can do one of the following (provided that the model permits):
1) choose and execute a transition urgently
2) choose to delay (forever or until interrupted by the environment)
During the simulation under the strategy, once the controller commits to a delay choice, it cannot change the decision and thus the environment should make a transition. The issue is that if the environment cannot take a transition (e.g. no uncontrollable edges available from the current state), then neither environment nor controller can progress (as the controller cannot change its delay decision), therefore the system is stuck in that location -- deadlock, and in a state with an invariant it means time-lock.
So a correct modeling pattern would be to always have environment edge available where the delay is permitted.
Missing documentation about the strategy synthesis assumptions. In particular, it is very easy to run into time-lock situation without further diagnostics even though the model itself does not have time-locks.
Further text is speculative.
Current strategy synthesis assumes that the controller can do one of the following (provided that the model permits): 1) choose and execute a transition urgently 2) choose to delay (forever or until interrupted by the environment)
During the simulation under the strategy, once the controller commits to a delay choice, it cannot change the decision and thus the environment should make a transition. The issue is that if the environment cannot take a transition (e.g. no uncontrollable edges available from the current state), then neither environment nor controller can progress (as the controller cannot change its delay decision), therefore the system is stuck in that location -- deadlock, and in a state with an invariant it means time-lock.
So a correct modeling pattern would be to always have environment edge available where the delay is permitted.