From a9637f6a7597e7adf4e6ff7ecc7699db80db18e1 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 12:30:16 +0100 Subject: [PATCH] PBTS model: minor fixes --- .../proposer-based-timestamp/pbts-sysmodel_002_draft.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index bf22e5ae6..f3e593d52 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -159,7 +159,6 @@ rounds, but the evaluation of the `timely` predicate is only relevant at round > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is > produced by the `getValue()` method, invoked by the proposer `p` of round > `round_p` when starting its proposing round with a nil `validValue_p`. -> > The first round at which a value `v` is proposed is then the round at which > the proposal for `v` was produced, and broadcast in a `PROPOSAL` message with > `vr = -1`. @@ -256,13 +255,12 @@ produced ensures that at least one correct process also observed a `POL(v,vr)`. > Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by > the proposer `p` of round `round_p` because its `validValue_p` variable was > set to `v`. -> > The broadcast `PROPOSAL` message, in this case, has its `vr > -1`, which can > only be accepted by processes that observed a `POL(v, vr)`. So, if there is a `POL(v,r)` with `r > v.round`, then there is a valid `POL(v,vr)` with `v.round <= vr < r`. -From this point, the reasoning becomes recursive: either `vr == v.round` and +From this point, the reasoning becomes recursive: either `vr = v.round` and `POL(v,vr)` is a timely proof-of-lock, or there is another `POL(v,vr')` with `vr' < vr`, recursively leading to the first scenario (as `vr` necessarily decreases at each recursive iteration).