src/HOL/TLA/Memory/RPC.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 9517 f58863b1406a
child 17309 c43ed29bd197
permissions -rw-r--r--
tuned;
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        RPC.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: RPC
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    RPC-Memory example: RPC specification
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@6255
    12
RPC = RPCParameters + ProcedureInterface + Memory +
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@6255
    15
  rpcSndChType  = "(rpcOp,Vals) channel"
wenzelm@6255
    16
  rpcRcvChType  = "memChType"
wenzelm@3807
    17
  rpcStType     = "(PrIds => rpcState) stfun"
wenzelm@3807
    18
wenzelm@3807
    19
consts
wenzelm@3807
    20
  (* state predicates *)
wenzelm@3807
    21
  RPCInit      :: "rpcRcvChType => rpcStType => PrIds => stpred"
wenzelm@3807
    22
wenzelm@3807
    23
  (* actions *)
wenzelm@3807
    24
  RPCFwd     :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
wenzelm@3807
    25
  RPCReject  :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
wenzelm@3807
    26
  RPCFail    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
wenzelm@3807
    27
  RPCReply   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
wenzelm@3807
    28
  RPCNext    :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action"
wenzelm@3807
    29
wenzelm@3807
    30
  (* temporal *)
wenzelm@3807
    31
  RPCIPSpec   :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal"
wenzelm@3807
    32
  RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
wenzelm@3807
    33
wenzelm@3807
    34
rules
wenzelm@6255
    35
  RPCInit_def       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
wenzelm@3807
    36
wenzelm@6255
    37
  RPCFwd_def        "RPCFwd send rcv rst p == ACT
wenzelm@3807
    38
                         $(Calling send p)
wenzelm@6255
    39
                         & $(rst!p) = # rpcA
wenzelm@6255
    40
                         & IsLegalRcvArg<arg<$(send!p)>>
wenzelm@6255
    41
                         & Call rcv p RPCRelayArg<arg<send!p>>
wenzelm@6255
    42
                         & (rst!p)$ = # rpcB
wenzelm@6255
    43
                         & unchanged (rtrner send!p)"
wenzelm@3807
    44
wenzelm@6255
    45
  RPCReject_def     "RPCReject send rcv rst p == ACT
wenzelm@6255
    46
                           $(rst!p) = # rpcA
wenzelm@6255
    47
                         & ~IsLegalRcvArg<arg<$(send!p)>>
wenzelm@6255
    48
                         & Return send p #BadCall
wenzelm@6255
    49
                         & unchanged ((rst!p), (caller rcv!p))"
wenzelm@3807
    50
wenzelm@6255
    51
  RPCFail_def       "RPCFail send rcv rst p == ACT
wenzelm@6255
    52
                           ~$(Calling rcv p)
wenzelm@6255
    53
                         & Return send p #RPCFailure
wenzelm@6255
    54
                         & (rst!p)$ = #rpcA
wenzelm@6255
    55
                         & unchanged (caller rcv!p)"
wenzelm@3807
    56
wenzelm@6255
    57
  RPCReply_def      "RPCReply send rcv rst p == ACT
wenzelm@6255
    58
                           ~$(Calling rcv p)
wenzelm@6255
    59
                         & $(rst!p) = #rpcB
wenzelm@6255
    60
		         & Return send p res<rcv!p>
wenzelm@6255
    61
                         & (rst!p)$ = #rpcA
wenzelm@6255
    62
                         & unchanged (caller rcv!p)"
wenzelm@3807
    63
wenzelm@6255
    64
  RPCNext_def       "RPCNext send rcv rst p == ACT
wenzelm@6255
    65
                        (  RPCFwd send rcv rst p
wenzelm@6255
    66
                         | RPCReject send rcv rst p
wenzelm@6255
    67
                         | RPCFail send rcv rst p
wenzelm@6255
    68
                         | RPCReply send rcv rst p)"
wenzelm@3807
    69
wenzelm@6255
    70
  RPCIPSpec_def     "RPCIPSpec send rcv rst p == TEMP
wenzelm@6255
    71
                           Init RPCInit rcv rst p
wenzelm@6255
    72
                         & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
wenzelm@6255
    73
                         & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
wenzelm@3807
    74
wenzelm@9517
    75
  RPCISpec_def      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
wenzelm@3807
    76
wenzelm@3807
    77
end