25 defs |
25 defs |
26 |
26 |
27 rq_def "rq == fst" |
27 rq_def "rq == fst" |
28 rbit_def "rbit == snd" |
28 rbit_def "rbit == snd" |
29 |
29 |
30 receiver_asig_def "receiver_asig == \ |
30 receiver_asig_def "receiver_asig == |
31 \ (UN pkt. {R_pkt(pkt)}, \ |
31 (UN pkt. {R_pkt(pkt)}, |
32 \ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \ |
32 (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), |
33 \ {})" |
33 {})" |
34 |
34 |
35 receiver_trans_def "receiver_trans == \ |
35 receiver_trans_def "receiver_trans == |
36 \ {tr. let s = fst(tr); \ |
36 {tr. let s = fst(tr); |
37 \ t = snd(snd(tr)) \ |
37 t = snd(snd(tr)) |
38 \ in \ |
38 in |
39 \ case fst(snd(tr)) \ |
39 case fst(snd(tr)) |
40 \ of \ |
40 of |
41 \ Next => False | \ |
41 Next => False | |
42 \ S_msg(m) => False | \ |
42 S_msg(m) => False | |
43 \ R_msg(m) => (rq(s) ~= []) & \ |
43 R_msg(m) => (rq(s) ~= []) & |
44 \ m = hd(rq(s)) & \ |
44 m = hd(rq(s)) & |
45 \ rq(t) = tl(rq(s)) & \ |
45 rq(t) = tl(rq(s)) & |
46 \ rbit(t)=rbit(s) | \ |
46 rbit(t)=rbit(s) | |
47 \ S_pkt(pkt) => False | \ |
47 S_pkt(pkt) => False | |
48 \ R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then \ |
48 R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then |
49 \ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else \ |
49 rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else |
50 \ rq(t) =rq(s) & rbit(t)=rbit(s) | \ |
50 rq(t) =rq(s) & rbit(t)=rbit(s) | |
51 \ S_ack(b) => b = rbit(s) & \ |
51 S_ack(b) => b = rbit(s) & |
52 \ rq(t) = rq(s) & \ |
52 rq(t) = rq(s) & |
53 \ rbit(t)=rbit(s) | \ |
53 rbit(t)=rbit(s) | |
54 \ R_ack(b) => False}" |
54 R_ack(b) => False}" |
55 |
55 |
56 receiver_ioa_def "receiver_ioa == \ |
56 receiver_ioa_def "receiver_ioa == |
57 \ (receiver_asig, {([],False)}, receiver_trans)" |
57 (receiver_asig, {([],False)}, receiver_trans)" |
58 |
58 |
59 end |
59 end |