// bounded retransmission protocol [D'AJJL01] // gxn/dxp 23/05/2001 // Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) nondeterministic //dtmc // number of chunks const int N = 256; // maximum number of retransmissions const int MAX = 5; // reliability of channels param float pL; param float pK; global T : bool; module sender s : [0..6]; // 0 idle // 1 next_frame // 2 wait_ack // 3 retransmit // 4 success // 5 error // 6 wait sync srep : [0..3]; // 0 bottom // 1 not ok (nok) // 2 do not know (dk) // 3 ok (ok) nrtr : [0..MAX]; i : [0..N]; bs : bool; s_ab : bool; fs : bool; ls : bool; // idle [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); // next_frame [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); // wait_ack [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); [TO_Msg] (s=2) -> (s'=3); [TO_Ack] (s=2) -> (s'=3); // retransmit [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); // success [] (s=4) & (i (s'=1) & (i'=i+1); [] (s=4) & (i=N) -> (s'=0) & (srep'=3); // error [SyncWait] (s=5) -> (s'=6); // wait sync [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); endmodule module receiver r : [0..5]; // 0 new_file // 1 fst_safe // 2 frame_received // 3 frame_reported // 4 idle // 5 resync rrep : [0..4]; // 0 bottom // 1 fst // 2 inc // 3 ok // 4 nok fr : bool; lr : bool; br : bool; r_ab : bool; recv : bool; // new_file [SyncWait] (r=0) -> (r'=0); [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); // fst_safe_frame [] (r=1) -> (r'=2) & (r_ab'=br); // frame_received [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); [aA] (r=2) & !(r_ab=br) -> (r'=4); // frame_reported [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); // idle [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); [SyncWait] (r=4) & (ls=true) -> (r'=5); [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); // resync [SyncWait] (r=5) -> (r'=0) & (rrep'=0); endmodule module checker [NewFile] (T=false) -> (T'=false); [NewFile] (T=false) -> (T'=true); endmodule module channelK k : [0..2]; // idle [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); // sending [aG] (k=1) -> (k'=0); // lost [TO_Msg] (k=2) -> (k'=0); endmodule module channelL l : [0..2]; // idle [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); // sending [aB] (l=1) -> (l'=0); // lost [TO_Ack] (l=2) -> (l'=0); endmodule init T=false & bs = false & s_ab = false & fs = false & ls = false & fr = false & lr = false & br = false & r_ab = false & recv = false & srep = 0 & i = 0 & k = 0 & l = 0 & r = 0 & s = 0 & nrtr = 0 & rrep = 0 endinit