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