|
1139
|
1 |
(* Title: HOL/IOA/example/Receiver.thy
|
|
1050
|
2 |
ID: $Id$
|
|
1139
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
|
4 |
Copyright 1994 TU Muenchen
|
|
1050
|
5 |
|
|
|
6 |
The implementation: receiver
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Receiver = List + IOA + Action + Lemmas +
|
|
|
10 |
|
|
|
11 |
types
|
|
|
12 |
|
|
|
13 |
'm receiver_state
|
|
|
14 |
= "'m list * bool"
|
|
|
15 |
(* messages mode *)
|
|
|
16 |
|
|
|
17 |
consts
|
|
|
18 |
|
|
1376
|
19 |
receiver_asig :: 'm action signature
|
|
|
20 |
receiver_trans:: ('m action, 'm receiver_state)transition set
|
|
|
21 |
receiver_ioa :: ('m action, 'm receiver_state)ioa
|
|
|
22 |
rq :: 'm receiver_state => 'm list
|
|
|
23 |
rbit :: 'm receiver_state => bool
|
|
1050
|
24 |
|
|
|
25 |
defs
|
|
|
26 |
|
|
|
27 |
rq_def "rq == fst"
|
|
|
28 |
rbit_def "rbit == snd"
|
|
|
29 |
|
|
1151
|
30 |
receiver_asig_def "receiver_asig ==
|
|
|
31 |
(UN pkt. {R_pkt(pkt)},
|
|
|
32 |
(UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
|
|
|
33 |
{})"
|
|
1050
|
34 |
|
|
1151
|
35 |
receiver_trans_def "receiver_trans ==
|
|
|
36 |
{tr. let s = fst(tr);
|
|
|
37 |
t = snd(snd(tr))
|
|
|
38 |
in
|
|
|
39 |
case fst(snd(tr))
|
|
|
40 |
of
|
|
|
41 |
Next => False |
|
|
|
42 |
S_msg(m) => False |
|
|
|
43 |
R_msg(m) => (rq(s) ~= []) &
|
|
1476
|
44 |
m = hd(rq(s)) &
|
|
|
45 |
rq(t) = tl(rq(s)) &
|
|
1151
|
46 |
rbit(t)=rbit(s) |
|
|
|
47 |
S_pkt(pkt) => False |
|
|
|
48 |
R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
|
|
1476
|
49 |
rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
|
|
|
50 |
rq(t) =rq(s) & rbit(t)=rbit(s) |
|
|
1151
|
51 |
S_ack(b) => b = rbit(s) &
|
|
|
52 |
rq(t) = rq(s) &
|
|
|
53 |
rbit(t)=rbit(s) |
|
|
|
54 |
R_ack(b) => False}"
|
|
1050
|
55 |
|
|
1151
|
56 |
receiver_ioa_def "receiver_ioa ==
|
|
|
57 |
(receiver_asig, {([],False)}, receiver_trans)"
|
|
1050
|
58 |
|
|
|
59 |
end
|