1 (* Title: HOL/IOA/example/Channels.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The (faulty) transmission channels (both directions) |
|
7 *) |
|
8 |
|
9 Channels = IOA + Action + Multiset + |
|
10 |
|
11 consts |
|
12 |
|
13 srch_asig, |
|
14 rsch_asig :: "'m action signature" |
|
15 |
|
16 srch_trans :: "('m action, 'm packet multiset)transition set" |
|
17 rsch_trans :: "('m action, bool multiset)transition set" |
|
18 |
|
19 srch_ioa :: "('m action, 'm packet multiset)ioa" |
|
20 rsch_ioa :: "('m action, bool multiset)ioa" |
|
21 |
|
22 defs |
|
23 |
|
24 srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, |
|
25 UN pkt. {R_pkt(pkt)}, |
|
26 {}>" |
|
27 |
|
28 rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, |
|
29 UN b. {R_ack(b)}, |
|
30 {}>" |
|
31 |
|
32 srch_trans_def "srch_trans == |
|
33 {tr. let s = fst(tr); |
|
34 t = snd(snd(tr)) |
|
35 in |
|
36 case fst(snd(tr)) |
|
37 of S_msg(m) => False | |
|
38 R_msg(m) => False | |
|
39 S_pkt(pkt) => t = addm(s, pkt) | |
|
40 R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) | |
|
41 S_ack(b) => False | |
|
42 R_ack(b) => False | |
|
43 C_m_s => False | |
|
44 C_m_r => False | |
|
45 C_r_s => False | |
|
46 C_r_r(m) => False}" |
|
47 |
|
48 rsch_trans_def "rsch_trans == |
|
49 {tr. let s = fst(tr); |
|
50 t = snd(snd(tr)) |
|
51 in |
|
52 case fst(snd(tr)) |
|
53 of |
|
54 S_msg(m) => False | |
|
55 R_msg(m) => False | |
|
56 S_pkt(pkt) => False | |
|
57 R_pkt(pkt) => False | |
|
58 S_ack(b) => t = addm(s,b) | |
|
59 R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) | |
|
60 C_m_s => False | |
|
61 C_m_r => False | |
|
62 C_r_s => False | |
|
63 C_r_r(m) => False}" |
|
64 |
|
65 |
|
66 srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>" |
|
67 rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>" |
|
68 |
|
69 end |
|