src/HOL/HOLCF/IOA/NTP/Receiver.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 61032 b57df8eecad6
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/NTP/Receiver.thy
     2     Author:     Tobias Nipkow & Konrad Slind
     3 *)
     4 
     5 section {* The implementation: receiver *}
     6 
     7 theory Receiver
     8 imports IOA Action
     9 begin
    10 
    11 type_synonym
    12 
    13 'm receiver_state
    14 = "'m list * bool multiset * 'm packet multiset * bool * bool"
    15 (* messages  #replies        #received            header mode *)
    16 
    17 definition rq :: "'m receiver_state => 'm list" where "rq == fst"
    18 definition rsent :: "'m receiver_state => bool multiset" where "rsent == fst o snd"
    19 definition rrcvd :: "'m receiver_state => 'm packet multiset" where "rrcvd == fst o snd o snd"
    20 definition rbit :: "'m receiver_state => bool" where "rbit == fst o snd o snd o snd"
    21 definition rsending :: "'m receiver_state => bool" where "rsending == snd o snd o snd o snd"
    22 
    23 definition
    24   receiver_asig :: "'m action signature" where
    25   "receiver_asig =
    26    (UN pkt. {R_pkt(pkt)},
    27     (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
    28     insert C_m_r (UN m. {C_r_r(m)}))"
    29 
    30 definition
    31   receiver_trans:: "('m action, 'm receiver_state)transition set" where
    32 "receiver_trans =
    33  {tr. let s = fst(tr);
    34           t = snd(snd(tr))
    35       in
    36       case fst(snd(tr))
    37       of
    38       S_msg(m) => False |
    39       R_msg(m) => rq(s) = (m # rq(t))   &
    40                   rsent(t)=rsent(s)     &
    41                   rrcvd(t)=rrcvd(s)     &
    42                   rbit(t)=rbit(s)       &
    43                   rsending(t)=rsending(s) |
    44       S_pkt(pkt) => False |
    45       R_pkt(pkt) => rq(t) = rq(s)                        &
    46                        rsent(t) = rsent(s)                  &
    47                        rrcvd(t) = addm (rrcvd s) pkt        &
    48                        rbit(t) = rbit(s)                    &
    49                        rsending(t) = rsending(s) |
    50       S_ack(b) => b = rbit(s)                        &
    51                      rq(t) = rq(s)                      &
    52                      rsent(t) = addm (rsent s) (rbit s) &
    53                      rrcvd(t) = rrcvd(s)                &
    54                      rbit(t)=rbit(s)                    &
    55                      rsending(s)                        &
    56                      rsending(t) |
    57       R_ack(b) => False |
    58       C_m_s => False |
    59  C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
    60              rq(t) = rq(s)                        &
    61              rsent(t)=rsent(s)                    &
    62              rrcvd(t)=rrcvd(s)                    &
    63              rbit(t)=rbit(s)                      &
    64              rsending(s)                          &
    65              ~rsending(t) |
    66     C_r_s => False |
    67  C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
    68              count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &
    69              rq(t) = rq(s)@[m]                         &
    70              rsent(t)=rsent(s)                         &
    71              rrcvd(t)=rrcvd(s)                         &
    72              rbit(t) = (~rbit(s))                      &
    73              ~rsending(s)                              &
    74              rsending(t)}"
    75 
    76 definition
    77   receiver_ioa  :: "('m action, 'm receiver_state)ioa" where
    78   "receiver_ioa =
    79     (receiver_asig, {([],{|},{|},False,False)}, receiver_trans,{},{})"
    80 
    81 lemma in_receiver_asig:
    82   "S_msg(m) ~: actions(receiver_asig)"
    83   "R_msg(m) : actions(receiver_asig)"
    84   "S_pkt(pkt) ~: actions(receiver_asig)"
    85   "R_pkt(pkt) : actions(receiver_asig)"
    86   "S_ack(b) : actions(receiver_asig)"
    87   "R_ack(b) ~: actions(receiver_asig)"
    88   "C_m_s ~: actions(receiver_asig)"
    89   "C_m_r : actions(receiver_asig)"
    90   "C_r_s ~: actions(receiver_asig)"
    91   "C_r_r(m) : actions(receiver_asig)"
    92   by (simp_all add: receiver_asig_def actions_def asig_projections)
    93 
    94 lemmas receiver_projections = rq_def rsent_def rrcvd_def rbit_def rsending_def
    95 
    96 end