1(*  Title:      HOL/HOLCF/IOA/ABP/Receiver.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>The implementation: receiver\<close>
6
7theory Receiver
8imports IOA.IOA Action Lemmas
9begin
10
11type_synonym
12  'm receiver_state = "'m list * bool"  \<comment> \<open>messages, mode\<close>
13
14definition
15  rq :: "'m receiver_state => 'm list" where
16  "rq = fst"
17
18definition
19  rbit :: "'m receiver_state => bool" where
20  "rbit = snd"
21
22definition
23  receiver_asig :: "'m action signature" where
24  "receiver_asig =
25    (UN pkt. {R_pkt(pkt)},
26    (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
27    {})"
28
29definition
30  receiver_trans :: "('m action, 'm receiver_state)transition set" where
31  "receiver_trans =
32   {tr. let s = fst(tr);
33            t = snd(snd(tr))
34        in
35        case fst(snd(tr))
36        of
37        Next    =>  False |
38        S_msg(m) => False |
39        R_msg(m) => (rq(s) ~= [])  &
40                     m = hd(rq(s))  &
41                     rq(t) = tl(rq(s))   &
42                    rbit(t)=rbit(s)  |
43        S_pkt(pkt) => False |
44        R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
45                           rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
46                           rq(t) =rq(s) & rbit(t)=rbit(s)  |
47        S_ack(b) => b = rbit(s)                        &
48                        rq(t) = rq(s)                    &
49                        rbit(t)=rbit(s) |
50        R_ack(b) => False}"
51
52definition
53  receiver_ioa :: "('m action, 'm receiver_state)ioa" where
54  "receiver_ioa =
55   (receiver_asig, {([],False)}, receiver_trans,{},{})"
56
57end
58