1(* Title: HOL/HOLCF/IOA/ABP/Spec.thy 2 Author: Olaf M��ller 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 = (UN m.{S_msg(m)}, 14 UN m.{R_msg(m)} Un {Next}, 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 Next => t=s | \<comment> \<open>Note that there is condition as in Sender\<close> 26 S_msg(m) => t = s@[m] | 27 R_msg(m) => s = (m#t) | 28 S_pkt(pkt) => False | 29 R_pkt(pkt) => False | 30 S_ack(b) => False | 31 R_ack(b) => False}" 32 33definition 34 spec_ioa :: "('m action, 'm list)ioa" where 35 ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans, {}, {})" 36 37end 38