src/HOL/HOLCF/IOA/ABP/Sender.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/ABP/Sender.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Sender.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@3072
     3
*)
mueller@3072
     4
wenzelm@17244
     5
header {* The implementation: sender *}
wenzelm@17244
     6
wenzelm@17244
     7
theory Sender
wenzelm@17244
     8
imports IOA Action Lemmas
wenzelm@17244
     9
begin
mueller@3072
    10
mueller@3072
    11
types
wenzelm@17244
    12
  'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
mueller@3072
    13
wenzelm@25131
    14
definition
wenzelm@25131
    15
  sq :: "'m sender_state => 'm list" where
wenzelm@25131
    16
  "sq = fst"
mueller@3072
    17
wenzelm@25131
    18
definition
wenzelm@25131
    19
  sbit :: "'m sender_state => bool" where
wenzelm@25131
    20
  "sbit = snd"
mueller@3072
    21
wenzelm@25131
    22
definition
wenzelm@25131
    23
  sender_asig :: "'m action signature" where
wenzelm@25131
    24
  "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
wenzelm@25131
    25
                   UN pkt. {S_pkt(pkt)},
wenzelm@25131
    26
                   {})"
mueller@3072
    27
wenzelm@25131
    28
definition
wenzelm@25131
    29
  sender_trans :: "('m action, 'm sender_state)transition set" where
wenzelm@25131
    30
  "sender_trans =
wenzelm@25131
    31
   {tr. let s = fst(tr);
wenzelm@25131
    32
            t = snd(snd(tr))
wenzelm@25131
    33
        in case fst(snd(tr))
wenzelm@25131
    34
        of
wenzelm@25131
    35
        Next     => if sq(s)=[] then t=s else False |
wenzelm@25131
    36
        S_msg(m) => sq(t)=sq(s)@[m]   &
wenzelm@25131
    37
                    sbit(t)=sbit(s)  |
wenzelm@25131
    38
        R_msg(m) => False |
wenzelm@25131
    39
        S_pkt(pkt) => sq(s) ~= []  &
wenzelm@25131
    40
                       hdr(pkt) = sbit(s)      &
wenzelm@25131
    41
                      msg(pkt) = hd(sq(s))    &
wenzelm@25131
    42
                      sq(t) = sq(s)           &
wenzelm@25131
    43
                      sbit(t) = sbit(s) |
wenzelm@25131
    44
        R_pkt(pkt) => False |
wenzelm@25131
    45
        S_ack(b)   => False |
wenzelm@25131
    46
        R_ack(b)   => if b = sbit(s) then
wenzelm@25131
    47
                       sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
wenzelm@25131
    48
                       sq(t)=sq(s) & sbit(t)=sbit(s)}"
wenzelm@25131
    49
  
wenzelm@25131
    50
definition
wenzelm@25131
    51
  sender_ioa :: "('m action, 'm sender_state)ioa" where
wenzelm@25131
    52
  "sender_ioa =
wenzelm@25131
    53
   (sender_asig, {([],True)}, sender_trans,{},{})"
mueller@3072
    54
mueller@3072
    55
end