src/HOLCF/IOA/ABP/Spec.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
     1 (*  Title:      HOLCF/IOA/ABP/Spec.thy
     2     ID:         $Id$
     3     Author:     Olaf Müller
     4 
     5 The specification of reliable transmission.
     6 *)
     7 
     8 Spec = List + IOA + Action +
     9 
    10 consts
    11 
    12 spec_sig   :: "'m action signature"
    13 spec_trans :: ('m action, 'm list)transition set
    14 spec_ioa   :: ('m action, 'm list)ioa
    15 
    16 defs
    17 
    18 sig_def "spec_sig == (UN m.{S_msg(m)}, 
    19                      UN m.{R_msg(m)} Un {Next}, 
    20                      {})"
    21 
    22 trans_def "spec_trans ==                           
    23  {tr. let s = fst(tr);                            
    24           t = snd(snd(tr))                        
    25       in                                          
    26       case fst(snd(tr))                           
    27       of   
    28       Next =>  t=s |\ (* Note that there is condition as in Sender *) 
    29       S_msg(m) => t = s@[m]  |                    
    30       R_msg(m) => s = (m#t)  |                    
    31       S_pkt(pkt) => False |                    
    32       R_pkt(pkt) => False |                    
    33       S_ack(b) => False |                      
    34       R_ack(b) => False}"
    35 
    36 ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
    37 
    38 end