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