author | oheimb |
Wed, 03 Apr 2002 10:21:13 +0200 | |
changeset 13076 | 70704dd48bd5 |
parent 9517 | f58863b1406a |
child 17309 | c43ed29bd197 |
permissions | -rw-r--r-- |
3807 | 1 |
(* |
2 |
File: RPC.ML |
|
3 |
Author: Stephan Merz |
|
4 |
Copyright: 1997 University of Munich |
|
5 |
||
6255 | 6 |
RPC-Memory example: RPC specification (theorems and proofs) |
3807 | 7 |
*) |
8 |
||
6255 | 9 |
val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def, |
10 |
RPCReply_def, RPCNext_def]; |
|
3807 | 11 |
|
12 |
val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def]; |
|
13 |
||
6255 | 14 |
val mem_css = (claset(), simpset()); |
15 |
||
3807 | 16 |
(* The RPC component engages in an action for process p only if there is an outstanding, |
17 |
unanswered call for that process. |
|
18 |
*) |
|
19 |
||
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
20 |
Goal "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
21 |
by (auto_tac (mem_css addsimps2 (Return_def::RPC_action_defs))); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
22 |
qed "RPCidle"; |
3807 | 23 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
24 |
Goal "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
25 |
by (auto_tac (mem_css addsimps2 RPC_action_defs)); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
26 |
qed "RPCbusy"; |
3807 | 27 |
|
28 |
(* RPC failure actions are visible. *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
29 |
Goal "|- RPCFail send rcv rst p --> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
30 |
\ <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
31 |
by (auto_tac (claset() addSDs [Return_changed], |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
32 |
simpset() addsimps [angle_def,RPCNext_def,RPCFail_def])); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
33 |
qed "RPCFail_vis"; |
3807 | 34 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
35 |
Goal "|- Enabled (RPCFail send rcv rst p) --> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
36 |
\ Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
37 |
by (force_tac (mem_css addSEs2 [enabled_mono,RPCFail_vis]) 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
38 |
qed "RPCFail_Next_enabled"; |
3807 | 39 |
|
40 |
(* Enabledness of some actions *) |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
41 |
Goal "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
42 |
\ |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
43 |
by (action_simp_tac (simpset() addsimps [RPCFail_def,Return_def,caller_def,rtrner_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
44 |
[exI] [base_enabled,Pair_inject] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
45 |
qed "RPCFail_enabled"; |
3807 | 46 |
|
9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
47 |
Goal "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
48 |
\ |- ~Calling rcv p & Calling send p & rst!p = #rpcB \ |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
49 |
\ --> Enabled (RPCReply send rcv rst p)"; |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
50 |
by (action_simp_tac (simpset() addsimps [RPCReply_def,Return_def,caller_def,rtrner_def]) |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
51 |
[exI] [base_enabled,Pair_inject] 1); |
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7881
diff
changeset
|
52 |
qed "RPCReply_enabled"; |