1(* Title: HOL/HOLCF/IOA/NTP/Sender.thy 2 Author: Tobias Nipkow & Konrad Slind 3*) 4 5section \<open>The implementation: sender\<close> 6 7theory Sender 8imports IOA.IOA Action 9begin 10 11type_synonym 12'm sender_state = "'m list * bool multiset * bool multiset * bool * bool" 13(* messages #sent #received header mode *) 14 15definition sq :: "'m sender_state => 'm list" where "sq = fst" 16definition ssent :: "'m sender_state => bool multiset" where "ssent = fst \<circ> snd" 17definition srcvd :: "'m sender_state => bool multiset" where "srcvd = fst \<circ> snd \<circ> snd" 18definition sbit :: "'m sender_state => bool" where "sbit = fst \<circ> snd \<circ> snd \<circ> snd" 19definition ssending :: "'m sender_state => bool" where "ssending = snd \<circ> snd \<circ> snd \<circ> snd" 20 21definition 22 sender_asig :: "'m action signature" where 23 "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), 24 UN pkt. {S_pkt(pkt)}, 25 {C_m_s,C_r_s})" 26 27definition 28 sender_trans :: "('m action, 'm sender_state)transition set" where 29 "sender_trans = 30 {tr. let s = fst(tr); 31 t = snd(snd(tr)) 32 in case fst(snd(tr)) 33 of 34 S_msg(m) => sq(t)=sq(s)@[m] \<and> 35 ssent(t)=ssent(s) \<and> 36 srcvd(t)=srcvd(s) \<and> 37 sbit(t)=sbit(s) \<and> 38 ssending(t)=ssending(s) | 39 R_msg(m) => False | 40 S_pkt(pkt) => hdr(pkt) = sbit(s) \<and> 41 (\<exists>Q. sq(s) = (msg(pkt)#Q)) \<and> 42 sq(t) = sq(s) \<and> 43 ssent(t) = addm (ssent s) (sbit s) \<and> 44 srcvd(t) = srcvd(s) \<and> 45 sbit(t) = sbit(s) \<and> 46 ssending(s) \<and> 47 ssending(t) | 48 R_pkt(pkt) => False | 49 S_ack(b) => False | 50 R_ack(b) => sq(t)=sq(s) \<and> 51 ssent(t)=ssent(s) \<and> 52 srcvd(t) = addm (srcvd s) b \<and> 53 sbit(t)=sbit(s) \<and> 54 ssending(t)=ssending(s) | 55 C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) \<and> 56 sq(t)=sq(s) \<and> 57 ssent(t)=ssent(s) \<and> 58 srcvd(t)=srcvd(s) \<and> 59 sbit(t)=sbit(s) \<and> 60 ssending(s) \<and> 61 ~ssending(t) | 62 C_m_r => False | 63 C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) \<and> 64 sq(t)=tl(sq(s)) \<and> 65 ssent(t)=ssent(s) \<and> 66 srcvd(t)=srcvd(s) \<and> 67 sbit(t) = (~sbit(s)) \<and> 68 ~ssending(s) \<and> 69 ssending(t) | 70 C_r_r(m) => False}" 71 72definition 73 sender_ioa :: "('m action, 'm sender_state)ioa" where 74 "sender_ioa = 75 (sender_asig, {([],{|},{|},False,True)}, sender_trans,{},{})" 76 77lemma in_sender_asig: 78 "S_msg(m) \<in> actions(sender_asig)" 79 "R_msg(m) \<notin> actions(sender_asig)" 80 "S_pkt(pkt) \<in> actions(sender_asig)" 81 "R_pkt(pkt) \<notin> actions(sender_asig)" 82 "S_ack(b) \<notin> actions(sender_asig)" 83 "R_ack(b) \<in> actions(sender_asig)" 84 "C_m_s \<in> actions(sender_asig)" 85 "C_m_r \<notin> actions(sender_asig)" 86 "C_r_s \<in> actions(sender_asig)" 87 "C_r_r(m) \<notin> actions(sender_asig)" 88 by (simp_all add: sender_asig_def actions_def asig_projections) 89 90lemmas sender_projections = sq_def ssent_def srcvd_def sbit_def ssending_def 91 92end 93