|
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 For simplicity, specify the instance of RPC that is used in the |
|
11 memory implementation (ignoring the BadCall exception). |
|
12 *) |
|
13 |
|
14 RPC = RPCParameters + ProcedureInterface + |
|
15 |
|
16 types |
|
17 rpcSndChType = "(rpcArgType,Vals) channel" |
|
18 rpcRcvChType = "(memArgType,Vals) channel" |
|
19 rpcStType = "(PrIds => rpcState) stfun" |
|
20 |
|
21 consts |
|
22 (* state predicates *) |
|
23 RPCInit :: "rpcRcvChType => rpcStType => PrIds => stpred" |
|
24 |
|
25 (* actions *) |
|
26 RPCFwd :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" |
|
27 RPCReject :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" |
|
28 RPCFail :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" |
|
29 RPCReply :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" |
|
30 RPCNext :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => action" |
|
31 |
|
32 (* temporal *) |
|
33 RPCIPSpec :: "rpcSndChType => rpcRcvChType => rpcStType => PrIds => temporal" |
|
34 RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal" |
|
35 |
|
36 rules |
|
37 RPCInit_def "$(RPCInit rcv rst p) .= |
|
38 ($(rst@p) .= # rpcA |
|
39 .& .~ $(Calling rcv p))" |
|
40 |
|
41 RPCFwd_def "RPCFwd send rcv rst p == |
|
42 $(Calling send p) |
|
43 .& $(rst@p) .= # rpcA |
|
44 .& IsLegalRcvArg[ arg[ $(send@p) ] ] |
|
45 .& Call rcv p (RPCRelayArg[ arg[ $(send@p)] ]) |
|
46 .& (rst@p)$ .= # rpcB |
|
47 .& unchanged (rtrner send @ p)" |
|
48 |
|
49 RPCReject_def "RPCReject send rcv rst p == |
|
50 $(rst@p) .= # rpcA |
|
51 .& .~ IsLegalRcvArg[ arg[ $(send@p) ] ] |
|
52 .& Return send p (#BadCall) |
|
53 .& unchanged <(rst@p), (caller rcv @ p)>" |
|
54 |
|
55 RPCFail_def "RPCFail send rcv rst p == |
|
56 .~ $(Calling rcv p) |
|
57 .& Return send p (#RPCFailure) |
|
58 .& (rst@p)$ .= #rpcA |
|
59 .& unchanged (caller rcv @ p)" |
|
60 |
|
61 RPCReply_def "RPCReply send rcv rst p == |
|
62 .~ $(Calling rcv p) |
|
63 .& $(rst@p) .= #rpcB |
|
64 .& Return send p (res[$(rcv@p)]) |
|
65 .& (rst@p)$ .= #rpcA |
|
66 .& unchanged (caller rcv @ p)" |
|
67 |
|
68 RPCNext_def "RPCNext send rcv rst p == |
|
69 RPCFwd send rcv rst p |
|
70 .| RPCReject send rcv rst p |
|
71 .| RPCFail send rcv rst p |
|
72 .| RPCReply send rcv rst p" |
|
73 |
|
74 RPCIPSpec_def "RPCIPSpec send rcv rst p == |
|
75 Init($(RPCInit rcv rst p)) |
|
76 .& [][ RPCNext send rcv rst p ]_<rst@p, rtrner send @ p, caller rcv @ p> |
|
77 .& WF(RPCNext send rcv rst p)_<rst@p, rtrner send @ p, caller rcv @ p>" |
|
78 |
|
79 RPCISpec_def "RPCISpec send rcv rst == RALL p. RPCIPSpec send rcv rst p" |
|
80 |
|
81 end |
|
82 |
|
83 |
|
84 |