Liveness Argument et SN(t), RN(t be values of sn and rn at time t From the algorithm, (1 SN(t and rN(t are increasing in t and sn(t s RN(t for all t (2) From safety(since i has not been sent before ty)RN(t)si and SN(t)= From (1)and (2 ), RN(t,=sN(t =i RN is incremented at t2 and sn at t3, so t2 <t3 A transmits i repeatedly up to t,, and thus to t2 when it is correctly received. Since q>0, t2 is finite B transmits RN=i+1 repeatedly until correctly received at t3, and q?0 implies that t3 is finite Eytan modiano
Liveness Argument • Let SN(t), RN(t) be values of SN and RN at time t From the algorithm, (1) SN(t) and RN(t) are increasing in t and SN(t) ≤ RN(t) for all t (2) From safety (since i has not been sent before t1) RN(t1) ≤ i and SN(t1) = i • From (1) and (2), RN(t1) = SN(t1) = i • RN is incremented at t2 and SN at t3, so t2 < t3 • A transmits i repeatedly up to t3, and thus to t2 when it is correctly received. Since q>0, t2 is finite • B transmits RN=i+1 repeatedly until correctly received at t3, and q>0 implies that t3 is finite. Eytan Modiano 11
Correctness of Stop& Wait with binary (finite)sN, RN Assume that frames travel on link in order Note that with integer sn, rn, either SN=RN (from t, to t2) or (3) SN=RN-1(from t2 to t3) (4) Since frames travel in order the sequence numbers arriving at b and the request numbers arriving at a are increasing, so a single bit can resolve the ambiguity between( 3 and(4) RN =0 and sn =1 or rn =1 and sN=0 = received packet is an old packet RN =0 and sn=o or rn =1 and sn= 1 - received packet is new Eytan modiano
Correctness of Stop & Wait with binary (finite) SN, RN • Assume that frames travel on link in order Note that with integer SN, RN, either SN=RN (from t1 to t 2) or (3) SN=RN-1 (from t2 to t 3) (4) Since frames travel in order, the sequence numbers arriving at B and the request numbers arriving at A are increasing, so a single bit can resolve the ambiguity between (3) and (4) – RN = 0 and SN = 1 or RN =1 and SN = 0 => received packet is an old packet – RN = 0 and SN = 0 or RN = 1 and SN = 1 => received packet is new Eyt an Modiano 12