3807
|
1 |
(*
|
|
2 |
File: MemClerk.ML
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
5 |
|
|
6 |
RPC-Memory example: Memory clerk specification (ML file)
|
|
7 |
*)
|
|
8 |
|
|
9 |
val MC_action_defs =
|
|
10 |
[MClkInit_def RS inteq_reflection]
|
|
11 |
@ [MClkFwd_def, MClkRetry_def, MClkReply_def, MClkNext_def];
|
|
12 |
|
|
13 |
val MC_temp_defs = [MClkIPSpec_def, MClkISpec_def];
|
|
14 |
|
|
15 |
(* The Clerk engages in an action for process p only if there is an outstanding,
|
|
16 |
unanswered call for that process.
|
|
17 |
*)
|
|
18 |
|
|
19 |
qed_goal "MClkidle" MemClerk.thy
|
|
20 |
".~ $(Calling send p) .& ($(cst@p) .= #clkA) .-> .~ MClkNext send rcv cst p"
|
4089
|
21 |
(fn _ => [ auto_tac (claset(),
|
|
22 |
simpset() addsimps (MC_action_defs @ [Return_def]))
|
3807
|
23 |
]);
|
|
24 |
|
|
25 |
qed_goal "MClkbusy" MemClerk.thy
|
|
26 |
"$(Calling rcv p) .-> .~ MClkNext send rcv cst p"
|
4089
|
27 |
(fn _ => [ auto_tac (claset(),
|
|
28 |
simpset() addsimps (MC_action_defs @ [Call_def]))
|
3807
|
29 |
]);
|
|
30 |
|
|
31 |
(* unlifted versions as introduction rules *)
|
|
32 |
|
|
33 |
bind_thm("MClkidleI", action_mp MClkidle);
|
|
34 |
bind_thm("MClkbusyI", action_mp MClkbusy);
|
|
35 |
|
|
36 |
(* Enabledness of actions *)
|
|
37 |
|
|
38 |
qed_goal "MClkFwd_enabled" MemClerk.thy
|
|
39 |
"!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
|
|
40 |
\ $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkA) \
|
|
41 |
\ .-> $(Enabled (MClkFwd send rcv cst p))"
|
4089
|
42 |
(fn _ => [action_simp_tac (simpset() addsimps [MClkFwd_def,Call_def,caller_def,rtrner_def])
|
3807
|
43 |
[] [base_enabled,Pair_inject] 1]);
|
|
44 |
|
|
45 |
qed_goal "MClkFwd_ch_enabled" MemClerk.thy
|
|
46 |
"Enabled (MClkFwd send rcv cst p) s \
|
|
47 |
\ ==> Enabled (<MClkFwd send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>) s"
|
4089
|
48 |
(fn [prem] => [auto_tac (claset() addSIs [prem RS enabled_mono],
|
|
49 |
simpset() addsimps [angle_def,MClkFwd_def])
|
3807
|
50 |
]);
|
|
51 |
|
|
52 |
qed_goal "MClkReply_change" MemClerk.thy
|
|
53 |
"MClkReply send rcv cst p .-> <MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>"
|
|
54 |
(fn _ => [auto_tac (action_css addsimps2 [angle_def,MClkReply_def]
|
|
55 |
addEs2 [Return_changedE])
|
|
56 |
]);
|
|
57 |
|
|
58 |
qed_goal "MClkReply_enabled" MemClerk.thy
|
|
59 |
"!!p. base_var <rtrner send @ p, caller rcv @ p, cst@p> ==> \
|
|
60 |
\ $(Calling send p) .& .~ $(Calling rcv p) .& ($(cst@p) .= #clkB) \
|
|
61 |
\ .-> $(Enabled (<MClkReply send rcv cst p>_<cst@p, rtrner send @ p, caller rcv @ p>))"
|
4089
|
62 |
(fn _ => [action_simp_tac (simpset()) [MClkReply_change RSN (2,enabled_mono)] [] 1,
|
|
63 |
action_simp_tac (simpset() addsimps [MClkReply_def,Return_def,caller_def,rtrner_def])
|
3807
|
64 |
[] [base_enabled,Pair_inject] 1
|
|
65 |
]);
|
|
66 |
|
|
67 |
qed_goal "MClkReplyNotRetry" MemClerk.thy
|
|
68 |
"MClkReply send rcv cst p .-> .~(MClkRetry send rcv cst p)"
|
4089
|
69 |
(fn _ => [ auto_tac (claset(),
|
|
70 |
simpset() addsimps [MClkReply_def,MClkRetry_def])
|
3807
|
71 |
]);
|