--- a/src/HOL/TLA/Memory/RPC.thy Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy Mon Feb 08 13:02:56 1999 +0100
@@ -7,15 +7,13 @@
Logic Image: TLA
RPC-Memory example: RPC specification
- For simplicity, specify the instance of RPC that is used in the
- memory implementation (ignoring the BadCall exception).
*)
-RPC = RPCParameters + ProcedureInterface +
+RPC = RPCParameters + ProcedureInterface + Memory +
types
- rpcSndChType = "(rpcArgType,Vals) channel"
- rpcRcvChType = "(memArgType,Vals) channel"
+ rpcSndChType = "(rpcOp,Vals) channel"
+ rpcRcvChType = "memChType"
rpcStType = "(PrIds => rpcState) stfun"
consts
@@ -34,49 +32,47 @@
RPCISpec :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
rules
- RPCInit_def "$(RPCInit rcv rst p) .=
- ($(rst@p) .= # rpcA
- .& .~ $(Calling rcv p))"
+ RPCInit_def "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
- RPCFwd_def "RPCFwd send rcv rst p ==
+ RPCFwd_def "RPCFwd send rcv rst p == ACT
$(Calling send p)
- .& $(rst@p) .= # rpcA
- .& IsLegalRcvArg[ arg[ $(send@p) ] ]
- .& Call rcv p (RPCRelayArg[ arg[ $(send@p)] ])
- .& (rst@p)$ .= # rpcB
- .& unchanged (rtrner send @ p)"
+ & $(rst!p) = # rpcA
+ & IsLegalRcvArg<arg<$(send!p)>>
+ & Call rcv p RPCRelayArg<arg<send!p>>
+ & (rst!p)$ = # rpcB
+ & unchanged (rtrner send!p)"
- RPCReject_def "RPCReject send rcv rst p ==
- $(rst@p) .= # rpcA
- .& .~ IsLegalRcvArg[ arg[ $(send@p) ] ]
- .& Return send p (#BadCall)
- .& unchanged <(rst@p), (caller rcv @ p)>"
+ RPCReject_def "RPCReject send rcv rst p == ACT
+ $(rst!p) = # rpcA
+ & ~IsLegalRcvArg<arg<$(send!p)>>
+ & Return send p #BadCall
+ & unchanged ((rst!p), (caller rcv!p))"
- RPCFail_def "RPCFail send rcv rst p ==
- .~ $(Calling rcv p)
- .& Return send p (#RPCFailure)
- .& (rst@p)$ .= #rpcA
- .& unchanged (caller rcv @ p)"
+ RPCFail_def "RPCFail send rcv rst p == ACT
+ ~$(Calling rcv p)
+ & Return send p #RPCFailure
+ & (rst!p)$ = #rpcA
+ & unchanged (caller rcv!p)"
- RPCReply_def "RPCReply send rcv rst p ==
- .~ $(Calling rcv p)
- .& $(rst@p) .= #rpcB
- .& Return send p (res[$(rcv@p)])
- .& (rst@p)$ .= #rpcA
- .& unchanged (caller rcv @ p)"
+ RPCReply_def "RPCReply send rcv rst p == ACT
+ ~$(Calling rcv p)
+ & $(rst!p) = #rpcB
+ & Return send p res<rcv!p>
+ & (rst!p)$ = #rpcA
+ & unchanged (caller rcv!p)"
- RPCNext_def "RPCNext send rcv rst p ==
- RPCFwd send rcv rst p
- .| RPCReject send rcv rst p
- .| RPCFail send rcv rst p
- .| RPCReply send rcv rst p"
+ RPCNext_def "RPCNext send rcv rst p == ACT
+ ( RPCFwd send rcv rst p
+ | RPCReject send rcv rst p
+ | RPCFail send rcv rst p
+ | RPCReply send rcv rst p)"
- RPCIPSpec_def "RPCIPSpec send rcv rst p ==
- Init($(RPCInit rcv rst p))
- .& [][ RPCNext send rcv rst p ]_<rst@p, rtrner send @ p, caller rcv @ p>
- .& WF(RPCNext send rcv rst p)_<rst@p, rtrner send @ p, caller rcv @ p>"
+ RPCIPSpec_def "RPCIPSpec send rcv rst p == TEMP
+ Init RPCInit rcv rst p
+ & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+ & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
- RPCISpec_def "RPCISpec send rcv rst == RALL p. RPCIPSpec send rcv rst p"
+ RPCISpec_def "RPCISpec send rcv rst == TEMP (! p. RPCIPSpec send rcv rst p)"
end