Bug 675

Summary: Shows deadlock in simulator but model does not contain deadlock
Product: UPPAAL Reporter: Martin Kristjansen <mk>
Component: GUIAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: minor    
Priority: P5    
Version: 4.1.24   
Hardware: PC   
OS: All   
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