Created attachment 340 [details]
Model which shows deadlock in the simulator
When the simulator is entered all possible steps are shown including a step that results in a deadlock. However, the model does not contain a deadlock.
All the nodes in the model have a lock and an invariant on that clock. The deadlock would happen if the invariant was not there. The verifier also states that there is no deadlock when using the query E<> deadlock.
I have attached the model in question.