(* Title: HOLCF/IOA/ABP/Sender.thy ID: $Id: Sender.thy,v 1.6 2005/09/03 14:50:23 wenzelm Exp $ Author: Olaf Müller *) header {* The implementation: sender *} theory Sender imports IOA Action Lemmas begin types 'm sender_state = "'m list * bool" -- {* messages, Alternating Bit *} constdefs sq :: "'m sender_state => 'm list" "sq == fst" sbit :: "'m sender_state => bool" "sbit == snd" sender_asig :: "'m action signature" "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), UN pkt. {S_pkt(pkt)}, {})" sender_trans :: "('m action, 'm sender_state)transition set" "sender_trans == {tr. let s = fst(tr); t = snd(snd(tr)) in case fst(snd(tr)) of Next => if sq(s)=[] then t=s else False | S_msg(m) => sq(t)=sq(s)@[m] & sbit(t)=sbit(s) | R_msg(m) => False | S_pkt(pkt) => sq(s) ~= [] & hdr(pkt) = sbit(s) & msg(pkt) = hd(sq(s)) & sq(t) = sq(s) & sbit(t) = sbit(s) | R_pkt(pkt) => False | S_ack(b) => False | R_ack(b) => if b = sbit(s) then sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else sq(t)=sq(s) & sbit(t)=sbit(s)}" sender_ioa :: "('m action, 'm sender_state)ioa" "sender_ioa == (sender_asig, {([],True)}, sender_trans,{},{})" ML {* use_legacy_bindings (the_context ()) *} end