src/HOL/IOA/ABP/Spec.thy
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1376 92f83b9d17e1
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
mueller@1139
     1
(*  Title:      HOL/IOA/example/Spec.thy
nipkow@1050
     2
    ID:         $Id$
mueller@1139
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@1139
     4
    Copyright   1994  TU Muenchen
nipkow@1050
     5
nipkow@1050
     6
The specification of reliable transmission
nipkow@1050
     7
*)
nipkow@1050
     8
nipkow@1050
     9
Spec = List + IOA + Action +
nipkow@1050
    10
nipkow@1050
    11
consts
nipkow@1050
    12
clasohm@1376
    13
spec_sig   :: 'm action signature
clasohm@1376
    14
spec_trans :: ('m action, 'm list)transition set
clasohm@1376
    15
spec_ioa   :: ('m action, 'm list)ioa
nipkow@1050
    16
nipkow@1050
    17
defs
nipkow@1050
    18
clasohm@1151
    19
sig_def "spec_sig == (UN m.{S_msg(m)}, 
clasohm@1151
    20
                     UN m.{R_msg(m)} Un {Next}, 
clasohm@1151
    21
                     {})"
nipkow@1050
    22
clasohm@1151
    23
trans_def "spec_trans ==                           
clasohm@1151
    24
 {tr. let s = fst(tr);                            
clasohm@1151
    25
          t = snd(snd(tr))                        
clasohm@1151
    26
      in                                          
clasohm@1151
    27
      case fst(snd(tr))                           
clasohm@1151
    28
      of   
clasohm@1151
    29
      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
clasohm@1151
    30
      S_msg(m) => t = s@[m]  |                    
clasohm@1151
    31
      R_msg(m) => s = (m#t)  |                    
clasohm@1151
    32
      S_pkt(pkt) => False |                    
clasohm@1151
    33
      R_pkt(pkt) => False |                    
clasohm@1151
    34
      S_ack(b) => False |                      
clasohm@1151
    35
      R_ack(b) => False}"
nipkow@1050
    36
nipkow@1050
    37
ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
nipkow@1050
    38
nipkow@1050
    39
end