(* Title: HOL/TLA/Memory/MemClerkParameters.thy Author: Stephan Merz, University of Munich *)
section‹RPC-Memory example: Parameters of the memory clerk›
theory MemClerkParameters imports RPCParameters begin
datatype mClkState = clkA | clkB
(* types sent on the clerk's send and receive channels are argument types of the memory and the RPC, respectively *) type_synonym mClkSndArgType = "memOp" type_synonym mClkRcvArgType = "rpcOp"
definition (* translate a memory call to an RPC call *)
MClkRelayArg :: "memOp ==> rpcOp" where"MClkRelayArg marg = memcall marg"
definition (* translate RPC failures to memory failures *)
MClkReplyVal :: "Vals ==> Vals" where"MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet am 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
