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);
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@6255
    19
  mClkSndArgType   = "memOp"
wenzelm@6255
    20
  mClkRcvArgType   = "rpcOp"
wenzelm@3807
    21
wenzelm@6255
    22
constdefs
wenzelm@3807
    23
  (* translate a memory call to an RPC call *)
wenzelm@6255
    24
  MClkRelayArg     :: "memOp => rpcOp"
wenzelm@6255
    25
    "MClkRelayArg marg == memcall marg"
wenzelm@3807
    26
  (* translate RPC failures to memory failures *)
wenzelm@3807
    27
  MClkReplyVal     :: "Vals => Vals"
wenzelm@6255
    28
    "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
wenzelm@3807
    29
wenzelm@3807
    30
end
wenzelm@3807
    31