I think it should implement that :
Algorithm 3.12: Broadcast with Sequence Number
Implements:
FIFOReliableBroadcast, instance frb.
Uses:
ReliableBroadcast, instance rb.
upon event frb, Init do
lsn := 0;
pending := ∅;
next := [1]N ;
upon event frb, Broadcast | m do
lsn := lsn + 1;
trigger rb, Broadcast | [DATA, self, m, lsn] ;
upon event rb, Deliver | p, [DATA, s, m, sn] do
pending := pending ∪ {(s, m, sn)};
while exists (s, m
, sn
) ∈ pending such that sn = next[s] do
next[s] := next[s]+1;
pending := pending \ {(s, m
, sn
)};
trigger frb, Deliver | s, m ;