From 50f079a8caac5cd83fc7a0a146a7449f250cbbc3 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 10:51:08 +0100 Subject: [PATCH] PBTS model: some formatting changes --- .../pbts-sysmodel_002_draft.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 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 8ac6a0e25..c09218590 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -92,7 +92,7 @@ such for any two correct processes `p` and `q`: Notice that, as a system parameter, `MSGDELAY` should be observed for any proposal message broadcast by correct processes: it is a *worst-case* parameter. -As message delays depends on the message size, the above requirement implicty +As message delays depends on the message size, the above requirement implicitly indicates that the size of proposal messages is either fixed or upper bounded. ## Problem Statement @@ -143,30 +143,31 @@ The property is based in the `timely` predicate defined in the following: #### **[PBTS-INV-TIMELY.0]** - [Time-Validity] If a correct process decides on value `v`, then the proposal - message proposing `v` was considered `timely` by at least `f+1` processes. + of `v` was considered `timely` by at least `f+1` processes. The `timely` predicate is evaluated when a process receives a proposal in a round of consensus. + A proposal is a tuple `(v, v.time, v.round)`, where `v` is the proposed value, `v.time` the proposal time, and `v.round` is the round at which `v` was first -proposed (and `v.time` was assigned). +proposed---so `v.time` and `v.round` were assigned. While the same proposal can be proposed multiple time, in different rounds of -consensus, we are interested on the first time it was proposed: +consensus, the `timely` predicate is verfied in the first time it was proposed: -##### **[PBTS-RECEPTION-STEP.0]** +#### **[PBTS-PROPOSAL-RECEPTION.0]** Let `p` be a correct process which is at round `r` of consensus: - `receiveTime_p[r]` is the time `p` reads from its local clock when it receives the proposal `(v, v.time, v.round)` with `v.round = r`. -##### **[PBTS-TIMELY.0]** +#### **[PBTS-TIMELY.0]** The proposal `(v, v.time, v.round)` for `v` is considered `timely` by a correct process `p` if: 1. `receiveTime_p[v.round] >= v.time - PRECISION` and -1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION` +1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. ### Timely Proof-of-Locks