src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 58249 180f1b3508ed
permissions -rw-r--r--
modernized specifications;
wenzelm@41589
     1
(*  Title:      HOL/TLA/Memory/MemClerkParameters.thy
wenzelm@41589
     2
    Author:     Stephan Merz, University of Munich
wenzelm@21624
     3
*)
wenzelm@3807
     4
wenzelm@21624
     5
header {* RPC-Memory example: Parameters of the memory clerk *}
wenzelm@3807
     6
wenzelm@17309
     7
theory MemClerkParameters
wenzelm@17309
     8
imports RPCParameters
wenzelm@17309
     9
begin
wenzelm@3807
    10
wenzelm@17309
    11
datatype mClkState = clkA | clkB
wenzelm@3807
    12
wenzelm@42018
    13
(* types sent on the clerk's send and receive channels are argument types
wenzelm@42018
    14
   of the memory and the RPC, respectively *)
wenzelm@42018
    15
type_synonym mClkSndArgType = "memOp"
wenzelm@42018
    16
type_synonym mClkRcvArgType = "rpcOp"
wenzelm@3807
    17
wenzelm@36866
    18
definition
wenzelm@3807
    19
  (* translate a memory call to an RPC call *)
wenzelm@6255
    20
  MClkRelayArg     :: "memOp => rpcOp"
wenzelm@36866
    21
  where "MClkRelayArg marg = memcall marg"
wenzelm@36866
    22
wenzelm@36866
    23
definition
wenzelm@3807
    24
  (* translate RPC failures to memory failures *)
wenzelm@3807
    25
  MClkReplyVal     :: "Vals => Vals"
wenzelm@36866
    26
  where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
wenzelm@3807
    27
wenzelm@3807
    28
end