src/HOLCF/IOA/ABP/Spec.thy
author nipkow
Mon, 12 Aug 2002 17:48:15 +0200
changeset 13490 44bdc150211b
parent 12218 6597093b77e7
child 14981 e73f8140af78
permissions -rw-r--r--
Added Mi and Max on sets, hid Min and Pls on numerals.

(*  Title:      HOLCF/IOA/ABP/Spec.thy
    ID:         $Id$
    Author:     Olaf Müller
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

The specification of reliable transmission.
*)

Spec = List + IOA + Action +

consts

spec_sig   :: "'m action signature"
spec_trans :: ('m action, 'm list)transition set
spec_ioa   :: ('m action, 'm list)ioa

defs

sig_def "spec_sig == (UN m.{S_msg(m)}, 
                     UN m.{R_msg(m)} Un {Next}, 
                     {})"

trans_def "spec_trans ==                           
 {tr. let s = fst(tr);                            
          t = snd(snd(tr))                        
      in                                          
      case fst(snd(tr))                           
      of   
      Next =>  t=s |\ (* Note that there is condition as in Sender *) 
      S_msg(m) => t = s@[m]  |                    
      R_msg(m) => s = (m#t)  |                    
      S_pkt(pkt) => False |                    
      R_pkt(pkt) => False |                    
      S_ack(b) => False |                      
      R_ack(b) => False}"

ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"

end