| Summary: | committed receiver causes time-locks | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | critical | ||
| Priority: | P5 | ||
| Version: | 4.1.24 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | model | ||
Created attachment 341 [details] model The issue was reported by Pieter Cuijpers. Consider the system of two processes: Sender is in committed location and sends on broadcast channel. Receiver is in committed location and receives on the same broadcast channel. The receiver on its own cannot make independend progress, but the system composed with the sender is actually fine (e.g. symbolic semantics works fine). Hoever, SMC declares a time-lock with half times, i.e. the simulations get stuck when the receiver is chosen-- this is inconsistent with symbolic semantics, because the deadlock "transition" is not there (also stratego does not have this issue). I propose a fix to handling of committed processes where the receive-only processes would be removed from the committed race.