|Summary:||Shows deadlock in simulator but model does not contain deadlock|
|Product:||UPPAAL||Reporter:||Martin Kristjansen <mk>|
|Component:||GUI||Assignee:||Marius Mikučionis <marius>|
|Attachments:||Model which shows deadlock in the simulator|
Description Martin Kristjansen 2019-12-02 12:07:08 CET
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.
Comment 1 Marius Mikučionis 2019-12-10 12:53:56 CET
Yes, that deadlock transition is superfluous and misleading. Thank you for the report