1(* Title: HOL/HOLCF/IOA/ABP/Sender.thy 2 Author: Olaf M��ller 3*) 4 5section \<open>The implementation: sender\<close> 6 7theory Sender 8imports IOA.IOA Action Lemmas 9begin 10 11type_synonym 12 'm sender_state = "'m list * bool" \<comment> \<open>messages, Alternating Bit\<close> 13 14definition 15 sq :: "'m sender_state => 'm list" where 16 "sq = fst" 17 18definition 19 sbit :: "'m sender_state => bool" where 20 "sbit = snd" 21 22definition 23 sender_asig :: "'m action signature" where 24 "sender_asig = ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), 25 UN pkt. {S_pkt(pkt)}, 26 {})" 27 28definition 29 sender_trans :: "('m action, 'm sender_state)transition set" where 30 "sender_trans = 31 {tr. let s = fst(tr); 32 t = snd(snd(tr)) 33 in case fst(snd(tr)) 34 of 35 Next => if sq(s)=[] then t=s else False | 36 S_msg(m) => sq(t)=sq(s)@[m] & 37 sbit(t)=sbit(s) | 38 R_msg(m) => False | 39 S_pkt(pkt) => sq(s) ~= [] & 40 hdr(pkt) = sbit(s) & 41 msg(pkt) = hd(sq(s)) & 42 sq(t) = sq(s) & 43 sbit(t) = sbit(s) | 44 R_pkt(pkt) => False | 45 S_ack(b) => False | 46 R_ack(b) => if b = sbit(s) then 47 sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else 48 sq(t)=sq(s) & sbit(t)=sbit(s)}" 49 50definition 51 sender_ioa :: "('m action, 'm sender_state)ioa" where 52 "sender_ioa = 53 (sender_asig, {([],True)}, sender_trans,{},{})" 54 55end 56