Theory New_Algorithm_Defs
section ‹The New Algorithm›
theory New_Algorithm_Defs
imports Heard_Of.HOModel "../Consensus_Types" "../Consensus_Misc" Three_Steps
begin
subsection ‹Model of the algorithm›
text ‹We assume that the values are linearly ordered, to be able to have each process
select the smallest value.›
axiomatization where val_linorder:
"OFCLASS(val, linorder_class)"
instance val :: linorder by (rule val_linorder)
record pstate =
x :: val
prop_vote :: "val option"
mru_vote :: "(nat × val) option"
decide :: "val option"