src/HOLCF/IOA/ABP/Abschannel.thy
author mueller
Wed Apr 30 11:24:14 1997 +0200 (1997-04-30)
changeset 3072 a31419014be5
child 3522 a34c20f4bf44
permissions -rw-r--r--
Old ABP files now running under the IOA meta theory based on HOLCF;
mueller@3072
     1
(*  Title:      HOLCF/IOA/ABP/Abschannel.thy
mueller@3072
     2
    ID:         $Id$
mueller@3072
     3
    Author:     Olaf Mueller
mueller@3072
     4
    Copyright   1995  TU Muenchen
mueller@3072
     5
mueller@3072
     6
The transmission channel 
mueller@3072
     7
*)
mueller@3072
     8
mueller@3072
     9
Abschannel = IOA + Action + Lemmas + List +
mueller@3072
    10
mueller@3072
    11
mueller@3072
    12
datatype ('a)abs_action =   S('a) | R('a)
mueller@3072
    13
mueller@3072
    14
mueller@3072
    15
consts
mueller@3072
    16
 
mueller@3072
    17
ch_asig  :: 'a abs_action signature
mueller@3072
    18
ch_trans :: ('a abs_action, 'a list)transition set
mueller@3072
    19
ch_ioa   :: ('a abs_action, 'a list)ioa
mueller@3072
    20
mueller@3072
    21
rsch_actions  :: 'm action => bool abs_action option
mueller@3072
    22
srch_actions  :: "'m action =>(bool * 'm) abs_action option"
mueller@3072
    23
mueller@3072
    24
srch_asig, 
mueller@3072
    25
rsch_asig  :: 'm action signature
mueller@3072
    26
 
mueller@3072
    27
srch_trans :: ('m action, 'm packet list)transition set
mueller@3072
    28
rsch_trans :: ('m action, bool list)transition set
mueller@3072
    29
mueller@3072
    30
srch_ioa   :: ('m action, 'm packet list)ioa
mueller@3072
    31
rsch_ioa   :: ('m action, bool list)ioa   
mueller@3072
    32
mueller@3072
    33
mueller@3072
    34
defs
mueller@3072
    35
mueller@3072
    36
srch_asig_def "srch_asig == asig_of(srch_ioa)"
mueller@3072
    37
rsch_asig_def "rsch_asig == asig_of(rsch_ioa)"
mueller@3072
    38
mueller@3072
    39
srch_trans_def "srch_trans == trans_of(srch_ioa)"  
mueller@3072
    40
rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
mueller@3072
    41
mueller@3072
    42
srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
mueller@3072
    43
rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
mueller@3072
    44
mueller@3072
    45
  
mueller@3072
    46
(**********************************************************
mueller@3072
    47
       G e n e r i c   C h a n n e l
mueller@3072
    48
 *********************************************************)
mueller@3072
    49
  
mueller@3072
    50
ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
mueller@3072
    51
mueller@3072
    52
ch_trans_def "ch_trans ==                                       
mueller@3072
    53
 {tr. let s = fst(tr);                                         
mueller@3072
    54
          t = snd(snd(tr))                                     
mueller@3072
    55
      in                                                       
mueller@3072
    56
      case fst(snd(tr))                                        
mueller@3072
    57
        of S(b) => ((t = s) | (t = s @ [b]))  |                
mueller@3072
    58
           R(b) => s ~= [] &                                   
mueller@3072
    59
                    b = hd(s) &                                 
mueller@3072
    60
                    ((t = s) | (t = tl(s)))    }"
mueller@3072
    61
  
mueller@3072
    62
ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
mueller@3072
    63
mueller@3072
    64
(**********************************************************
mueller@3072
    65
  C o n c r e t e  C h a n n e l s  b y   R e n a m i n g 
mueller@3072
    66
 *********************************************************)
mueller@3072
    67
  
mueller@3072
    68
rsch_actions_def "rsch_actions (akt) ==                      
mueller@3072
    69
            case akt of   
mueller@3072
    70
           Next    =>  None |          
mueller@3072
    71
           S_msg(m) => None |         
mueller@3072
    72
            R_msg(m) => None |         
mueller@3072
    73
           S_pkt(packet) => None |    
mueller@3072
    74
            R_pkt(packet) => None |    
mueller@3072
    75
            S_ack(b) => Some(S(b)) |   
mueller@3072
    76
            R_ack(b) => Some(R(b))"
mueller@3072
    77
mueller@3072
    78
srch_actions_def "srch_actions (akt) ==                      
mueller@3072
    79
            case akt of   
mueller@3072
    80
            Next    =>  None |          
mueller@3072
    81
           S_msg(m) => None |         
mueller@3072
    82
            R_msg(m) => None |         
mueller@3072
    83
           S_pkt(p) => Some(S(p)) |   
mueller@3072
    84
            R_pkt(p) => Some(R(p)) |   
mueller@3072
    85
            S_ack(b) => None |         
mueller@3072
    86
            R_ack(b) => None"
mueller@3072
    87
mueller@3072
    88
mueller@3072
    89
end  
mueller@3072
    90
mueller@3072
    91
mueller@3072
    92
mueller@3072
    93
mueller@3072
    94
mueller@3072
    95
mueller@3072
    96
mueller@3072
    97
mueller@3072
    98
mueller@3072
    99
mueller@3072
   100
mueller@3072
   101
mueller@3072
   102
mueller@3072
   103
mueller@3072
   104
mueller@3072
   105
mueller@3072
   106
mueller@3072
   107