Theory CT_Defs
section ‹Chandra-Toueg $\diamond S$ Algorithm›
theory CT_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" Three_Steps
begin
text ‹
The following record models the local state of a process.
›
record 'val pstate =
x :: 'val
mru_vote :: "(nat × 'val) option"
commt :: "'val"
decide :: "'val option"
text ‹The algorithm relies on a coordinator for each phase of the algorithm.
A phase lasts three rounds. The HO model formalization already provides the
infrastructure for this, but unfortunately the coordinator is not passed to
the @{term sendMsg} function. Using the infrastructure would thus require
additional invariants and proofs; for simplicity, we use a global
constant instead.›
consts coord :: "nat ⇒ process"
specification (coord)
coord_phase[rule_format]: "∀r r'. three_phase r = three_phase r' ⟶ coord r = coord r'"
by(auto)
text ‹
Possible messages sent during the execution of the algorithm.
›