src/HOL/TLA/Memory/MemClerkParameters.thy
changeset 3807 82a99b090d9d
child 6255 db63752140c7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed Oct 08 11:50:33 1997 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +(*
     1.5 +    File:        MemClerkParameters.thy
     1.6 +    Author:      Stephan Merz
     1.7 +    Copyright:   1997 University of Munich
     1.8 +
     1.9 +    Theory Name: MemClerkParameters
    1.10 +    Logic Image: TLA
    1.11 +
    1.12 +    RPC-Memory example: Parameters of the memory clerk.
    1.13 +*)
    1.14 +
    1.15 +MemClerkParameters = RPCParameters + 
    1.16 +
    1.17 +datatype  mClkState  =  clkA | clkB
    1.18 +
    1.19 +types
    1.20 +  (* types sent on the clerk's send and receive channels are argument types
    1.21 +     of the memory and the RPC, respectively *)
    1.22 +  mClkSndArgType   = "memArgType"
    1.23 +  mClkRcvArgType   = "rpcArgType"
    1.24 +
    1.25 +consts
    1.26 +  (* translate a memory call to an RPC call *)
    1.27 +  MClkRelayArg     :: "memArgType => rpcArgType"
    1.28 +  (* translate RPC failures to memory failures *)
    1.29 +  MClkReplyVal     :: "Vals => Vals"
    1.30 +
    1.31 +rules
    1.32 +  MClkRelayArg_def    "MClkRelayArg marg == Inl (remoteCall, marg)"
    1.33 +  MClkReplyVal_def    "MClkReplyVal v == 
    1.34 +                           if v = RPCFailure then MemFailure else v"
    1.35 +
    1.36 +end
    1.37 +