Faulty channels 10 ? Protokol...
Protokol ?FC pre komunikáciu s dvoma FC (pre cr, cs a pre ackr, acks) má splnat nasledujúce podmienky:
invariant mr ? ms
|mr| = n ? |mr| = n + 1
Program P3
declare ks, kr: integer
initially
ks, kr = 1, 0
? cs, cr, acks, ackr = null, null, null, null
? mr = null
assign
ackr := ackr;kr
? ks := ks + 1 if acks ? null ? ks = head(acks)
|| acks := tail(acks) if acks ? null
? cs := cs;(ks, ms[ks])
? kr, mr := kr + 1, mr;head(cr).val
if cr ? null ? kr ? head(cr).dex
|| cr := tail(cr)