47 G e n e r i c C h a n n e l |
47 G e n e r i c C h a n n e l |
48 *********************************************************) |
48 *********************************************************) |
49 |
49 |
50 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" |
50 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" |
51 |
51 |
52 ch_trans_def "ch_trans == \ |
52 ch_trans_def "ch_trans == |
53 \ {tr. let s = fst(tr); \ |
53 {tr. let s = fst(tr); |
54 \ t = snd(snd(tr)) \ |
54 t = snd(snd(tr)) |
55 \ in \ |
55 in |
56 \ case fst(snd(tr)) \ |
56 case fst(snd(tr)) |
57 \ of S(b) => ((t = s) | (t = s @ [b])) | \ |
57 of S(b) => ((t = s) | (t = s @ [b])) | |
58 \ R(b) => s ~= [] & \ |
58 R(b) => s ~= [] & |
59 \ b = hd(s) & \ |
59 b = hd(s) & |
60 \ ((t = s) | (t = tl(s))) }" |
60 ((t = s) | (t = tl(s))) }" |
61 |
61 |
62 ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)" |
62 ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)" |
63 |
63 |
64 (********************************************************** |
64 (********************************************************** |
65 C o n c r e t e C h a n n e l s b y R e n a m i n g |
65 C o n c r e t e C h a n n e l s b y R e n a m i n g |
66 *********************************************************) |
66 *********************************************************) |
67 |
67 |
68 rsch_actions_def "rsch_actions (akt) == \ |
68 rsch_actions_def "rsch_actions (akt) == |
69 \ case akt of \ |
69 case akt of |
70 \ Next => None | \ |
70 Next => None | |
71 \ S_msg(m) => None | \ |
71 S_msg(m) => None | |
72 \ R_msg(m) => None | \ |
72 R_msg(m) => None | |
73 \ S_pkt(packet) => None | \ |
73 S_pkt(packet) => None | |
74 \ R_pkt(packet) => None | \ |
74 R_pkt(packet) => None | |
75 \ S_ack(b) => Some(S(b)) | \ |
75 S_ack(b) => Some(S(b)) | |
76 \ R_ack(b) => Some(R(b))" |
76 R_ack(b) => Some(R(b))" |
77 |
77 |
78 srch_actions_def "srch_actions (akt) == \ |
78 srch_actions_def "srch_actions (akt) == |
79 \ case akt of \ |
79 case akt of |
80 \ Next => None | \ |
80 Next => None | |
81 \ S_msg(m) => None | \ |
81 S_msg(m) => None | |
82 \ R_msg(m) => None | \ |
82 R_msg(m) => None | |
83 \ S_pkt(p) => Some(S(p)) | \ |
83 S_pkt(p) => Some(S(p)) | |
84 \ R_pkt(p) => Some(R(p)) | \ |
84 R_pkt(p) => Some(R(p)) | |
85 \ S_ack(b) => None | \ |
85 S_ack(b) => None | |
86 \ R_ack(b) => None" |
86 R_ack(b) => None" |
87 |
87 |
88 |
88 |
89 end |
89 end |
90 |
90 |
91 |
91 |