(* Title: HOL/HOLCF/IOA/ABP/Receiver.thy Author : Olaf M ü ller section ‹ The implementation: receiver› theory Receiverimports IOA.IOA Action Lemmas begin type_synonym "'m list * bool" ― ‹ messages, mode› definition "'m receiver_state => 'm list" where "rq = fst" definition "'m receiver_state => bool" where "rbit = snd" definition "'m action signature" where "receiver_asig = (UN pkt. {R_pkt(pkt)}, (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), {})" definition "('m action, 'm receiver_state)transition set" where "receiver_trans = {tr. let s = fst(tr); t = snd(snd(tr)) in case fst(snd(tr)) of Next => False | S_msg(m) => False | R_msg(m) => (rq(s) ~= []) & m = hd(rq(s)) & rq(t) = tl(rq(s)) & rbit(t)=rbit(s) | S_pkt(pkt) => False | R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else rq(t) =rq(s) & rbit(t)=rbit(s) | S_ack(b) => b = rbit(s) & rq(t) = rq(s) & rbit(t)=rbit(s) | R_ack(b) => False}" definition "('m action, 'm receiver_state)ioa" where "receiver_ioa = (receiver_asig, {([],False)}, receiver_trans,{},{})" end
Messung V0.5 in Prozent C=91 H=99 G=94
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-08-25)
¤ *© Formatika GbR, Deutschland
