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