|
1 (* Title: HOLCF/IOA/ABP/Abschannel.thy |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1995 TU Muenchen |
|
5 |
|
6 The transmission channel |
|
7 *) |
|
8 |
|
9 Abschannel = IOA + Action + Lemmas + List + |
|
10 |
|
11 |
|
12 datatype ('a)abs_action = S('a) | R('a) |
|
13 |
|
14 |
|
15 consts |
|
16 |
|
17 ch_asig :: 'a abs_action signature |
|
18 ch_trans :: ('a abs_action, 'a list)transition set |
|
19 ch_ioa :: ('a abs_action, 'a list)ioa |
|
20 |
|
21 rsch_actions :: 'm action => bool abs_action option |
|
22 srch_actions :: "'m action =>(bool * 'm) abs_action option" |
|
23 |
|
24 srch_asig, |
|
25 rsch_asig :: 'm action signature |
|
26 |
|
27 srch_trans :: ('m action, 'm packet list)transition set |
|
28 rsch_trans :: ('m action, bool list)transition set |
|
29 |
|
30 srch_ioa :: ('m action, 'm packet list)ioa |
|
31 rsch_ioa :: ('m action, bool list)ioa |
|
32 |
|
33 |
|
34 defs |
|
35 |
|
36 srch_asig_def "srch_asig == asig_of(srch_ioa)" |
|
37 rsch_asig_def "rsch_asig == asig_of(rsch_ioa)" |
|
38 |
|
39 srch_trans_def "srch_trans == trans_of(srch_ioa)" |
|
40 rsch_trans_def "rsch_trans == trans_of(rsch_ioa)" |
|
41 |
|
42 srch_ioa_def "srch_ioa == rename ch_ioa srch_actions" |
|
43 rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions" |
|
44 |
|
45 |
|
46 (********************************************************** |
|
47 G e n e r i c C h a n n e l |
|
48 *********************************************************) |
|
49 |
|
50 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" |
|
51 |
|
52 ch_trans_def "ch_trans == |
|
53 {tr. let s = fst(tr); |
|
54 t = snd(snd(tr)) |
|
55 in |
|
56 case fst(snd(tr)) |
|
57 of S(b) => ((t = s) | (t = s @ [b])) | |
|
58 R(b) => s ~= [] & |
|
59 b = hd(s) & |
|
60 ((t = s) | (t = tl(s))) }" |
|
61 |
|
62 ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)" |
|
63 |
|
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 |
|
66 *********************************************************) |
|
67 |
|
68 rsch_actions_def "rsch_actions (akt) == |
|
69 case akt of |
|
70 Next => None | |
|
71 S_msg(m) => None | |
|
72 R_msg(m) => None | |
|
73 S_pkt(packet) => None | |
|
74 R_pkt(packet) => None | |
|
75 S_ack(b) => Some(S(b)) | |
|
76 R_ack(b) => Some(R(b))" |
|
77 |
|
78 srch_actions_def "srch_actions (akt) == |
|
79 case akt of |
|
80 Next => None | |
|
81 S_msg(m) => None | |
|
82 R_msg(m) => None | |
|
83 S_pkt(p) => Some(S(p)) | |
|
84 R_pkt(p) => Some(R(p)) | |
|
85 S_ack(b) => None | |
|
86 R_ack(b) => None" |
|
87 |
|
88 |
|
89 end |
|
90 |
|
91 |
|
92 |
|
93 |
|
94 |
|
95 |
|
96 |
|
97 |
|
98 |
|
99 |
|
100 |
|
101 |
|
102 |
|
103 |
|
104 |
|
105 |
|
106 |
|
107 |