section ‹The $A_{T,E}$ Algorithm› theory Ate_Defs imports Heard_Of.HOModel "../Consensus_Types" begin text ‹The contents of this file have been taken almost verbatim from the Heard Of Model AFP entry. The only difference is that the types have been changed.› subsection ‹Model of the algorithm› text ‹The following record models the local state of a process.› record 'val pstate = x :: "'val" ― ‹current value held by process› decide :: "'val option" ― ‹value the process has decided on, if any› text ‹ The ‹x› field of the initial state is unconstrained, but no decision has yet been taken. › definition Ate_initState where "Ate_initState p st ≡ (decide st = None)" locale ate_parameters = fixes α::nat and T::nat and E::nat assumes TNaE:"T ≥ 2*(N + 2*α - E)" and TltN:"T < N" and EltN:"E < N" begin text ‹The following are consequences of the assumptions on the parameters.› lemma majE: "2 * (E - α) ≥ N" using TNaE TltN by auto lemma Egta: "E > α" using majE EltN by auto lemma Tge2a: "T ≥ 2 * α" using TNaE EltN by auto text ‹ At every round, each process sends its current ‹x›. If it received more than ‹T› messages, it selects the smallest value and store it in ‹x›. As in algorithm \emph{OneThirdRule}, we therefore require values to be linearly ordered. If more than ‹E› messages holding the same value are received, the process decides that value. › definition mostOftenRcvd where "mostOftenRcvd (msgs::process ⇒ 'val option) ≡ {v. ∀w. card {qq. msgs qq = Some w} ≤ card {qq. msgs qq = Some v}}" definition Ate_sendMsg :: "nat ⇒ process ⇒ process ⇒ 'val pstate ⇒ 'val" where "Ate_sendMsg r p q st ≡ x st" definition Ate_nextState :: "nat ⇒ process ⇒ ('val::linorder) pstate ⇒ (process ⇒ 'val option) ⇒ 'val pstate ⇒ bool" where "Ate_nextState r p st msgs st' ≡ (if card {q. msgs q ≠ None} > T then x st' = Min (mostOftenRcvd msgs) else x st' = x st) ∧ ( (∃v. card {q. msgs q = Some v} > E ∧ decide st' = Some v) ∨ ¬ (∃v. card {q. msgs q = Some v} > E) ∧ decide st' = decide st)" subsection ‹Communication predicate for $A_{T,E}$› definition Ate_commPerRd where "Ate_commPerRd HOrs SHOrs ≡ ∀p. card (HOrs p - SHOrs p) ≤ α" text ‹ The global communication predicate stipulates the three following conditions: \begin{itemize} \item for every process ‹p› there are infinitely many rounds where ‹p› receives more than ‹T› messages, \item for every process ‹p› there are infinitely many rounds where ‹p› receives more than ‹E› uncorrupted messages, \item and there are infinitely many rounds in which more than ‹E - α› processes receive uncorrupted messages from the same set of processes, which contains more than ‹T› processes. \end{itemize} › definition Ate_commGlobal where "Ate_commGlobal HOs SHOs ≡ (∀r p. ∃r' > r. card (HOs r' p) > T) ∧ (∀r p. ∃r' > r. card (SHOs r' p ∩ HOs r' p) > E) ∧ (∀r. ∃r' > r. ∃π1 π2. card π1 > E - α ∧ card π2 > T ∧ (∀p ∈ π1. HOs r' p = π2 ∧ SHOs r' p ∩ HOs r' p = π2))" subsection ‹The $A_{T,E}$ Heard-Of machine› text ‹ We now define the non-coordinated SHO machine for the Ate algorithm by assembling the algorithm definition and its communication-predicate. › definition Ate_SHOMachine where "Ate_SHOMachine = ⦇ CinitState = (λ p st crd. Ate_initState p (st::('val::linorder) pstate)), sendMsg = Ate_sendMsg, CnextState = (λ r p st msgs crd st'. Ate_nextState r p st msgs st'), SHOcommPerRd = (Ate_commPerRd:: process HO ⇒ process HO ⇒ bool), SHOcommGlobal = Ate_commGlobal ⦈" abbreviation "Ate_M ≡ (Ate_SHOMachine::(process, 'val::linorder pstate, 'val) SHOMachine)" end ― ‹locale @{text "ate_parameters"}› end (* theory AteDefs *)