src/HOL/HOLCF/IOA/ABP/Receiver.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/ABP/Receiver.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOLCF/IOA/ABP/Receiver.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* The implementation: receiver *}
     6 
     7 theory Receiver
     8 imports IOA Action Lemmas
     9 begin
    10 
    11 types
    12   'm receiver_state = "'m list * bool"  -- {* messages, mode *}
    13 
    14 definition
    15   rq :: "'m receiver_state => 'm list" where
    16   "rq = fst"
    17 
    18 definition
    19   rbit :: "'m receiver_state => bool" where
    20   "rbit = snd"
    21 
    22 definition
    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 
    29 definition
    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 
    52 definition
    53   receiver_ioa :: "('m action, 'm receiver_state)ioa" where
    54   "receiver_ioa =
    55    (receiver_asig, {([],False)}, receiver_trans,{},{})"
    56 
    57 end