author | wenzelm |
Thu, 20 Mar 2008 16:54:11 +0100 | |
changeset 26365 | e6d3714b8853 |
parent 26359 | 6d437bde2f1d |
child 36866 | 426d5781bb25 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: MemClerk.thy |
|
17309 | 3 |
ID: $Id$ |
3807 | 4 |
Author: Stephan Merz |
5 |
Copyright: 1997 University of Munich |
|
21624 | 6 |
*) |
3807 | 7 |
|
21624 | 8 |
header {* RPC-Memory example: specification of the memory clerk *} |
3807 | 9 |
|
17309 | 10 |
theory MemClerk |
11 |
imports Memory RPC MemClerkParameters |
|
12 |
begin |
|
3807 | 13 |
|
14 |
types |
|
15 |
(* The clerk takes the same arguments as the memory and sends requests to the RPC *) |
|
16 |
mClkSndChType = "memChType" |
|
17 |
mClkRcvChType = "rpcSndChType" |
|
18 |
mClkStType = "(PrIds => mClkState) stfun" |
|
19 |
||
6255 | 20 |
constdefs |
3807 | 21 |
(* state predicates *) |
22 |
MClkInit :: "mClkRcvChType => mClkStType => PrIds => stpred" |
|
6255 | 23 |
"MClkInit rcv cst p == PRED (cst!p = #clkA & ~Calling rcv p)" |
3807 | 24 |
|
25 |
(* actions *) |
|
26 |
MClkFwd :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
|
6255 | 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 |
||
3807 | 34 |
MClkRetry :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
6255 | 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 |
||
3807 | 41 |
MClkReply :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
6255 | 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 |
||
3807 | 49 |
MClkNext :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => action" |
6255 | 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 |
||
3807 | 55 |
|
56 |
(* temporal *) |
|
57 |
MClkIPSpec :: "mClkSndChType => mClkRcvChType => mClkStType => PrIds => temporal" |
|
6255 | 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)" |
|
3807 | 63 |
|
6255 | 64 |
MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal" |
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
6255
diff
changeset
|
65 |
"MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)" |
3807 | 66 |
|
21624 | 67 |
lemmas MC_action_defs = |
68 |
MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def |
|
69 |
||
70 |
lemmas MC_temp_defs = MClkIPSpec_def MClkISpec_def |
|
71 |
||
72 |
(* The Clerk engages in an action for process p only if there is an outstanding, |
|
73 |
unanswered call for that process. |
|
74 |
*) |
|
75 |
lemma MClkidle: "|- ~$Calling send p & $(cst!p) = #clkA --> ~MClkNext send rcv cst p" |
|
76 |
by (auto simp: Return_def MC_action_defs) |
|
77 |
||
78 |
lemma MClkbusy: "|- $Calling rcv p --> ~MClkNext send rcv cst p" |
|
79 |
by (auto simp: Call_def MC_action_defs) |
|
80 |
||
81 |
||
82 |
(* Enabledness of actions *) |
|
83 |
||
84 |
lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> |
|
85 |
|- Calling send p & ~Calling rcv p & cst!p = #clkA |
|
86 |
--> Enabled (MClkFwd send rcv cst p)" |
|
26359 | 87 |
by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def}, |
88 |
@{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] |
|
89 |
[@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
|
21624 | 90 |
|
91 |
lemma MClkFwd_ch_enabled: "|- Enabled (MClkFwd send rcv cst p) --> |
|
92 |
Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
|
93 |
by (auto elim!: enabled_mono simp: angle_def MClkFwd_def) |
|
94 |
||
95 |
lemma MClkReply_change: "|- MClkReply send rcv cst p --> |
|
96 |
<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)" |
|
97 |
by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use]) |
|
98 |
||
99 |
lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==> |
|
100 |
|- Calling send p & ~Calling rcv p & cst!p = #clkB |
|
101 |
--> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))" |
|
26342 | 102 |
apply (tactic {* action_simp_tac @{simpset} |
26359 | 103 |
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *}) |
26342 | 104 |
apply (tactic {* action_simp_tac (@{simpset} addsimps |
26359 | 105 |
[@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) |
106 |
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) |
|
21624 | 107 |
done |
108 |
||
109 |
lemma MClkReplyNotRetry: "|- MClkReply send rcv cst p --> ~MClkRetry send rcv cst p" |
|
110 |
by (auto simp: MClkReply_def MClkRetry_def) |
|
17309 | 111 |
|
3807 | 112 |
end |