src/HOL/TLA/Memory/MemClerkParameters.thy
author wenzelm
Wed May 12 16:44:49 2010 +0200 (2010-05-12)
changeset 36866 426d5781bb25
parent 21624 6f79647cf536
child 41589 bbd861837ebc
permissions -rw-r--r--
modernized specifications;
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        MemClerkParameters.thy
wenzelm@17309
     3
    ID:          $Id$
wenzelm@3807
     4
    Author:      Stephan Merz
wenzelm@3807
     5
    Copyright:   1997 University of Munich
wenzelm@21624
     6
*)
wenzelm@3807
     7
wenzelm@21624
     8
header {* RPC-Memory example: Parameters of the memory clerk *}
wenzelm@3807
     9
wenzelm@17309
    10
theory MemClerkParameters
wenzelm@17309
    11
imports RPCParameters
wenzelm@17309
    12
begin
wenzelm@3807
    13
wenzelm@17309
    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@36866
    22
definition
wenzelm@3807
    23
  (* translate a memory call to an RPC call *)
wenzelm@6255
    24
  MClkRelayArg     :: "memOp => rpcOp"
wenzelm@36866
    25
  where "MClkRelayArg marg = memcall marg"
wenzelm@36866
    26
wenzelm@36866
    27
definition
wenzelm@3807
    28
  (* translate RPC failures to memory failures *)
wenzelm@3807
    29
  MClkReplyVal     :: "Vals => Vals"
wenzelm@36866
    30
  where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
wenzelm@3807
    31
wenzelm@3807
    32
end