Question about 1-to-Many Synchronization in UPPAAL

[Szpilman2]

Dear UPPAAL Team,

I hope this message finds you well.

According to the UPPAAL documentation, the definition of a broadcast channel is as follows:

Broadcast channels allow 1-to-many synchronizations. The intuition is that an edge with the synchronization label e! emits a broadcast on the channel e, and any enabled edge with the synchronization label e? will synchronize with the emitting process. That is, an edge with an emit-synchronization on a broadcast channel can always fire (provided that the guard is satisfied), regardless of whether any receiving edges are enabled. However, those receiving edges that are enabled will synchronize. Note that clock guards are not allowed on edges receiving on a broadcast channel. The update on the emitting edge is executed first, and the updates on the receiving edges are executed left-to-right in the order the processes are given in the system definition.

I would like to achieve a 1-to-many synchronization where, unlike broadcast channels, all receiving edges must synchronize and proceed to the next state when the e! event occurs. In other words, the synchronization should only proceed when all receiving processes are enabled, not just one or more.

Additionally, I would like to impose clock constraints on this transition, which is not allowed with broadcast channels.

Could you please assist me in achieving this?

Thank you very much for your help.

Best regards,
Peyman

[mikucionisaau]

You could use a shared variable to count the number of ready processes and then add a guard on the sending edge.

Clock constraints on the sender side should also work.

[Szpilman2]

Thank you so much for your support. could you possibly give me a simple example representing your idea? actually I don't know how to count number of ready processes...

also shall I use an ordinary channel in the model or broadcast?

thank you so much again.

[mikucionisaau]

Here's an example with msg being broadcast:

[Szpilman2]

Dear Marius, Thank you so much 🥇