Bug 676 - committed receiver causes time-locks
Summary: committed receiver causes time-locks
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.24
Hardware: All All
: P5 critical
Assignee: Marius Mikučionis
Depends on:
Reported: 2019-12-19 17:51 CET by Marius Mikučionis
Modified: 2020-01-08 11:55 CET (History)
0 users

See Also:

model (1.19 KB, text/xml)
2019-12-19 17:51 CET, Marius Mikučionis

Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2019-12-19 17:51:46 CET
Created attachment 341 [details]

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.