isabelle: src/HOL/TLA/Memory/MemClerk.thy@86c58273f8c0 (annotated)

3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	1	(*
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	2	File: MemClerk.thy
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	3	Author: Stephan Merz
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	4	Copyright: 1997 University of Munich
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	5
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	6	Theory Name: MemClerk
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	7	Logic Image: TLA
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	8
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	9	RPC-Memory example: specification of the memory clerk.
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	10	*)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	11
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	12	MemClerk = Memory + RPC + MemClerkParameters +
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	13
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	14	types
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	15	(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	16	mClkSndChType = "memChType"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	17	mClkRcvChType = "rpcSndChType"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	18	mClkStType = "(PrIds => mClkState) stfun"
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	19
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	20	constdefs
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	21	(* state predicates *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	22	MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	23	"MClkInit rcv cst p == PRED (cst!p = #clkA & ~Calling rcv p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	24
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	25	(* actions *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	26	MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	27	"MClkFwd send rcv cst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	28	$Calling send p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	29	& $(cst!p) = #clkA
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	30	& Call rcv p MClkRelayArg<arg<send!p>>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	31	& (cst!p)$ = #clkB
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	32	& unchanged (rtrner send!p)"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	33
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	34	MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	35	"MClkRetry send rcv cst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	36	$(cst!p) = #clkB
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	37	& res<$(rcv!p)> = #RPCFailure
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	38	& Call rcv p MClkRelayArg<arg<send!p>>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	39	& unchanged (cst!p, rtrner send!p)"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	40
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	41	MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	42	"MClkReply send rcv cst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	43	~$Calling rcv p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	44	& $(cst!p) = #clkB
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	45	& Return send p MClkReplyVal<res<rcv!p>>
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	46	& (cst!p)$ = #clkA
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	47	& unchanged (caller rcv!p)"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	48
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	49	MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	50	"MClkNext send rcv cst p == ACT
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	51	( MClkFwd send rcv cst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	52	\| MClkRetry send rcv cst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	53	\| MClkReply send rcv cst p)"
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	54
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	55
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	56	(* temporal *)
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	57	MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal"
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	58	"MClkIPSpec send rcv cst p == TEMP
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	59	Init MClkInit rcv cst p
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	60	& [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	61	& WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	62	& SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	63
6255 db63752140c7 updated (Stephan Merz); wenzelm parents: 3807 diff changeset	64	MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
9517 f58863b1406a tuned version by Stephan Merz (unbatchified etc.); wenzelm parents: 6255 diff changeset	65	"MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
3807 82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	66
82a99b090d9d A formalization of TLA in HOL -- by Stephan Merz; wenzelm parents: diff changeset	67	end

author	wenzelm
	Wed, 05 Dec 2001 03:13:57 +0100
changeset 12378	86c58273f8c0
parent 11703	6e5de8d4290a
child 17309	c43ed29bd197
permissions	-rw-r--r--