| Summary: | Shows deadlock in simulator but model does not contain deadlock | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Martin Kristjansen <mk> |
| Component: | GUI | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | minor | ||
| Priority: | P5 | ||
| Version: | 4.1.24 | ||
| Hardware: | PC | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | Model which shows deadlock in the simulator | ||
Yes, that deadlock transition is superfluous and misleading. Thank you for the report |
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.