src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Wed Sep 07 20:22:39 2005 +0200 (2005-09-07)
changeset 17309 c43ed29bd197
parent 11703 6e5de8d4290a
child 21624 6f79647cf536
permissions -rw-r--r--
converted to Isar theory format;
     1 (*
     2     File:        MemClerkParameters.thy
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1997 University of Munich
     6 
     7     Theory Name: MemClerkParameters
     8     Logic Image: TLA
     9 
    10     RPC-Memory example: Parameters of the memory clerk.
    11 *)
    12 
    13 theory MemClerkParameters
    14 imports RPCParameters
    15 begin
    16 
    17 datatype mClkState = clkA | clkB
    18 
    19 types
    20   (* types sent on the clerk's send and receive channels are argument types
    21      of the memory and the RPC, respectively *)
    22   mClkSndArgType   = "memOp"
    23   mClkRcvArgType   = "rpcOp"
    24 
    25 constdefs
    26   (* translate a memory call to an RPC call *)
    27   MClkRelayArg     :: "memOp => rpcOp"
    28     "MClkRelayArg marg == memcall marg"
    29   (* translate RPC failures to memory failures *)
    30   MClkReplyVal     :: "Vals => Vals"
    31     "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    32 
    33 ML {* use_legacy_bindings (the_context ()) *}
    34 
    35 end