src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Mon Feb 08 13:02:56 1999 +0100 (1999-02-08)
changeset 6255 db63752140c7
parent 3807 82a99b090d9d
child 11703 6e5de8d4290a
permissions -rw-r--r--
updated (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   = "memOp"
    20   mClkRcvArgType   = "rpcOp"
    21 
    22 constdefs
    23   (* translate a memory call to an RPC call *)
    24   MClkRelayArg     :: "memOp => rpcOp"
    25     "MClkRelayArg marg == memcall marg"
    26   (* translate RPC failures to memory failures *)
    27   MClkReplyVal     :: "Vals => Vals"
    28     "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    29 
    30 end
    31