isabelle: src/HOLCF/IOA/NTP/Receiver.thy@0b2ff9541727 (annotated)

3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/NTP/Receiver.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* The implementation: receiver *}
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Receiver
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports IOA Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	11
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	types
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	13
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	14	'm receiver_state
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	15	= "'m list * bool multiset * 'm packet multiset * bool * bool"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	16	(* messages #replies #received header mode *)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	17
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	18	consts
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	19
6468 a7b1669f5365 put types into "" because of signature clash; mueller parents: 3852 diff changeset	20	receiver_asig :: "'m action signature"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	receiver_trans:: "('m action, 'm receiver_state)transition set"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	22	receiver_ioa :: "('m action, 'm receiver_state)ioa"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	23	rq :: "'m receiver_state => 'm list"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	24	rsent :: "'m receiver_state => bool multiset"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	25	rrcvd :: "'m receiver_state => 'm packet multiset"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	26	rbit :: "'m receiver_state => bool"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	27	rsending :: "'m receiver_state => bool"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	28
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	29	defs
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	30
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	31	rq_def: "rq == fst"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	32	rsent_def: "rsent == fst o snd"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	33	rrcvd_def: "rrcvd == fst o snd o snd"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	34	rbit_def: "rbit == fst o snd o snd o snd"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	35	rsending_def: "rsending == snd o snd o snd o snd"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	36
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	37	receiver_asig_def: "receiver_asig ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	38	(UN pkt. {R_pkt(pkt)},
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	39	(UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	40	insert C_m_r (UN m. {C_r_r(m)}))"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	41
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	42	receiver_trans_def: "receiver_trans ==
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	43	{tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	44	t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	45	in
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	46	case fst(snd(tr))
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	47	of
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	48	S_msg(m) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	49	R_msg(m) => rq(s) = (m # rq(t)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	50	rsent(t)=rsent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	51	rrcvd(t)=rrcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	52	rbit(t)=rbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	53	rsending(t)=rsending(s) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	54	S_pkt(pkt) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	55	R_pkt(pkt) => rq(t) = rq(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	56	rsent(t) = rsent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	57	rrcvd(t) = addm (rrcvd s) pkt &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	58	rbit(t) = rbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	59	rsending(t) = rsending(s) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	60	S_ack(b) => b = rbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	61	rq(t) = rq(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	62	rsent(t) = addm (rsent s) (rbit s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	63	rrcvd(t) = rrcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	64	rbit(t)=rbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	65	rsending(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	66	rsending(t) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	67	R_ack(b) => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	68	C_m_s => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	69	C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	70	rq(t) = rq(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	71	rsent(t)=rsent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	72	rrcvd(t)=rrcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	73	rbit(t)=rbit(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	74	rsending(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	75	~rsending(t) \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	76	C_r_s => False \|
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	77	C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y. hdr(y)=rbit(s)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	78	count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	79	rq(t) = rq(s)@[m] &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	80	rsent(t)=rsent(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	81	rrcvd(t)=rrcvd(s) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	82	rbit(t) = (~rbit(s)) &
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	83	~rsending(s) &
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	84	rsending(t)}"
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	85
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	86
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	87	receiver_ioa_def: "receiver_ioa ==
3523 23eae933c2d9 changes needed for introducing fairness mueller parents: 3073 diff changeset	88	(receiver_asig, {([],{\|},{\|},False,False)}, receiver_trans,{},{})"
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	89
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	90	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	91
3073 88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	92	end

author	wenzelm
	Sat, 03 Sep 2005 16:50:22 +0200
changeset 17244	0b2ff9541727
parent 14981	e73f8140af78
child 19739	c58ef2aa5430
permissions	-rw-r--r--