1 (* Title: HOLCF/IOA/ABP/Abschannel.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* The transmission channel *} |
|
6 |
|
7 theory Abschannel |
|
8 imports IOA Action Lemmas |
|
9 begin |
|
10 |
|
11 datatype 'a abs_action = S 'a | R 'a |
|
12 |
|
13 |
|
14 (********************************************************** |
|
15 G e n e r i c C h a n n e l |
|
16 *********************************************************) |
|
17 |
|
18 definition |
|
19 ch_asig :: "'a abs_action signature" where |
|
20 "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" |
|
21 |
|
22 definition |
|
23 ch_trans :: "('a abs_action, 'a list)transition set" where |
|
24 "ch_trans = |
|
25 {tr. let s = fst(tr); |
|
26 t = snd(snd(tr)) |
|
27 in |
|
28 case fst(snd(tr)) |
|
29 of S(b) => ((t = s) | (t = s @ [b])) | |
|
30 R(b) => s ~= [] & |
|
31 b = hd(s) & |
|
32 ((t = s) | (t = tl(s)))}" |
|
33 |
|
34 definition |
|
35 ch_ioa :: "('a abs_action, 'a list)ioa" where |
|
36 "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})" |
|
37 |
|
38 |
|
39 (********************************************************** |
|
40 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 |
|
41 *********************************************************) |
|
42 |
|
43 definition |
|
44 rsch_actions :: "'m action => bool abs_action option" where |
|
45 "rsch_actions (akt) = |
|
46 (case akt of |
|
47 Next => None | |
|
48 S_msg(m) => None | |
|
49 R_msg(m) => None | |
|
50 S_pkt(packet) => None | |
|
51 R_pkt(packet) => None | |
|
52 S_ack(b) => Some(S(b)) | |
|
53 R_ack(b) => Some(R(b)))" |
|
54 |
|
55 definition |
|
56 srch_actions :: "'m action =>(bool * 'm) abs_action option" where |
|
57 "srch_actions akt = |
|
58 (case akt of |
|
59 Next => None | |
|
60 S_msg(m) => None | |
|
61 R_msg(m) => None | |
|
62 S_pkt(p) => Some(S(p)) | |
|
63 R_pkt(p) => Some(R(p)) | |
|
64 S_ack(b) => None | |
|
65 R_ack(b) => None)" |
|
66 |
|
67 definition |
|
68 srch_ioa :: "('m action, 'm packet list)ioa" where |
|
69 "srch_ioa = rename ch_ioa srch_actions" |
|
70 definition |
|
71 rsch_ioa :: "('m action, bool list)ioa" where |
|
72 "rsch_ioa = rename ch_ioa rsch_actions" |
|
73 |
|
74 definition |
|
75 srch_asig :: "'m action signature" where |
|
76 "srch_asig = asig_of(srch_ioa)" |
|
77 |
|
78 definition |
|
79 rsch_asig :: "'m action signature" where |
|
80 "rsch_asig = asig_of(rsch_ioa)" |
|
81 |
|
82 definition |
|
83 srch_trans :: "('m action, 'm packet list)transition set" where |
|
84 "srch_trans = trans_of(srch_ioa)" |
|
85 definition |
|
86 rsch_trans :: "('m action, bool list)transition set" where |
|
87 "rsch_trans = trans_of(rsch_ioa)" |
|
88 |
|
89 end |
|