|
1 (* Title: HOL/IOA/NTP/Abschannel.thy |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The (faulty) transmission channel (both directions) |
|
7 *) |
|
8 |
|
9 Abschannel = IOA + Action + |
|
10 |
|
11 datatype ('a)abs_action = S('a) | R('a) |
|
12 |
|
13 consts |
|
14 |
|
15 ch_asig :: 'a abs_action signature |
|
16 |
|
17 ch_trans :: ('a abs_action, 'a multiset)transition set |
|
18 |
|
19 ch_ioa :: ('a abs_action, 'a multiset)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 multiset)transition set |
|
28 rsch_trans :: ('m action, bool multiset)transition set |
|
29 |
|
30 srch_ioa :: ('m action, 'm packet multiset)ioa |
|
31 rsch_ioa :: ('m action, bool multiset)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 ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})" |
|
47 |
|
48 ch_trans_def "ch_trans == |
|
49 {tr. let s = fst(tr); |
|
50 t = snd(snd(tr)) |
|
51 in |
|
52 case fst(snd(tr)) |
|
53 of S(b) => t = addm s b | |
|
54 R(b) => count s b ~= 0 & t = delm s b}" |
|
55 |
|
56 ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)" |
|
57 |
|
58 |
|
59 rsch_actions_def "rsch_actions (akt) == |
|
60 case akt of |
|
61 S_msg(m) => None | |
|
62 R_msg(m) => None | |
|
63 S_pkt(packet) => None | |
|
64 R_pkt(packet) => None | |
|
65 S_ack(b) => Some(S(b)) | |
|
66 R_ack(b) => Some(R(b)) | |
|
67 C_m_s => None | |
|
68 C_m_r => None | |
|
69 C_r_s => None | |
|
70 C_r_r(m) => None" |
|
71 |
|
72 srch_actions_def "srch_actions (akt) == |
|
73 case akt of |
|
74 S_msg(m) => None | |
|
75 R_msg(m) => None | |
|
76 S_pkt(p) => Some(S(p)) | |
|
77 R_pkt(p) => Some(R(p)) | |
|
78 S_ack(b) => None | |
|
79 R_ack(b) => None | |
|
80 C_m_s => None | |
|
81 C_m_r => None | |
|
82 C_r_s => None | |
|
83 C_r_r(m) => None" |
|
84 |
|
85 end |
|
86 |
|
87 |
|
88 |
|
89 |
|
90 |
|
91 |
|
92 |
|
93 |
|
94 |
|
95 |
|
96 |
|
97 |
|
98 |
|
99 |
|
100 |
|
101 |
|
102 |
|
103 |