src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Wed Oct 08 11:50:33 1997 +0200 (1997-10-08)
changeset 3807 82a99b090d9d
child 6255 db63752140c7
permissions -rw-r--r--
A formalization of TLA in HOL -- by Stephan Merz;
     1 (*
     2     File:        MemClerkParameters.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: MemClerkParameters
     7     Logic Image: TLA
     8 
     9     RPC-Memory example: Parameters of the memory clerk.
    10 *)
    11 
    12 MemClerkParameters = RPCParameters + 
    13 
    14 datatype  mClkState  =  clkA | clkB
    15 
    16 types
    17   (* types sent on the clerk's send and receive channels are argument types
    18      of the memory and the RPC, respectively *)
    19   mClkSndArgType   = "memArgType"
    20   mClkRcvArgType   = "rpcArgType"
    21 
    22 consts
    23   (* translate a memory call to an RPC call *)
    24   MClkRelayArg     :: "memArgType => rpcArgType"
    25   (* translate RPC failures to memory failures *)
    26   MClkReplyVal     :: "Vals => Vals"
    27 
    28 rules
    29   MClkRelayArg_def    "MClkRelayArg marg == Inl (remoteCall, marg)"
    30   MClkReplyVal_def    "MClkReplyVal v == 
    31                            if v = RPCFailure then MemFailure else v"
    32 
    33 end
    34