src/HOLCF/IOA/ABP/Sender.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17244 0b2ff9541727
permissions -rw-r--r--
Merged in license change from Isabelle2004
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Sender.thy
mueller@3072
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@3072
     4
wenzelm@12218
     5
The implementation: sender.
mueller@3072
     6
*)
mueller@3072
     7
mueller@3072
     8
Sender = IOA + Action + List + Lemmas +
mueller@3072
     9
mueller@3072
    10
types
mueller@3072
    11
mueller@3072
    12
'm sender_state = "'m list  *  bool"
mueller@3072
    13
(*                messages     Alternating Bit   *)
mueller@3072
    14
mueller@3072
    15
consts
mueller@3072
    16
mueller@6468
    17
sender_asig   :: "'m action signature"
mueller@3072
    18
sender_trans  :: ('m action, 'm sender_state)transition set
mueller@3072
    19
sender_ioa    :: ('m action, 'm sender_state)ioa
mueller@3072
    20
sq            :: 'm sender_state => 'm list
mueller@3072
    21
sbit          :: 'm sender_state => bool
mueller@3072
    22
mueller@3072
    23
defs
mueller@3072
    24
mueller@3072
    25
sq_def       "sq == fst"
mueller@3072
    26
sbit_def     "sbit == snd"
mueller@3072
    27
mueller@3072
    28
sender_asig_def
mueller@3072
    29
  "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),       
mueller@3072
    30
                  UN pkt. {S_pkt(pkt)},                   
mueller@3072
    31
                  {})"
mueller@3072
    32
mueller@3072
    33
sender_trans_def "sender_trans ==                                     
mueller@3072
    34
 {tr. let s = fst(tr);                                               
mueller@3072
    35
          t = snd(snd(tr))                                           
mueller@3072
    36
      in case fst(snd(tr))                                           
mueller@3072
    37
      of   
mueller@3072
    38
      Next     => if sq(s)=[] then t=s else False |                
mueller@3072
    39
      S_msg(m) => sq(t)=sq(s)@[m]   &                                
mueller@3072
    40
                  sbit(t)=sbit(s)  |                                 
mueller@3072
    41
      R_msg(m) => False |                                            
mueller@3072
    42
      S_pkt(pkt) => sq(s) ~= []  &                                   
mueller@3072
    43
                     hdr(pkt) = sbit(s)      &                        
mueller@3072
    44
                    msg(pkt) = hd(sq(s))    &                   
mueller@3072
    45
                    sq(t) = sq(s)           &                        
mueller@3072
    46
                    sbit(t) = sbit(s) |                              
mueller@3072
    47
      R_pkt(pkt) => False |                                          
mueller@3072
    48
      S_ack(b)   => False |                                          
mueller@3072
    49
      R_ack(b)   => if b = sbit(s) then                              
mueller@3072
    50
                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
mueller@3072
    51
                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
mueller@3072
    52
mueller@3072
    53
sender_ioa_def "sender_ioa == 
mueller@3522
    54
 (sender_asig, {([],True)}, sender_trans,{},{})"
mueller@3072
    55
mueller@3072
    56
end