15 (* The clerk takes the same arguments as the memory and sends requests to the RPC *) |
15 (* The clerk takes the same arguments as the memory and sends requests to the RPC *) |
16 mClkSndChType = "memChType" |
16 mClkSndChType = "memChType" |
17 mClkRcvChType = "rpcSndChType" |
17 mClkRcvChType = "rpcSndChType" |
18 mClkStType = "(PrIds => mClkState) stfun" |
18 mClkStType = "(PrIds => mClkState) stfun" |
19 |
19 |
20 consts |
20 constdefs |
21 (* state predicates *) |
21 (* state predicates *) |
22 MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" |
22 MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" |
|
23 "MClkInit rcv cst p == PRED (cst!p = #clkA & ~Calling rcv p)" |
23 |
24 |
24 (* actions *) |
25 (* actions *) |
25 MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
26 MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
|
27 "MClkFwd send rcv cst p == ACT |
|
28 $Calling send p |
|
29 & $(cst!p) = #clkA |
|
30 & Call rcv p MClkRelayArg<arg<send!p>> |
|
31 & (cst!p)$ = #clkB |
|
32 & unchanged (rtrner send!p)" |
|
33 |
26 MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
34 MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
|
35 "MClkRetry send rcv cst p == ACT |
|
36 $(cst!p) = #clkB |
|
37 & res<$(rcv!p)> = #RPCFailure |
|
38 & Call rcv p MClkRelayArg<arg<send!p>> |
|
39 & unchanged (cst!p, rtrner send!p)" |
|
40 |
27 MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
41 MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
|
42 "MClkReply send rcv cst p == ACT |
|
43 ~$Calling rcv p |
|
44 & $(cst!p) = #clkB |
|
45 & Return send p MClkReplyVal<res<rcv!p>> |
|
46 & (cst!p)$ = #clkA |
|
47 & unchanged (caller rcv!p)" |
|
48 |
28 MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
49 MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
|
50 "MClkNext send rcv cst p == ACT |
|
51 ( MClkFwd send rcv cst p |
|
52 | MClkRetry send rcv cst p |
|
53 | MClkReply send rcv cst p)" |
|
54 |
29 |
55 |
30 (* temporal *) |
56 (* temporal *) |
31 MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" |
57 MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" |
|
58 "MClkIPSpec send rcv cst p == TEMP |
|
59 Init MClkInit rcv cst p |
|
60 & [][ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p) |
|
61 & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p) |
|
62 & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)" |
|
63 |
32 MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" |
64 MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" |
|
65 "MClkISpec send rcv cst == TEMP (!p. MClkIPSpec send rcv cst p)" |
33 |
66 |
34 rules |
|
35 MClkInit_def "$(MClkInit rcv cst p) .= |
|
36 ($(cst@p) .= #clkA .& .~ $(Calling rcv p))" |
|
37 |
|
38 MClkFwd_def "MClkFwd send rcv cst p == |
|
39 $(Calling send p) |
|
40 .& $(cst@p) .= #clkA |
|
41 .& Call rcv p (MClkRelayArg[ arg[$(send@p)] ]) |
|
42 .& (cst@p)$ .= #clkB |
|
43 .& unchanged (rtrner send @ p)" |
|
44 |
|
45 MClkRetry_def "MClkRetry send rcv cst p == |
|
46 $(cst@p) .= #clkB |
|
47 .& res[$(rcv@p)] .= #RPCFailure |
|
48 .& Call rcv p (MClkRelayArg[ arg[$(send@p)] ]) |
|
49 .& unchanged <cst@p, rtrner send @ p>" |
|
50 |
|
51 MClkReply_def "MClkReply send rcv cst p == |
|
52 .~ $(Calling rcv p) |
|
53 .& $(cst@p) .= #clkB |
|
54 .& Return send p (MClkReplyVal[ res[$(rcv@p)] ]) |
|
55 .& (cst@p)$ .= #clkA |
|
56 .& unchanged (caller rcv @ p)" |
|
57 |
|
58 MClkNext_def "MClkNext send rcv cst p == |
|
59 MClkFwd send rcv cst p |
|
60 .| MClkRetry send rcv cst p |
|
61 .| MClkReply send rcv cst p" |
|
62 |
|
63 MClkIPSpec_def "MClkIPSpec send rcv cst p == |
|
64 Init($(MClkInit rcv cst p)) |
|
65 .& [][ MClkNext send rcv cst p ]_<cst@p, rtrner send @ p, caller rcv @ p> |
|
66 .& WF(MClkFwd send rcv cst p)_<cst@p, rtrner send @ p, caller rcv @ p> |
|
67 .& SF(MClkReply send rcv cst p)_<cst@p, rtrner send @ p, caller rcv @ p>" |
|
68 |
|
69 MClkISpec_def "MClkISpec send rcv cst == RALL p. MClkIPSpec send rcv cst p" |
|
70 end |
67 end |
71 |
68 |
72 |
69 |