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