src/HOL/TLA/Memory/RPCParameters.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        RPCParameters.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: RPCParameters
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    RPC-Memory example: RPC parameters
wenzelm@3807
    10
    For simplicity, specify the instance of RPC that is used in the
wenzelm@3807
    11
    memory implementation.
wenzelm@3807
    12
*)
wenzelm@3807
    13
wenzelm@3807
    14
RPCParameters = MemoryParameters +
wenzelm@3807
    15
wenzelm@6255
    16
datatype  rpcOp = memcall memOp | othercall Vals
wenzelm@3807
    17
datatype  rpcState = rpcA | rpcB
wenzelm@3807
    18
wenzelm@6255
    19
(***
wenzelm@3807
    20
types
wenzelm@3807
    21
  (* type of RPC arguments other than memory calls *)
wenzelm@3807
    22
  noMemArgType
wenzelm@3807
    23
  (* legal arguments for (our instance of) the RPC component *)
wenzelm@3807
    24
  rpcArgType = "(rpcOps * memArgType) + (rpcOps * noMemArgType)"
wenzelm@3807
    25
wenzelm@3807
    26
arities
wenzelm@3807
    27
  noMemArgType :: term
wenzelm@6255
    28
***)
wenzelm@3807
    29
wenzelm@3807
    30
consts
wenzelm@3807
    31
  (* some particular return values *)
wenzelm@6255
    32
  RPCFailure     :: Vals
wenzelm@6255
    33
  BadCall        :: Vals
wenzelm@3807
    34
  
wenzelm@3807
    35
  (* Translate an rpc call to a memory call and test if the current argument
wenzelm@3807
    36
     is legal for the receiver (i.e., the memory). This can now be a little
wenzelm@3807
    37
     simpler than for the generic RPC component. RelayArg returns an arbitrary
wenzelm@3807
    38
     memory call for illegal arguments. *)
wenzelm@6255
    39
(***
wenzelm@6255
    40
  IsLegalRcvArg  :: rpcArgType => bool
wenzelm@6255
    41
  RPCRelayArg    :: rpcArgType => memArgType
wenzelm@6255
    42
***)
wenzelm@6255
    43
  IsLegalRcvArg  :: rpcOp => bool
wenzelm@6255
    44
  RPCRelayArg    :: rpcOp => memOp
wenzelm@3807
    45
wenzelm@3807
    46
rules
wenzelm@3807
    47
  (* RPCFailure is different from MemVals and exceptions *)
wenzelm@6255
    48
  RFNoMemVal        "RPCFailure ~: MemVal"
wenzelm@3807
    49
  NotAResultNotRF   "NotAResult ~= RPCFailure"
wenzelm@3807
    50
  OKNotRF           "OK ~= RPCFailure"
wenzelm@3807
    51
  BANotRF           "BadArg ~= RPCFailure"
wenzelm@3807
    52
wenzelm@6255
    53
(***
wenzelm@3807
    54
  IsLegalRcvArg_def "IsLegalRcvArg ra == EX marg. ra = Inl (remoteCall,marg)"
wenzelm@3807
    55
  RPCRelayArg_def   "RPCRelayArg ra == 
wenzelm@3807
    56
                         case ra of Inl (rm) => (snd rm)
wenzelm@6255
    57
                                  | Inr (rn) => (read, @ l. True)"
wenzelm@6255
    58
***)
wenzelm@6255
    59
defs
wenzelm@6255
    60
  IsLegalRcvArg_def "IsLegalRcvArg ra ==
wenzelm@6255
    61
		         case ra of (memcall m) => True
wenzelm@6255
    62
		                  | (othercall v) => False"
wenzelm@6255
    63
  RPCRelayArg_def   "RPCRelayArg ra ==
wenzelm@6255
    64
		         case ra of (memcall m) => m
wenzelm@6255
    65
		                  | (othercall v) => arbitrary"
wenzelm@3807
    66
end
wenzelm@3807
    67
wenzelm@3807
    68