Bug 675 - Shows deadlock in simulator but model does not contain deadlock
Summary: Shows deadlock in simulator but model does not contain deadlock
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.1.23
Hardware: PC Linux
: P5 enhancement
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2019-12-02 12:07 CET by Martin Kristjansen
Modified: 2019-12-02 12:07 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

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.