src/HOL/IOA/ABP/Receiver.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1476 608483c2122a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/IOA/example/Receiver.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 The implementation: receiver
     7 *)
     8 
     9 Receiver = List + IOA + Action + Lemmas +
    10 
    11 types 
    12 
    13 'm receiver_state
    14 = "'m list * bool"
    15 (* messages  mode *)
    16 
    17 consts
    18 
    19   receiver_asig :: 'm action signature
    20   receiver_trans:: ('m action, 'm receiver_state)transition set
    21   receiver_ioa  :: ('m action, 'm receiver_state)ioa
    22   rq            :: 'm receiver_state => 'm list
    23   rbit          :: 'm receiver_state => bool
    24 
    25 defs
    26 
    27 rq_def       "rq == fst"
    28 rbit_def     "rbit == snd"
    29 
    30 receiver_asig_def "receiver_asig ==            
    31  (UN pkt. {R_pkt(pkt)},                       
    32   (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),   
    33   {})"
    34 
    35 receiver_trans_def "receiver_trans ==                                    
    36  {tr. let s = fst(tr);                                                  
    37           t = snd(snd(tr))                                              
    38       in                                                                
    39       case fst(snd(tr))                                                 
    40       of   
    41       Next    =>  False |     
    42       S_msg(m) => False |                                               
    43       R_msg(m) => (rq(s) ~= [])  &                                     
    44                    m = hd(rq(s))  &                             
    45                    rq(t) = tl(rq(s))   &                              
    46                   rbit(t)=rbit(s)  |                                 
    47       S_pkt(pkt) => False |                                          
    48       R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
    49                          rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
    50                          rq(t) =rq(s) & rbit(t)=rbit(s)  |   
    51       S_ack(b) => b = rbit(s)                        &               
    52                       rq(t) = rq(s)                    &             
    53                       rbit(t)=rbit(s) |                              
    54       R_ack(b) => False}"
    55 
    56 receiver_ioa_def "receiver_ioa == 
    57  (receiver_asig, {([],False)}, receiver_trans)"
    58 
    59 end