author | wenzelm |
Fri, 26 Jun 2015 15:55:44 +0200 | |
changeset 60591 | e0b77517f9a9 |
parent 60588 | 750c533459b1 |
child 60592 | c9bd1d902f04 |
permissions | -rw-r--r-- |
41589 | 1 |
(* Title: HOL/TLA/Memory/RPC.thy |
2 |
Author: Stephan Merz, University of Munich |
|
21624 | 3 |
*) |
3807 | 4 |
|
58889 | 5 |
section {* RPC-Memory example: RPC specification *} |
3807 | 6 |
|
17309 | 7 |
theory RPC |
8 |
imports RPCParameters ProcedureInterface Memory |
|
9 |
begin |
|
3807 | 10 |
|
42018 | 11 |
type_synonym rpcSndChType = "(rpcOp,Vals) channel" |
12 |
type_synonym rpcRcvChType = "memChType" |
|
60588 | 13 |
type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun" |
3807 | 14 |
|
15 |
consts |
|
16 |
(* state predicates *) |
|
60588 | 17 |
RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred" |
3807 | 18 |
|
19 |
(* actions *) |
|
60588 | 20 |
RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action" |
21 |
RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action" |
|
22 |
RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action" |
|
23 |
RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action" |
|
24 |
RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action" |
|
3807 | 25 |
|
26 |
(* temporal *) |
|
60588 | 27 |
RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal" |
28 |
RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal" |
|
3807 | 29 |
|
17309 | 30 |
defs |
60591 | 31 |
RPCInit_def: "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)" |
3807 | 32 |
|
17309 | 33 |
RPCFwd_def: "RPCFwd send rcv rst p == ACT |
3807 | 34 |
$(Calling send p) |
60591 | 35 |
\<and> $(rst!p) = # rpcA |
36 |
\<and> IsLegalRcvArg<arg<$(send!p)>> |
|
37 |
\<and> Call rcv p RPCRelayArg<arg<send!p>> |
|
38 |
\<and> (rst!p)$ = # rpcB |
|
39 |
\<and> unchanged (rtrner send!p)" |
|
3807 | 40 |
|
17309 | 41 |
RPCReject_def: "RPCReject send rcv rst p == ACT |
6255 | 42 |
$(rst!p) = # rpcA |
60591 | 43 |
\<and> \<not>IsLegalRcvArg<arg<$(send!p)>> |
44 |
\<and> Return send p #BadCall |
|
45 |
\<and> unchanged ((rst!p), (caller rcv!p))" |
|
3807 | 46 |
|
17309 | 47 |
RPCFail_def: "RPCFail send rcv rst p == ACT |
60587 | 48 |
\<not>$(Calling rcv p) |
60591 | 49 |
\<and> Return send p #RPCFailure |
50 |
\<and> (rst!p)$ = #rpcA |
|
51 |
\<and> unchanged (caller rcv!p)" |
|
3807 | 52 |
|
17309 | 53 |
RPCReply_def: "RPCReply send rcv rst p == ACT |
60587 | 54 |
\<not>$(Calling rcv p) |
60591 | 55 |
\<and> $(rst!p) = #rpcB |
56 |
\<and> Return send p res<rcv!p> |
|
57 |
\<and> (rst!p)$ = #rpcA |
|
58 |
\<and> unchanged (caller rcv!p)" |
|
3807 | 59 |
|
17309 | 60 |
RPCNext_def: "RPCNext send rcv rst p == ACT |
6255 | 61 |
( RPCFwd send rcv rst p |
60591 | 62 |
\<or> RPCReject send rcv rst p |
63 |
\<or> RPCFail send rcv rst p |
|
64 |
\<or> RPCReply send rcv rst p)" |
|
3807 | 65 |
|
17309 | 66 |
RPCIPSpec_def: "RPCIPSpec send rcv rst p == TEMP |
6255 | 67 |
Init RPCInit rcv rst p |
60591 | 68 |
\<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p) |
69 |
\<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)" |
|
3807 | 70 |
|
60587 | 71 |
RPCISpec_def: "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)" |
17309 | 72 |
|
21624 | 73 |
|
74 |
lemmas RPC_action_defs = |
|
75 |
RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def |
|
76 |
||
77 |
lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def |
|
78 |
||
79 |
||
80 |
(* The RPC component engages in an action for process p only if there is an outstanding, |
|
81 |
unanswered call for that process. |
|
82 |
*) |
|
83 |
||
60588 | 84 |
lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p" |
21624 | 85 |
by (auto simp: Return_def RPC_action_defs) |
86 |
||
60591 | 87 |
lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p" |
21624 | 88 |
by (auto simp: RPC_action_defs) |
89 |
||
90 |
(* RPC failure actions are visible. *) |
|
60588 | 91 |
lemma RPCFail_vis: "\<turnstile> RPCFail send rcv rst p \<longrightarrow> |
21624 | 92 |
<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)" |
93 |
by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def) |
|
94 |
||
60588 | 95 |
lemma RPCFail_Next_enabled: "\<turnstile> Enabled (RPCFail send rcv rst p) \<longrightarrow> |
21624 | 96 |
Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))" |
97 |
by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use]) |
|
98 |
||
99 |
(* Enabledness of some actions *) |
|
60588 | 100 |
lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow> |
60591 | 101 |
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42018
diff
changeset
|
102 |
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def}, |
39159 | 103 |
@{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
104 |
[@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
|
21624 | 105 |
|
60588 | 106 |
lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow> |
60591 | 107 |
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB |
60588 | 108 |
\<longrightarrow> Enabled (RPCReply send rcv rst p)" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42018
diff
changeset
|
109 |
by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def}, |
39159 | 110 |
@{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
111 |
[@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
|
3807 | 112 |
|
113 |
end |