trans pseudocode: prune()

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)
+}