(* File: RPC.ML ID: $Id: RPC.ML,v 1.6 2005/09/07 18:22:43 wenzelm Exp $ Author: Stephan Merz Copyright: 1997 University of Munich RPC-Memory example: RPC specification (theorems and proofs) *) val RPC_action_defs = [RPCInit_def, RPCFwd_def, RPCReject_def, RPCFail_def, RPCReply_def, RPCNext_def]; val RPC_temp_defs = [RPCIPSpec_def, RPCISpec_def]; val mem_css = (claset(), simpset()); (* The RPC component engages in an action for process p only if there is an outstanding, unanswered call for that process. *) Goal "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"; by (auto_tac (mem_css addsimps2 (Return_def::RPC_action_defs))); qed "RPCidle"; Goal "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"; by (auto_tac (mem_css addsimps2 RPC_action_defs)); qed "RPCbusy"; (* RPC failure actions are visible. *) Goal "|- RPCFail send rcv rst p --> \ \ <RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"; by (auto_tac (claset() addSDs [Return_changed], simpset() addsimps [angle_def,RPCNext_def,RPCFail_def])); qed "RPCFail_vis"; Goal "|- Enabled (RPCFail send rcv rst p) --> \ \ Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"; by (force_tac (mem_css addSEs2 [enabled_mono,RPCFail_vis]) 1); qed "RPCFail_Next_enabled"; (* Enabledness of some actions *) Goal "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> \ \ |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"; by (action_simp_tac (simpset() addsimps [RPCFail_def,Return_def,caller_def,rtrner_def]) [exI] [base_enabled,Pair_inject] 1); qed "RPCFail_enabled"; Goal "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> \ \ |- ~Calling rcv p & Calling send p & rst!p = #rpcB \ \ --> Enabled (RPCReply send rcv rst p)"; by (action_simp_tac (simpset() addsimps [RPCReply_def,Return_def,caller_def,rtrner_def]) [exI] [base_enabled,Pair_inject] 1); qed "RPCReply_enabled";