9 rsch_trans :: "('m action, bool multiset)transition set" |
17 rsch_trans :: "('m action, bool multiset)transition set" |
10 |
18 |
11 srch_ioa :: "('m action, 'm packet multiset)ioa" |
19 srch_ioa :: "('m action, 'm packet multiset)ioa" |
12 rsch_ioa :: "('m action, bool multiset)ioa" |
20 rsch_ioa :: "('m action, bool multiset)ioa" |
13 |
21 |
14 rules |
22 defs |
15 |
23 |
16 srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \ |
24 srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \ |
17 \ UN pkt. {R_pkt(pkt)}, \ |
25 \ UN pkt. {R_pkt(pkt)}, \ |
18 \ {}>" |
26 \ {}>" |
19 |
27 |
20 rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \ |
28 rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \ |
21 \ UN b. {R_ack(b)}, \ |
29 \ UN b. {R_ack(b)}, \ |
22 \ {}>" |
30 \ {}>" |
23 |
31 |
24 srch_trans_def "srch_trans == \ |
32 srch_trans_def "srch_trans == \ |
25 \ {tr. let s = fst(tr); \ |
33 \ {tr. let s = fst(tr); \ |
26 \ t = snd(snd(tr)) \ |
34 \ t = snd(snd(tr)) \ |
27 \ in \ |
35 \ in \ |
28 \ case fst(snd(tr)) \ |
36 \ case fst(snd(tr)) \ |
29 \ of S_msg(m) => False | \ |
37 \ of S_msg(m) => False | \ |
30 \ R_msg(m) => False | \ |
38 \ R_msg(m) => False | \ |
31 \ S_pkt(pkt) => t = addm(s, pkt) | \ |
39 \ S_pkt(pkt) => t = addm(s, pkt) | \ |
32 \ R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) | \ |
40 \ R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) | \ |
33 \ S_ack(b) => False | \ |
41 \ S_ack(b) => False | \ |
34 \ R_ack(b) => False | \ |
42 \ R_ack(b) => False | \ |
35 \ C_m_s => False | \ |
43 \ C_m_s => False | \ |
36 \ C_m_r => False | \ |
44 \ C_m_r => False | \ |
37 \ C_r_s => False | \ |
45 \ C_r_s => False | \ |
38 \ C_r_r(m) => False}" |
46 \ C_r_r(m) => False}" |
39 |
47 |
40 rsch_trans_def "rsch_trans == \ |
48 rsch_trans_def "rsch_trans == \ |
41 \ {tr. let s = fst(tr); \ |
49 \ {tr. let s = fst(tr); \ |
42 \ t = snd(snd(tr)) \ |
50 \ t = snd(snd(tr)) \ |
43 \ in \ |
51 \ in \ |
44 \ case fst(snd(tr)) \ |
52 \ case fst(snd(tr)) \ |
45 \ of \ |
53 \ of \ |
46 \ S_msg(m) => False | \ |
54 \ S_msg(m) => False | \ |
47 \ R_msg(m) => False | \ |
55 \ R_msg(m) => False | \ |
48 \ S_pkt(pkt) => False | \ |
56 \ S_pkt(pkt) => False | \ |
49 \ R_pkt(pkt) => False | \ |
57 \ R_pkt(pkt) => False | \ |
50 \ S_ack(b) => t = addm(s,b) | \ |
58 \ S_ack(b) => t = addm(s,b) | \ |
51 \ R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) | \ |
59 \ R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) | \ |
52 \ C_m_s => False | \ |
60 \ C_m_s => False | \ |
53 \ C_m_r => False | \ |
61 \ C_m_r => False | \ |
54 \ C_r_s => False | \ |
62 \ C_r_s => False | \ |
55 \ C_r_r(m) => False}" |
63 \ C_r_r(m) => False}" |
56 |
64 |
57 |
65 |
58 srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>" |
66 srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>" |
59 rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>" |
67 rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>" |