search

informalsystems / verification

Specifications of the protocols and the experiments on their verification
9 stars 2 forks source link

Discrepancy in IsCorrectPowerForSet docs and implementation #8

Open OStevan opened 4 years ago

OStevan commented 4 years ago

Docs which explain the check which is supposed to be done by the function IsCorrectPowerForSet tell us that the inequality which should be used is CP > 2 / 3 FP. However, the function is written in terms of CP > 2 / 3 TP which is what it should be (as far as I understand). @milosevic @konnov

konnov commented 4 years ago

Theoretically, there is no big difference at the specification level between writing 3 * CP > 2 * TP and CP > 2 * FP. (Note that although it is customary to write 2/3 in distributed algorithms, this is incorrect in integer arithmetics, due to integer truncation). In terms of running the model checkers (TLC and Apalache), the form CP > 2 * FP is more preferable, as the constructed sets are smaller.

konnov commented 4 years ago

I guess, there is a typo in the first constraint CP > 2 / 3 FP, as the assumption about the number of faults should be TP = CP + FP > 3 * FP

OStevan commented 4 years ago

Yes, that was my impression that there is a typo.

ebuchman commented 4 years ago

Is this fixed in the tendermint-rs repo?