1(*  Title:      HOL/HOLCF/IOA/NTP/Spec.thy
2    Author:     Tobias Nipkow & Konrad Slind
3*)
4
5section \<open>The specification of reliable transmission\<close>
6
7theory Spec
8imports IOA.IOA Action
9begin
10
11definition
12  spec_sig :: "'m action signature" where
13  sig_def: "spec_sig = (\<Union>m.{S_msg(m)}, 
14                        \<Union>m.{R_msg(m)}, 
15                        {})"
16
17definition
18  spec_trans :: "('m action, 'm list)transition set" where
19  trans_def: "spec_trans =
20   {tr. let s = fst(tr);                            
21            t = snd(snd(tr))                        
22        in                                          
23        case fst(snd(tr))                           
24        of                                          
25        S_msg(m) \<Rightarrow> t = s@[m]  |                    
26        R_msg(m) \<Rightarrow> s = (m#t)  |                    
27        S_pkt(pkt) \<Rightarrow> False |                    
28        R_pkt(pkt) \<Rightarrow> False |                    
29        S_ack(b) \<Rightarrow> False |                      
30        R_ack(b) \<Rightarrow> False |                      
31        C_m_s \<Rightarrow> False |                            
32        C_m_r \<Rightarrow> False |                            
33        C_r_s \<Rightarrow> False |                            
34        C_r_r(m) \<Rightarrow> False}"
35
36definition
37  spec_ioa :: "('m action, 'm list)ioa" where
38  ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans,{},{})"
39
40end
41