This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 676

Summary: committed receiver causes time-locks
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: critical    
Priority: P5    
Version: 4.1.24   
Hardware: All   
OS: All   
Architecture:
Attachments: model

Description Marius Mikučionis 2019-12-19 17:51:46 CET
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.