(* Title: HOL/TLA/Memory/MemClerk.thy
Author: Stephan Merz, University of Munich
*)
section \<open>RPC-Memory example: specification of the memory clerk\<close>
theory MemClerk
imports Memory RPC MemClerkParameters
begin
(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
type_synonym mClkSndChType = "memChType"
type_synonym mClkRcvChType = "rpcSndChType"
type_synonym mClkStType = "(PrIds \<Rightarrow> mClkState) stfun"
definition
(* state predicates *)
MClkInit :: "mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> stpred"
where "MClkInit rcv cst p = PRED (cst!p = #clkA \<and> \<not>Calling rcv p)"
definition
(* actions *)
MClkFwd :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkFwd send rcv cst p = ACT
$Calling send p
\<and> $(cst!p) = #clkA
\<and> Call rcv p MClkRelayArg<arg<send!p>>
\<and> (cst!p)$ = #clkB
\<and> unchanged (rtrner send!p)"
definition
MClkRetry :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkRetry send rcv cst p = ACT
$(cst!p) = #clkB
\<and> res<$(rcv!p)> = #RPCFailure
\<and> Call rcv p MClkRelayArg<arg<send!p>>
\<and> unchanged (cst!p, rtrner send!p)"
definition
MClkReply :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkReply send rcv cst p = ACT
\<not>$Calling rcv p
\<and> $(cst!p) = #clkB
\<and> Return send p MClkReplyVal<res<rcv!p>>
\<and> (cst!p)$ = #clkA
\<and> unchanged (caller rcv!p)"
definition
MClkNext :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
where "MClkNext send rcv cst p = ACT
( MClkFwd send rcv cst p
\<or> MClkRetry send rcv cst p
\<or> MClkReply send rcv cst p)"
definition
(* temporal *)
MClkIPSpec :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> temporal"
where "MClkIPSpec send rcv cst p = TEMP
Init MClkInit rcv cst p
\<and> \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
\<and> WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
\<and> SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
definition
MClkISpec :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> temporal"
where "MClkISpec send rcv cst = TEMP (\<forall>p. MClkIPSpec send rcv cst p)"
lemmas MC_action_defs =
MClkInit_def MClkFwd_def MClkRetry_def MClkReply_def MClkNext_def
lemmas MC_temp_defs = MClkIPSpec_def MClkISpec_def
(* The Clerk engages in an action for process p only if there is an outstanding,
unanswered call for that process.
*)
lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
by (auto simp: AReturn_def MC_action_defs)
lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
by (auto simp: ACall_def MC_action_defs)
(* Enabledness of actions *)
lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>
\<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA
\<longrightarrow> Enabled (MClkFwd send rcv cst p)"
by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm MClkFwd_def},
@{thm ACall_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p) \<longrightarrow>
Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
by (auto elim!: enabled_mono simp: angle_def MClkFwd_def)
lemma MClkReply_change: "\<turnstile> MClkReply send rcv cst p \<longrightarrow>
<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p)"
by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use])
lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>
\<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkB
\<longrightarrow> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
apply (tactic \<open>action_simp_tac \<^context>
[@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
apply (tactic \<open>action_simp_tac (\<^context> addsimps
[@{thm MClkReply_def}, @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}])
[exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
done
lemma MClkReplyNotRetry: "\<turnstile> MClkReply send rcv cst p \<longrightarrow> \<not>MClkRetry send rcv cst p"
by (auto simp: MClkReply_def MClkRetry_def)
end