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