I'm trying to model a consensus algorithm, in which a common coin (a distributed random number) is used to overcome the FLP impossibility.
The termination of the algorithm is based on the fact that by repeating the coin flips we will get the needed value eventually (because of the uniform randomness, as I understand).
The below spec does not model the entire algorithm, just the part with the common coin.
Does it look reasonable to model that "eventual" with <>done as a fairness assumption?
I'm not sure. It sounds a bit like assuming the conclusion, but on the other hand I'm not trying to prove that probabilistic property, just use it.
In this example Decides looks similar to Live, but in the final spec the Decides property would be different.
------------- MODULE CommonCoinConverges --------------
EXTENDS TLAPS
VARIABLE val
VARIABLE done
vars == <<val, done>>
Round == /\ ~done
/\ \E newCoin \in BOOLEAN : \* Take a new random number.
/\ done' = (newCoin = val) \* Check, if the value is lucky.
/\ val' = newCoin
Terminated == done /\ UNCHANGED vars \* Just to avoid a deadlock in a proof bellow.
Init == /\ val \in BOOLEAN
/\ done = FALSE
Next == Round \/ Terminated
Live == <>done
Spec == Init /\ [][Next]_vars /\ Live
---------------------------------------------------------
TypeOK == /\ val \in BOOLEAN
/\ done \in BOOLEAN
Decides == <>[]done
THEOREM Spec => []TypeOK /\ Decides
=========================================================
As a side note, I managed to prove the above theorem in TLAPS from the updated_enabled_cdot branch by looking
Although I'm still not sure if I would be able to do that again :) The proof tactics for temporal operators are not clear to me.
Maybe there is a paper or a book on such tactics that I should read before trying to prove something like this? :)
THEOREM Spec => []TypeOK /\ Decides
<1>1. Spec => []TypeOK
<2>1. Init => TypeOK BY DEF Init, TypeOK
<2>2. TypeOK /\ [Next]_vars => TypeOK'
<3> SUFFICES ASSUME TypeOK, Next PROVE TypeOK' BY DEF vars, TypeOK
<3> CASE Round BY DEF Round, TypeOK
<3> CASE Terminated BY DEF Terminated, TypeOK, vars
<3>q. QED BY DEF TypeOK, Next, Round, Terminated
<2>q. QED BY <2>1, <2>2, PTL DEF Spec
<1>2. Spec => Decides
<2>x. TypeOK /\ Spec => [] (~done \/ []done)
<3>1. ASSUME TypeOK /\ [Next]_vars PROVE ~done \/ done'
<4> SUFFICES ASSUME TypeOK, Next PROVE ~done \/ (done') BY <3>1 DEF vars
<4> CASE Round BY DEF Round
<4> CASE Terminated BY DEF Terminated, vars
<4> QED BY DEF Next
<3>q. QED BY <3>1, <1>1, PTL DEF Spec
<2>q. QED BY <1>1, <2>x, PTL DEF Spec, Live, Decides
<1>q. QED BY <1>1, <1>2
Sincerely,
Karolis Petrauskas