This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 675 - Shows deadlock in simulator but model does not contain deadlock
Summary: Shows deadlock in simulator but model does not contain deadlock
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.1.24
Hardware: PC All
: P5 minor
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2019-12-02 12:07 CET by Martin Kristjansen
Modified: 2019-12-10 12:53 CET (History)
0 users

See Also:
Architecture:

Attachments
Model which shows deadlock in the simulator (1.71 KB, text/xml)
2019-12-02 12:07 CET, Martin Kristjansen 		Details
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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