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