IOA/example/Channels.thy
changeset 252 a4dc62a46ee4
parent 251 f04b33ce250f
child 253 132634d24019
equal deleted inserted replaced
251:f04b33ce250f 252:a4dc62a46ee4
     1 (*  Title:      HOL/IOA/example/Channels.thy
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow & Konrad Slind
       
     4     Copyright   1994  TU Muenchen
       
     5 
       
     6 The (faulty) transmission channels (both directions)
       
     7 *)
       
     8 
       
     9 Channels = IOA + Action + Multiset +
       
    10 
       
    11 consts
       
    12 
       
    13 srch_asig, 
       
    14 rsch_asig  :: "'m action signature"
       
    15 
       
    16 srch_trans :: "('m action, 'm packet multiset)transition set"
       
    17 rsch_trans :: "('m action, bool multiset)transition set"
       
    18 
       
    19 srch_ioa   :: "('m action, 'm packet multiset)ioa"
       
    20 rsch_ioa   :: "('m action, bool multiset)ioa"
       
    21 
       
    22 defs
       
    23 
       
    24 srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},    
       
    25                             UN pkt. {R_pkt(pkt)},    
       
    26                             {}>"
       
    27 
       
    28 rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, 
       
    29                             UN b. {R_ack(b)}, 
       
    30                             {}>"
       
    31 
       
    32 srch_trans_def "srch_trans ==                                       
       
    33  {tr. let s = fst(tr);                                             
       
    34           t = snd(snd(tr))                                         
       
    35       in                                                           
       
    36       case fst(snd(tr))                                            
       
    37         of S_msg(m) => False |                                     
       
    38            R_msg(m) => False |                                     
       
    39            S_pkt(pkt) => t = addm(s, pkt) |                        
       
    40            R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) |   
       
    41            S_ack(b) => False |                                     
       
    42            R_ack(b) => False |                                     
       
    43            C_m_s => False |                                        
       
    44            C_m_r => False |                                        
       
    45            C_r_s => False |                                        
       
    46            C_r_r(m) => False}"
       
    47 
       
    48 rsch_trans_def "rsch_trans ==                         
       
    49  {tr. let s = fst(tr);                               
       
    50           t = snd(snd(tr))                           
       
    51       in                                             
       
    52       case fst(snd(tr))                              
       
    53       of                                             
       
    54       S_msg(m) => False |                            
       
    55       R_msg(m) => False |                            
       
    56       S_pkt(pkt) => False |                          
       
    57       R_pkt(pkt) => False |                          
       
    58       S_ack(b) => t = addm(s,b) |                    
       
    59       R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) |  
       
    60       C_m_s => False |                               
       
    61       C_m_r => False |                               
       
    62       C_r_s => False |                               
       
    63       C_r_r(m) => False}"
       
    64 
       
    65 
       
    66 srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"
       
    67 rsch_ioa_def "rsch_ioa == <rsch_asig, {{|}}, rsch_trans>"
       
    68 
       
    69 end