| Summary: | liveness check crashes on model with (process) priorities | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | RESOLVED FIXED | ||
| Severity: | critical | CC: | adavid |
| Priority: | P4 | ||
| Version: | 4.1.20 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | minimal model | ||
Fixed and release in version 4.1.20 |
Created attachment 314 [details] minimal model The small model demonstrates the issue. The root cause is that the priority filter generates terminating (NULL) tokens and the liveness filter is not prepared for such.