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