author | wenzelm |
Fri, 26 Jun 2015 11:44:22 +0200 | |
changeset 60587 | 0318b43ee95c |
parent 58889 | 5b7a9633cfa8 |
child 60588 | 750c533459b1 |
permissions | -rw-r--r-- |
41589 | 1 |
(* Title: HOL/TLA/Memory/MemClerk.thy |
2 |
Author: Stephan Merz, University of Munich |
|
21624 | 3 |
*) |
3807 | 4 |
|
58889 | 5 |
section {* RPC-Memory example: specification of the memory clerk *} |
3807 | 6 |
|
17309 | 7 |
theory MemClerk |
8 |
imports Memory RPC MemClerkParameters |
|
9 |
begin |
|
3807 | 10 |
|
42018 | 11 |
(* The clerk takes the same arguments as the memory and sends requests to the RPC *) |
12 |
type_synonym mClkSndChType = "memChType" |
|
13 |
type_synonym mClkRcvChType = "rpcSndChType" |
|
14 |
type_synonym mClkStType = "(PrIds => mClkState) stfun" |
|
3807 | 15 |
|
36866 | 16 |
definition |
3807 | 17 |
(* state predicates *) |
18 |
MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" |
|
60587 | 19 |
where "MClkInit rcv cst p = PRED (cst!p = #clkA & \<not>Calling rcv p)" |
3807 | 20 |
|
36866 | 21 |
definition |
3807 | 22 |
(* actions *) |
23 |
MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
|
36866 | 24 |
where "MClkFwd send rcv cst p = ACT |
6255 | 25 |
$Calling send p |
26 |
& $(cst!p) = #clkA |
|
27 |
& Call rcv p MClkRelayArg<arg<send!p>> |
|
28 |
& (cst!p)$ = #clkB |
|
29 |
& unchanged (rtrner send!p)" |
|
30 |
||
36866 | 31 |
definition |
3807 | 32 |
MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
36866 | 33 |
where "MClkRetry send rcv cst p = ACT |
6255 | 34 |
$(cst!p) = #clkB |
35 |
& res<$(rcv!p)> = #RPCFailure |
|
36 |
& Call rcv p MClkRelayArg<arg<send!p>> |
|
37 |
& unchanged (cst!p, rtrner send!p)" |
|
38 |
||
36866 | 39 |
definition |
3807 | 40 |
MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
36866 | 41 |
where "MClkReply send rcv cst p = ACT |
60587 | 42 |
\<not>$Calling rcv p |
6255 | 43 |
& $(cst!p) = #clkB |
44 |
& Return send p MClkReplyVal<res<rcv!p>> |
|
45 |
& (cst!p)$ = #clkA |
|
46 |
& unchanged (caller rcv!p)" |
|
47 |
||
36866 | 48 |
definition |
3807 | 49 |
MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
36866 | 50 |
where "MClkNext send rcv cst p = ACT |
6255 | 51 |
( MClkFwd send rcv cst p |
52 |
| MClkRetry send rcv cst p |
|
53 |
| MClkReply send rcv cst p)" |
|
54 |
||
36866 | 55 |
definition |
3807 | 56 |
(* temporal *) |
57 |
MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" |
|
36866 | 58 |
where "MClkIPSpec send rcv cst p = TEMP |
6255 | 59 |
Init MClkInit rcv cst p |
60587 | 60 |
& \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p) |
6255 | 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)" |
|
3807 | 63 |
|
36866 | 64 |
definition |
6255 | 65 |
MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" |
60587 | 66 |
where "MClkISpec send rcv cst = TEMP (\<forall>p. MClkIPSpec send rcv cst p)" |
3807 | 67 |
|
21624 | 68 |
lemmas MC_action_defs = |
69 |
MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def |
|
70 |
||
71 |
lemmas MC_temp_defs = MClkIPSpec_def MClkISpec_def |
|
72 |
||
73 |
(* The Clerk engages in an action for process p only if there is an outstanding, |
|
74 |
unanswered call for that process. |
|
75 |
*) |
|
60587 | 76 |
lemma MClkidle: "|- \<not>$Calling send p & $(cst!p) = #clkA --> \<not>MClkNext send rcv cst p" |
21624 | 77 |
by (auto simp: Return_def MC_action_defs) |
78 |
||
60587 | 79 |
lemma MClkbusy: "|- $Calling rcv p --> \<not>MClkNext send rcv cst p" |
21624 | 80 |
by (auto simp: Call_def MC_action_defs) |
81 |
||
82 |
||
83 |
(* Enabledness of actions *) |
|
84 |
||
60587 | 85 |
lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> |
86 |
|- Calling send p & \<not>Calling rcv p & cst!p = #clkA |
|
21624 | 87 |
--> Enabled (MClkFwd send rcv cst p)" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42018
diff
changeset
|
88 |
by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def}, |
26359 | 89 |
@{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
90 |
[@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
|
21624 | 91 |
|
92 |
lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p) --> |
|
93 |
Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
|
94 |
by (auto elim!: enabled_mono simp: angle_def MClkFwd_def) |
|
95 |
||
96 |
lemma MClkReply_change: "|- MClkReply send rcv cst p --> |
|
97 |
<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)" |
|
98 |
by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use]) |
|
99 |
||
60587 | 100 |
lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> |
101 |
|- Calling send p & \<not>Calling rcv p & cst!p = #clkB |
|
21624 | 102 |
--> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42018
diff
changeset
|
103 |
apply (tactic {* action_simp_tac @{context} |
26359 | 104 |
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *}) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42018
diff
changeset
|
105 |
apply (tactic {* action_simp_tac (@{context} addsimps |
26359 | 106 |
[@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) |
107 |
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
|
21624 | 108 |
done |
109 |
||
60587 | 110 |
lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> \<not>MClkRetry send rcv cst p" |
21624 | 111 |
by (auto simp: MClkReply_def MClkRetry_def) |
17309 | 112 |
|
3807 | 113 |
end |