Up to index of Isabelle/HOL/TLA/Memory
theory MemClerk(* File: MemClerk.thy ID: $Id: MemClerk.thy,v 1.5 2005/09/07 18:22:41 wenzelm Exp $ Author: Stephan Merz Copyright: 1997 University of Munich Theory Name: MemClerk Logic Image: TLA RPC-Memory example: specification of the memory clerk. *) theory MemClerk imports Memory RPC MemClerkParameters begin types (* The clerk takes the same arguments as the memory and sends requests to the RPC *) mClkSndChType = "memChType" mClkRcvChType = "rpcSndChType" mClkStType = "(PrIds => mClkState) stfun" constdefs (* state predicates *) MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" "MClkInit rcv cst p == PRED (cst!p = #clkA & ~Calling rcv p)" (* actions *) MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" "MClkFwd send rcv cst p == ACT $Calling send p & $(cst!p) = #clkA & Call rcv p MClkRelayArg<arg<send!p>> & (cst!p)$ = #clkB & unchanged (rtrner send!p)" MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" "MClkRetry send rcv cst p == ACT $(cst!p) = #clkB & res<$(rcv!p)> = #RPCFailure & Call rcv p MClkRelayArg<arg<send!p>> & unchanged (cst!p, rtrner send!p)" MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" "MClkReply send rcv cst p == ACT ~$Calling rcv p & $(cst!p) = #clkB & Return send p MClkReplyVal<res<rcv!p>> & (cst!p)$ = #clkA & unchanged (caller rcv!p)" MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" "MClkNext send rcv cst p == ACT ( MClkFwd send rcv cst p | MClkRetry send rcv cst p | MClkReply send rcv cst p)" (* temporal *) MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" "MClkIPSpec send rcv cst p == TEMP Init MClkInit rcv cst p & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p) & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p) & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)" MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)" ML {* use_legacy_bindings (the_context ()) *} end
theorem MClkidle:
|- ¬ $Calling send p ∧ $(cst!p) = #clkA --> ¬ MClkNext send rcv cst p
theorem MClkbusy:
|- $Calling rcv p --> ¬ MClkNext send rcv cst p
theorem MClkFwd_enabled:
basevars (rtrner send!p, caller rcv!p, cst!p) ==> |- Calling send p ∧ ¬ Calling rcv p ∧ cst!p = #clkA --> Enabled MClkFwd send rcv cst p
theorem MClkFwd_ch_enabled:
|- Enabled MClkFwd send rcv cst p --> Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))
theorem MClkReply_change:
|- MClkReply send rcv cst p --> <MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)
theorem MClkReply_enabled:
basevars (rtrner send!p, caller rcv!p, cst!p) ==> |- Calling send p ∧ ¬ Calling rcv p ∧ cst!p = #clkB --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))
theorem MClkReplyNotRetry:
|- MClkReply send rcv cst p --> ¬ MClkRetry send rcv cst p