diff options
| -rw-r--r-- | doc/trans.pseudo | 41 |
1 files changed, 36 insertions, 5 deletions
diff --git a/doc/trans.pseudo b/doc/trans.pseudo index 644633a..cf3e6b9 100644 --- a/doc/trans.pseudo +++ b/doc/trans.pseudo @@ -66,7 +66,7 @@ recv(m) { } acks := union(positiveAcks, negativeAcks) - for each ack in acks s.t. sender(ack) == sender(m) && m.seq > ack.seq+1 { + if t.e. ack in acks s.t. sender(ack) == sender(m) && m.seq > ack.seq+1 { insert(m.id, negativeAcks) } } @@ -81,10 +81,6 @@ retransmit() { } } -prune() { - // TODO: use Observable Predicate for Delivery -} - // Observable Predicate for Delivery. // The process that broadcast c has received and acked message a at the time of broadcasting c. // All assertions must hold in order to return true. @@ -107,3 +103,38 @@ OPD(a, c m) bool { } } } + +// Extend seq to include A. +OPDseq(seq []m, A m) ok { + if A in seq { + return true + } + + // C -> ... -> B -> ... ?-> A + C := first(seq) + B := last(seq) + + sent := all m in received s.t. m.sender == B && m not in seq + potentialPredecessors := sent + B.positiveAcks - C.negativeAcks + + for each m in potentialPredecessors { + if OPDseq(append(seq, m), A) { + return true + } + } + + return false +} + +// Free memory from the received list. +prune() { + A := oldest(received) + for all q in group { + C := most recent m in received s.t. m.sender == q + if !OPDseq(m[]{C}, A) { // q has not received A + return + } + } + // All processes have received A. + delete(A, received) +} |