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