1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,55 @@
     1.4 +(*  Title:      HOLCF/IOA/ABP/Sender.thy
     1.5 +    Author:     Olaf Müller
     1.6 +*)
     1.7 +
     1.8 +header {* The implementation: sender *}
     1.9 +
    1.10 +theory Sender
    1.11 +imports IOA Action Lemmas
    1.12 +begin
    1.13 +
    1.14 +types
    1.15 +  'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
    1.16 +
    1.17 +definition
    1.18 +  sq :: "'m sender_state => 'm list" where
    1.19 +  "sq = fst"
    1.20 +
    1.21 +definition
    1.22 +  sbit :: "'m sender_state => bool" where
    1.23 +  "sbit = snd"
    1.24 +
    1.25 +definition
    1.26 +  sender_asig :: "'m action signature" where
    1.27 +  "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
    1.28 +                   UN pkt. {S_pkt(pkt)},
    1.29 +                   {})"
    1.30 +
    1.31 +definition
    1.32 +  sender_trans :: "('m action, 'm sender_state)transition set" where
    1.33 +  "sender_trans =
    1.34 +   {tr. let s = fst(tr);
    1.35 +            t = snd(snd(tr))
    1.36 +        in case fst(snd(tr))
    1.37 +        of
    1.38 +        Next     => if sq(s)=[] then t=s else False |
    1.39 +        S_msg(m) => sq(t)=sq(s)@[m]   &
    1.40 +                    sbit(t)=sbit(s)  |
    1.41 +        R_msg(m) => False |
    1.42 +        S_pkt(pkt) => sq(s) ~= []  &
    1.43 +                       hdr(pkt) = sbit(s)      &
    1.44 +                      msg(pkt) = hd(sq(s))    &
    1.45 +                      sq(t) = sq(s)           &
    1.46 +                      sbit(t) = sbit(s) |
    1.47 +        R_pkt(pkt) => False |
    1.48 +        S_ack(b)   => False |
    1.49 +        R_ack(b)   => if b = sbit(s) then
    1.50 +                       sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
    1.51 +                       sq(t)=sq(s) & sbit(t)=sbit(s)}"
    1.52 +  
    1.53 +definition
    1.54 +  sender_ioa :: "('m action, 'm sender_state)ioa" where
    1.55 +  "sender_ioa =
    1.56 +   (sender_asig, {([],True)}, sender_trans,{},{})"
    1.57 +
    1.58 +end