Compare commits

...

37 Commits

Author SHA1 Message Date
Kukovec
e8d239c64a readme update 2 2022-05-31 16:38:31 +02:00
Kukovec
fefc49fc10 readme update 2022-05-31 16:28:31 +02:00
Kukovec
ae786b6751 More precise notes 2022-05-31 16:22:24 +02:00
Kukovec
8a56b81c18 experiments 2022-05-31 16:20:49 +02:00
Kukovec
24ea13790d PR comments 2022-05-31 15:45:54 +02:00
Daniel Cason
6bc95409ce Results of running make mockery 2022-05-25 12:46:51 +02:00
Daniel Cason
be61f581fd Merge remote-tracking branch 'origin' into main/pbts 2022-05-25 12:42:55 +02:00
Daniel Cason
fcd560282f Merge branch 'main/pbts' of github.com:tendermint/tendermint into main/pbts 2022-05-25 12:36:18 +02:00
Daniel Cason
be7e3ddada PBTS spec: link to Github project with related issues 2022-05-25 12:34:39 +02:00
Daniel Cason
387c8570fa PBTS: added deprecation note on BFTTime documentation 2022-05-24 18:28:31 +02:00
Daniel Cason
0fd04d45bf PBTS spec: fixing and/or removing broken links 2022-05-24 18:28:31 +02:00
Daniel Cason
35abab42c4 Spec/consensus: references (links) to BFTTime updated 2022-05-24 18:28:31 +02:00
Daniel Cason
3c88e2a0bc Spec: outdated BFTTime documentation removed
* The file was actually moved to the PBTS spec repository
2022-05-24 18:28:31 +02:00
Daniel Cason
d83dd53825 Spec: consensus/block Time initial specification 2022-05-24 18:28:31 +02:00
Daniel Cason
455ad37d4e PBTS: using proper Markdown subscripts in spec 2022-05-24 18:28:31 +02:00
Daniel Cason
e9e2a0c63f PBTS: redundant not changes in algorithm removed 2022-05-24 18:28:31 +02:00
Daniel Cason
798bd3c4c6 PBTS: changes in arXiv algorithm made more clear 2022-05-24 18:28:31 +02:00
Daniel Cason
e6d1f7d96e PBTS: using proper Markdown subscripts in spec [2] 2022-05-24 18:28:31 +02:00
Daniel Cason
ce628dec1a PBTS: using proper Markdown subscripts in spec 2022-05-24 18:28:31 +02:00
Daniel Cason
36d74b7f59 PBTS: reference to v1 removed from algorithmic spec 2022-05-24 18:28:31 +02:00
Kukovec
6c09780776 formatting 2022-05-24 18:28:31 +02:00
Kukovec
60f0f7bcd0 run script/docs 2022-05-24 18:28:31 +02:00
Kukovec
aa8581a9f0 move + rename 2022-05-24 18:28:31 +02:00
Daniel Cason
c251a59d0e PBTS: added deprecation note on BFTTime documentation 2022-05-24 16:49:18 +02:00
Daniel Cason
4f9cb80836 PBTS spec: fixing and/or removing broken links 2022-05-24 16:34:45 +02:00
Daniel Cason
85290686c3 Spec/consensus: references (links) to BFTTime updated 2022-05-24 16:14:22 +02:00
Daniel Cason
c7738bfb06 Spec: outdated BFTTime documentation removed
* The file was actually moved to the PBTS spec repository
2022-05-24 16:10:49 +02:00
Daniel Cason
5c7a1ea45c Spec: consensus/block Time initial specification 2022-05-24 16:09:42 +02:00
Daniel Cason
4aab6be8eb PBTS: using proper Markdown subscripts in spec 2022-05-12 17:35:02 +02:00
Daniel Cason
3354c1aebb PBTS: redundant not changes in algorithm removed 2022-05-12 17:20:41 +02:00
Daniel Cason
ba137f9c85 PBTS: changes in arXiv algorithm made more clear 2022-05-12 17:17:12 +02:00
Daniel Cason
0d3c1ddbbd PBTS: using proper Markdown subscripts in spec [2] 2022-05-12 17:06:45 +02:00
Daniel Cason
444ed8c679 PBTS: using proper Markdown subscripts in spec 2022-05-12 16:54:04 +02:00
Daniel Cason
858358aa8d PBTS: reference to v1 removed from algorithmic spec 2022-05-12 16:47:20 +02:00
Kukovec
cd48156f66 formatting 2022-05-06 15:10:33 +02:00
Kukovec
026f378e50 run script/docs 2022-05-06 15:07:20 +02:00
Kukovec
1b7aabcc39 move + rename 2022-05-06 11:31:49 +02:00
92 changed files with 1568903 additions and 459 deletions

View File

@@ -4,10 +4,8 @@ package mocks
import (
context "context"
testing "testing"
mock "github.com/stretchr/testify/mock"
types "github.com/tendermint/tendermint/abci/types"
)
@@ -422,8 +420,13 @@ func (_m *Client) Wait() {
_m.Called()
}
// NewClient creates a new instance of Client. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewClient(t testing.TB) *Client {
type NewClientT interface {
mock.TestingT
Cleanup(func())
}
// NewClient creates a new instance of Client. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewClient(t NewClientT) *Client {
mock := &Client{}
mock.Mock.Test(t)

View File

@@ -4,10 +4,8 @@ package mocks
import (
context "context"
testing "testing"
mock "github.com/stretchr/testify/mock"
types "github.com/tendermint/tendermint/abci/types"
)
@@ -338,8 +336,13 @@ func (_m *Application) VerifyVoteExtension(_a0 context.Context, _a1 *types.Reque
return r0, r1
}
// NewApplication creates a new instance of Application. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewApplication(t testing.TB) *Application {
type NewApplicationT interface {
mock.TestingT
Cleanup(func())
}
// NewApplication creates a new instance of Application. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewApplication(t NewApplicationT) *Application {
mock := &Application{}
mock.Mock.Test(t)

View File

@@ -3,8 +3,6 @@
package mocks
import (
testing "testing"
mock "github.com/stretchr/testify/mock"
state "github.com/tendermint/tendermint/internal/state"
)
@@ -29,8 +27,13 @@ func (_m *ConsSyncReactor) SwitchToConsensus(_a0 state.State, _a1 bool) {
_m.Called(_a0, _a1)
}
// NewConsSyncReactor creates a new instance of ConsSyncReactor. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewConsSyncReactor(t testing.TB) *ConsSyncReactor {
type NewConsSyncReactorT interface {
mock.TestingT
Cleanup(func())
}
// NewConsSyncReactor creates a new instance of ConsSyncReactor. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewConsSyncReactor(t NewConsSyncReactorT) *ConsSyncReactor {
mock := &ConsSyncReactor{}
mock.Mock.Test(t)

View File

@@ -3,10 +3,7 @@
package mocks
import (
testing "testing"
mock "github.com/stretchr/testify/mock"
types "github.com/tendermint/tendermint/types"
)
@@ -61,8 +58,13 @@ func (_m *BlockStore) LoadBlockMeta(height int64) *types.BlockMeta {
return r0
}
// NewBlockStore creates a new instance of BlockStore. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewBlockStore(t testing.TB) *BlockStore {
type NewBlockStoreT interface {
mock.TestingT
Cleanup(func())
}
// NewBlockStore creates a new instance of BlockStore. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewBlockStore(t NewBlockStoreT) *BlockStore {
mock := &BlockStore{}
mock.Mock.Test(t)

View File

@@ -11,8 +11,6 @@ import (
mock "github.com/stretchr/testify/mock"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -173,8 +171,13 @@ func (_m *Mempool) Update(ctx context.Context, blockHeight int64, blockTxs types
return r0
}
// NewMempool creates a new instance of Mempool. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewMempool(t testing.TB) *Mempool {
type NewMempoolT interface {
mock.TestingT
Cleanup(func())
}
// NewMempool creates a new instance of Mempool. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewMempool(t NewMempoolT) *Mempool {
mock := &Mempool{}
mock.Mock.Test(t)

View File

@@ -13,8 +13,6 @@ import (
p2p "github.com/tendermint/tendermint/internal/p2p"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -153,8 +151,13 @@ func (_m *Connection) String() string {
return r0
}
// NewConnection creates a new instance of Connection. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewConnection(t testing.TB) *Connection {
type NewConnectionT interface {
mock.TestingT
Cleanup(func())
}
// NewConnection creates a new instance of Connection. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewConnection(t NewConnectionT) *Connection {
mock := &Connection{}
mock.Mock.Test(t)

View File

@@ -10,8 +10,6 @@ import (
mock "github.com/stretchr/testify/mock"
p2p "github.com/tendermint/tendermint/internal/p2p"
testing "testing"
)
// Transport is an autogenerated mock type for the Transport type
@@ -151,8 +149,13 @@ func (_m *Transport) String() string {
return r0
}
// NewTransport creates a new instance of Transport. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewTransport(t testing.TB) *Transport {
type NewTransportT interface {
mock.TestingT
Cleanup(func())
}
// NewTransport creates a new instance of Transport. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewTransport(t NewTransportT) *Transport {
mock := &Transport{}
mock.Mock.Test(t)

View File

@@ -12,8 +12,6 @@ import (
tenderminttypes "github.com/tendermint/tendermint/types"
testing "testing"
types "github.com/tendermint/tendermint/abci/types"
)
@@ -168,8 +166,13 @@ func (_m *EventSink) Type() indexer.EventSinkType {
return r0
}
// NewEventSink creates a new instance of EventSink. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewEventSink(t testing.TB) *EventSink {
type NewEventSinkT interface {
mock.TestingT
Cleanup(func())
}
// NewEventSink creates a new instance of EventSink. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewEventSink(t NewEventSinkT) *EventSink {
mock := &EventSink{}
mock.Mock.Test(t)

View File

@@ -5,8 +5,6 @@ package mocks
import (
mock "github.com/stretchr/testify/mock"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -232,8 +230,13 @@ func (_m *BlockStore) Size() int64 {
return r0
}
// NewBlockStore creates a new instance of BlockStore. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewBlockStore(t testing.TB) *BlockStore {
type NewBlockStoreT interface {
mock.TestingT
Cleanup(func())
}
// NewBlockStore creates a new instance of BlockStore. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewBlockStore(t NewBlockStoreT) *BlockStore {
mock := &BlockStore{}
mock.Mock.Test(t)

View File

@@ -8,8 +8,6 @@ import (
mock "github.com/stretchr/testify/mock"
state "github.com/tendermint/tendermint/internal/state"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -74,8 +72,13 @@ func (_m *EvidencePool) Update(_a0 context.Context, _a1 state.State, _a2 types.E
_m.Called(_a0, _a1, _a2)
}
// NewEvidencePool creates a new instance of EvidencePool. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewEvidencePool(t testing.TB) *EvidencePool {
type NewEvidencePoolT interface {
mock.TestingT
Cleanup(func())
}
// NewEvidencePool creates a new instance of EvidencePool. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewEvidencePool(t NewEvidencePoolT) *EvidencePool {
mock := &EvidencePool{}
mock.Mock.Test(t)

View File

@@ -7,8 +7,6 @@ import (
state "github.com/tendermint/tendermint/internal/state"
tendermintstate "github.com/tendermint/tendermint/proto/tendermint/state"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -189,8 +187,13 @@ func (_m *Store) SaveValidatorSets(_a0 int64, _a1 int64, _a2 *types.ValidatorSet
return r0
}
// NewStore creates a new instance of Store. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewStore(t testing.TB) *Store {
type NewStoreT interface {
mock.TestingT
Cleanup(func())
}
// NewStore creates a new instance of Store. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewStore(t NewStoreT) *Store {
mock := &Store{}
mock.Mock.Test(t)

View File

@@ -8,8 +8,6 @@ import (
mock "github.com/stretchr/testify/mock"
state "github.com/tendermint/tendermint/internal/state"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -85,8 +83,13 @@ func (_m *StateProvider) State(ctx context.Context, height uint64) (state.State,
return r0, r1
}
// NewStateProvider creates a new instance of StateProvider. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewStateProvider(t testing.TB) *StateProvider {
type NewStateProviderT interface {
mock.TestingT
Cleanup(func())
}
// NewStateProvider creates a new instance of StateProvider. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewStateProvider(t NewStateProviderT) *StateProvider {
mock := &StateProvider{}
mock.Mock.Test(t)

View File

@@ -3,11 +3,9 @@
package mocks
import (
testing "testing"
time "time"
mock "github.com/stretchr/testify/mock"
time "time"
)
// Source is an autogenerated mock type for the Source type
@@ -29,8 +27,13 @@ func (_m *Source) Now() time.Time {
return r0
}
// NewSource creates a new instance of Source. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewSource(t testing.TB) *Source {
type NewSourceT interface {
mock.TestingT
Cleanup(func())
}
// NewSource creates a new instance of Source. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewSource(t NewSourceT) *Source {
mock := &Source{}
mock.Mock.Test(t)

View File

@@ -7,8 +7,6 @@ import (
mock "github.com/stretchr/testify/mock"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -68,8 +66,13 @@ func (_m *Provider) ReportEvidence(_a0 context.Context, _a1 types.Evidence) erro
return r0
}
// NewProvider creates a new instance of Provider. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewProvider(t testing.TB) *Provider {
type NewProviderT interface {
mock.TestingT
Cleanup(func())
}
// NewProvider creates a new instance of Provider. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewProvider(t NewProviderT) *Provider {
mock := &Provider{}
mock.Mock.Test(t)

View File

@@ -7,8 +7,6 @@ import (
mock "github.com/stretchr/testify/mock"
testing "testing"
time "time"
types "github.com/tendermint/tendermint/types"
@@ -118,8 +116,13 @@ func (_m *LightClient) VerifyLightBlockAtHeight(ctx context.Context, height int6
return r0, r1
}
// NewLightClient creates a new instance of LightClient. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewLightClient(t testing.TB) *LightClient {
type NewLightClientT interface {
mock.TestingT
Cleanup(func())
}
// NewLightClient creates a new instance of LightClient. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewLightClient(t NewLightClientT) *LightClient {
mock := &LightClient{}
mock.Mock.Test(t)

View File

@@ -12,8 +12,6 @@ import (
mock "github.com/stretchr/testify/mock"
testing "testing"
types "github.com/tendermint/tendermint/types"
)
@@ -798,8 +796,13 @@ func (_m *Client) Validators(ctx context.Context, height *int64, page *int, perP
return r0, r1
}
// NewClient creates a new instance of Client. It also registers the testing.TB interface on the mock and a cleanup function to assert the mocks expectations.
func NewClient(t testing.TB) *Client {
type NewClientT interface {
mock.TestingT
Cleanup(func())
}
// NewClient creates a new instance of Client. It also registers a testing interface on the mock and a cleanup function to assert the mocks expectations.
func NewClient(t NewClientT) *Client {
mock := &Client{}
mock.Mock.Test(t)

View File

@@ -122,19 +122,8 @@ The full solution is detailed and formalized in the [Protocol Specification][alg
- [System Model and Properties][sysmodel]
- [Protocol Specification][algorithm]
- [TLA+ Specification][proposertla] (first draft, not updated)
### Open issues
- [PBTS: evidence #355][issue355]: not really clear the context, probably not going to be solved.
- [PBTS: should synchrony parameters be adaptive? #371][issue371]
- [PBTS: Treat proposal and block parts explicitly in the spec #372][issue372]
- [PBTS: margins for proposal times assigned by Byzantine proposers #377][issue377]
### Closed issues
- [Proposer time - fix message filter condition #353][issue353]
- [PBTS: association between timely predicate and timeout_commit #370][issue370]
- [TLA+ Specification][proposertla]
- [Project on Github][project] (collection of PBTS-related issues)
[main_v1]: ./v1/pbts_001_draft.md
@@ -144,14 +133,9 @@ The full solution is detailed and formalized in the [Protocol Specification][alg
[sysmodel]: ./pbts-sysmodel_002_draft.md
[sysmodel_v1]: ./v1/pbts-sysmodel_001_draft.md
[proposertla]: ./tla/TendermintPBT_001_draft.tla
[proposertla]: ./tla/TendermintPBT.tla
[bfttime]: https://github.com/tendermint/tendermint/blob/master/spec/consensus/bft-time.md
[bfttime]: ./bft-time.md
[arXiv]: https://arxiv.org/pdf/1807.04938.pdf
[issue353]: https://github.com/tendermint/spec/issues/353
[issue355]: https://github.com/tendermint/spec/issues/355
[issue370]: https://github.com/tendermint/spec/issues/370
[issue371]: https://github.com/tendermint/spec/issues/371
[issue372]: https://github.com/tendermint/spec/issues/372
[issue377]: https://github.com/tendermint/spec/issues/377
[project]: https://github.com/orgs/tendermint/projects/10

View File

@@ -1,8 +1,7 @@
---
order: 2
---
# BFT Time
> BFTTime was removed from Tendermint consensus from v0.36, being replaced by [PBTS](./README.md).
Tendermint provides a deterministic, Byzantine fault-tolerant, source of time.
Time in Tendermint is defined with the Time field of the block header.

View File

@@ -16,30 +16,22 @@ When a value `v` is produced by a process, it also assigns the associated propos
If the same value `v` is then re-proposed in a subsequent round of consensus,
it retains its original time, assigned by its original proposer.
A value `v` should re-proposed when it becomes locked by the network, i.e., when it receives `2f + 1 PREVOTES` in a round `r` of consensus.
A value `v` is re-proposed when it becomes a valid value, i.e., when it receives `2f + 1 PREVOTE`s in a round `r` of consensus.
This means that processes with `2f + 1`-equivalent voting power accepted, in round `r`, both `v` and its associated time `v.time`.
Since the originally proposed value and its associated time were considered valid, there is no reason for reassigning `v.time`.
In the [first version][algorithm_v1] of this specification, proposals were defined as pairs `(v, time)`.
In addition, the same value `v` could be proposed, in different rounds, but would be associated to distinct times each time it was reproposed.
Since this possibility does not exist in this second specification, the proposal time became part of the proposed value.
With this simplification, several small changes to the [arXiv][arXiv] algorithm are no longer required.
## Time Monotonicity
Values decided in successive heights of consensus must have increasing times, so:
- Monotonicity: for any process `p` and any two decided heights `h` and `h'`, if `h > h'` then `decision_p[h].time > decision_p[h'].time`.
- Monotonicity: for any process `p` and any two decided heights `h` and `h'`, if `h > h'` then <code>decision<sub>p</sub>[h].time > decision<sub>p</sub>[h'].time</code>.
For ensuring time monotonicity, it is enough to ensure that a value `v` proposed by process `p` at height `h_p` has `v.time > decision_p[h_p-1].time`.
So, if process `p` is the proposer of a round of height `h_p` and reads from its clock a time `now_p <= decision_p[h_p-1]`,
it should postpone the generation of its proposal until `now_p > decision_p[h_p-1]`.
For ensuring time monotonicity, it is enough to ensure that a value `v` proposed by process `p` at height <code>h<sub>p</sub></code> has <code>v.time > decision<sub>p</sub>[h<sub>p</sub>-1].time</code>.
So, if process `p` is the proposer of a round of height <code>h<sub>p</sub></code> and reads from its clock a time <code>now<sub>p</sub> <= decision<sub>p</sub>[h<sub>p</sub>-1]</code>,
it should postpone the generation of its proposal until <code>now<sub>p</sub> > decision<sub>p</sub>[h<sub>p</sub>-1]</code>.
> Although it should be considered, this scenario is unlikely during regular operation,
as from `decision_p[h_p-1].time` and the start of height `h_p`, a complete consensus instance need to terminate.
Notice that monotonicity is not introduced by this proposal, being already ensured by [`BFTTime`][bfttime].
In `BFTTime`, the `Timestamp` field of every `Precommit` message of height `h_p` sent by a correct process is required to be larger than `decision_p[h_p-1].time`, as one of such `Timestamp` fields becomes the time assigned to a value proposed at height `h_p`.
as from <code>decision<sub>p</sub>[h<sub>p</sub>-1].time</code> and the start of height <code>h<sub>p</sub></code>, a complete consensus instance need to terminate.
The time monotonicity of values proposed in heights of consensus is verified by the `valid()` predicate, to which every proposed value is submitted.
A value rejected by the `valid()` implementation is not accepted by any correct process.
@@ -55,33 +47,31 @@ It is a temporal requirement, associated with the following synchrony (that is,
#### **[PBTS-RECEPTION-STEP.1]**
Let `now_p` be the time, read from the clock of process `p`, at which `p` receives the proposed value `v`.
Let <code>now<sub>p</sub></code> be the time, read from the clock of process `p`, at which `p` receives the proposed value `v`.
The proposal is considered `timely` by `p` when:
1. `now_p >= v.time - PRECISION`
1. `now_p <= v.time + MSGDELAY + PRECISION`
1. <code>now<sub>p</sub> >= v.time - PRECISION</code>
1. <code>now<sub>p</sub> <= v.time + MSGDELAY + PRECISION</code>
The first condition derives from the fact that the generation and sending of `v` precedes its reception.
The minimum receiving time `now_p` for `v` be considered `timely` by `p` is derived from the extreme scenario when
The minimum receiving time <code>now<sub>p</sub></code> for `v` be considered `timely` by `p` is derived from the extreme scenario when
the clock of `p` is `PRECISION` *behind* of the clock of the proposer of `v`, and the proposal's transmission delay is `0` (minimum).
The second condition derives from the assumption of an upper bound for the transmission delay of a proposal.
The maximum receiving time `now_p` for `v` be considered `timely` by `p` is derived from the extreme scenario when
The maximum receiving time <code>now<sub>p</sub></code> for `v` be considered `timely` by `p` is derived from the extreme scenario when
the clock of `p` is `PRECISION` *ahead* of the clock of the proposer of `v`, and the proposal's transmission delay is `MSGDELAY` (maximum).
## Updated Consensus Algorithm
The following changes are proposed for the algorithm in the [arXiv paper][arXiv].
#### New `StartRound`
#### New `StartRound` (Lines 11 - 21)
There are two additions to the `propose` round step when executed by the `proposer` of a round:
1. to ensure time monotonicity, the proposer does not propose a value until its current local time becomes greater than the previously decided value's time
1. when the proposer produce a new proposal it sets the proposal's time to its current local time
- no changes are made to the logic when a proposer has a non-nil `validValue`, which retains its original proposal time.
#### **[PBTS-ALG-STARTROUND.1]**
1. The proposer does not propose a value until its current local time becomes greater than the previously decided value's time;
1. When the proposer produces a new proposal, it sets the proposal's time to its current local time;
- No changes are made to the logic when a proposer re-proposes its `validValue`, which retains its original proposal time.
```go
function StartRound(round) {
@@ -102,20 +92,18 @@ function StartRound(round) {
}
```
#### New Rule Replacing Lines 22 - 27
#### New rule for accepting values (Lines 22 - 27)
The rule on line 22 applies to values `v` proposed for the first time, i.e., for proposals not backed by `2f + 1 PREVOTE`s for `v` in a previous round.
The rule on line 22 applies to values `v` proposed for the first time, i.e., for proposals not backed by `PREVOTE`s for `v` in a previous round `vr < r`.
The `PROPOSAL` message, in this case, carry `-1` in its `validRound` field.
The new rule for issuing a `PREVOTE` for a proposed value `v` requires the value to be `timely`.
As the `timely` predicate is evaluated in the moment that the value is received,
as part of a `PROPOSAL` message, we require the `PROPOSAL` message to be `timely`.
#### **[PBTS-ALG-UPON-PROP.1]**
The `timely` predicate is evaluated in the moment that the value is received,
as part of a `PROPOSAL` message, by comparing the process local time with `v.time`.
```go
upon timely(PROPOSAL, h_p, round_p, v, 1) from proposer(h_p, round_p) while step_p = propose do {
if valid(v) (lockedRound_p = 1 lockedValue_p = v) {
upon PROPOSAL, h_p, round_p, v, 1 from proposer(h_p, round_p) while step_p = propose do {
if timely(v.time) valid(v) (lockedRound_p = 1 lockedValue_p = v) {
broadcast PREVOTE, h_p, round_p, id(v)
}
else {
@@ -125,24 +113,15 @@ upon timely(⟨PROPOSAL, h_p, round_p, v, 1⟩) from proposer(h_p, round_p) w
}
```
#### Rules at Lines 28 - 33 remain unchanged
#### All other rules remains unchanged
The rule on line 28 applies to values `v` proposed again in the current round because its proposer received `2f + 1 PREVOTE`s for `v` in a previous round `vr`.
This means that there was a round `r <= vr` in which `2f + 1` processes accepted `v` for the first time, and so sent `PREVOTE`s for `v`.
Which, in turn, means that these processes executed the line 22 of the algorithm, and therefore judged `v` as a `timely` proposal.
In other words, we don't need to verify whether `v` is a timely proposal because at least `f + 1` processes judged `v` as `timely` in a previous round,
and because, since `v` was re-proposed as a `validValue` (line 16), `v.time` has not being updated from its original proposal.
**All other rules remains unchanged.**
Notice, in particular, that the rule on line 28 for values re-proposed, and backed by `2f + 1`-equivalent voting power `PREVOTE` messages, is not affected by the changes.
Back to [main document][main].
[main]: ./README.md
[algorithm_v1]: ./v1/pbts-algorithm_001_draft.md
[sysmodel]: ./pbts-sysmodel_002_draft.md
[bfttime]: https://github.com/tendermint/tendermint/blob/master/spec/consensus/bft-time.md
[bfttime]: ./bft-time.md
[arXiv]: https://arxiv.org/pdf/1807.04938.pdf

View File

@@ -42,10 +42,10 @@ and drifts of local clocks from real time.
#### **[PBTS-CLOCK-PRECISION.0]**
There exists a system parameter `PRECISION`, such that
for any two processes `p` and `q`, with local clocks `C_p` and `C_q`:
for any two processes `p` and `q`, with local clocks <code>C<sub>p</sub></code> and <code>C<sub>q</sub></code>:
- If `p` and `q` are equipped with synchronized clocks,
then for any real-time `t` we have `|C_p(t) - C_q(t)| <= PRECISION`.
then for any real-time `t` we have <code>|C<sub>p</sub>(t) - C<sub>q</sub>(t)| <= PRECISION</code>.
`PRECISION` thus bounds the difference on the times simultaneously read by processes
from their local clocks, so that their clocks can be considered synchronized.
@@ -60,12 +60,12 @@ processes from their clocks to real time.
For the sake of completeness, we define a parameter `ACCURACY` such that:
- At real time `t` there is at least one correct process `p` which clock marks
`C_p(t)` with `|C_p(t) - t| <= ACCURACY`.
<code>C<sub>p</sub>(t)</code> with <code>|C<sub>p</sub>(t) - t| <= ACCURACY</code>.
As a consequence, applying the definition of `PRECISION`, we have:
- At real time `t` the synchronized clock of any correct process `p` marks
`C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION`.
<code>C<sub>p</sub>(t)</code> with <code>|C<sub>p</sub>(t) - t| <= ACCURACY + PRECISION</code>.
The reason for not adopting `ACCURACY` as a system parameter is the assumption
that `PRECISION >> ACCURACY`.
@@ -163,7 +163,7 @@ 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`.
> <code>round<sub>p</sub></code> when starting its proposing round with a nil <code>validValue<sub>p</sub></code>.
> 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`.
@@ -190,7 +190,7 @@ associated proposal time `v.time` is considered `timely`.
> Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate
> is evaluated by a process `p` when it receives a valid `PROPOSAL` message
> from the proposer of the current round `round_p` with `vr = -1`.
> from the proposer of the current round <code>round<sub>p</sub></code> with `vr = -1`.
### Timely Proof-of-Locks
@@ -259,7 +259,7 @@ produced (by hypothesis) we can affirm 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
> the proposer `p` of round <code>round<sub>p</sub></code> because its <code>validValue<sub>p</sub></code> variable was
> set to `v`.
> The `PROPOSAL` message broadcast by the proposer, in this case, had `vr > -1`,
> and it could only be accepted by processes that also observed a `POL(v,vr)`.

View File

@@ -1,109 +0,0 @@
--------------------------- MODULE Apalache -----------------------------------
(*
* This is a standard module for use with the Apalache model checker.
* The meaning of the operators is explained in the comments.
* Many of the operators serve as additional annotations of their arguments.
* As we like to preserve compatibility with TLC and TLAPS, we define the
* operator bodies by erasure. The actual interpretation of the operators is
* encoded inside Apalache. For the moment, these operators are mirrored in
* the class at.forsyte.apalache.tla.lir.oper.ApalacheOper.
*
* Igor Konnov, Jure Kukovec, Informal Systems 2020-2021
*)
(**
* An assignment of an expression e to a state variable x. Typically, one
* uses the non-primed version of x in the initializing predicate Init and
* the primed version of x (that is, x') in the transition predicate Next.
* Although TLA+ does not have a concept of a variable assignment, we find
* this concept extremely useful for symbolic model checking. In pure TLA+,
* one would simply write x = e, or x \in {e}.
*
* Apalache automatically converts some expressions of the form
* x = e or x \in {e} into assignments. However, if you like to annotate
* assignments by hand, you can use this operator.
*
* For a further discussion on that matter, see:
* https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md
*)
x := e == x = e
(**
* A generator of a data structure. Given a positive integer `bound`, and
* assuming that the type of the operator application is known, we
* recursively generate a TLA+ data structure as a tree, whose width is
* bound by the number `bound`.
*
* The body of this operator is redefined by Apalache.
*)
Gen(size) == {}
(**
* Convert a set of pairs S to a function F. Note that if S contains at least
* two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,
* then F is not uniquely defined. We use CHOOSE to resolve this ambiguity.
* Apalache implements a more efficient encoding of this operator
* than the default one.
*
* @type: Set(<<a, b>>) => (a -> b);
*)
SetAsFun(S) ==
LET Dom == { x: <<x, y>> \in S }
Rng == { y: <<x, y>> \in S }
IN
[ x \in Dom |-> CHOOSE y \in Rng: <<x, y>> \in S ]
(**
* As TLA+ is untyped, one can use function- and sequence-specific operators
* interchangeably. However, to maintain correctness w.r.t. our type-system,
* an explicit cast is needed when using functions as sequences.
*)
LOCAL INSTANCE Sequences
FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)
(**
* Annotating an expression \E x \in S: P as Skolemizable. That is, it can
* be replaced with an expression c \in S /\ P(c) for a fresh constant c.
* Not every exisential can be replaced with a constant, this should be done
* with care. Apalache detects Skolemizable expressions by static analysis.
*)
Skolem(e) == e
(**
* A hint to the model checker to expand a set S, instead of dealing
* with it symbolically. Apalache finds out which sets have to be expanded
* by static analysis.
*)
Expand(S) == S
(**
* A hint to the model checker to replace its argument Cardinality(S) >= k
* with a series of existential quantifiers for a constant k.
* Similar to Skolem, this has to be done carefully. Apalache automatically
* places this hint by static analysis.
*)
ConstCardinality(cardExpr) == cardExpr
(**
* The folding operator, used to implement computation over a set.
* Apalache implements a more efficient encoding than the one below.
* (from the community modules).
*)
RECURSIVE FoldSet(_,_,_)
FoldSet( Op(_,_), v, S ) == IF S = {}
THEN v
ELSE LET w == CHOOSE x \in S: TRUE
IN LET T == S \ {w}
IN FoldSet( Op, Op(v,w), T )
(**
* The folding operator, used to implement computation over a sequence.
* Apalache implements a more efficient encoding than the one below.
* (from the community modules).
*)
RECURSIVE FoldSeq(_,_,_)
FoldSeq( Op(_,_), v, seq ) == IF seq = <<>>
THEN v
ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) )
===============================================================================

View File

@@ -1,4 +1,4 @@
----------------------------- MODULE MC_PBT -------------------------------
----------------------------- MODULE MC_PBT_2C_2F -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
@@ -38,40 +38,31 @@ VARIABLES
evidence, \* the messages that were used by the correct processes to make transitions
\* @type: ACTION;
action, \* we use this variable to see which action was taken
\* @type: PROCESS -> Set(PROPMESSAGE);
receivedTimelyProposal, \* used to keep track when a process receives a timely VALUE message
\* @type: <<ROUND,PROCESS>> -> TIME;
inspectedProposal \* used to keep track when a process tries to receive a message
proposalReceptionTime \* used to keep track when a process receives a message
\* Invariant support
VARIABLES
\* @type: ROUND -> TIME;
beginRound, \* the minimum of the local clocks at the time any process entered a new round
\* @type: PROCESS -> TIME;
endConsensus, \* the local time when a decision is made
\* @type: ROUND -> TIME;
lastBeginRound, \* the maximum of the local clocks in each round
\* @type: ROUND -> TIME;
proposalTime, \* the real time when a proposer proposes in a round
\* @type: ROUND -> TIME;
proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
\* @type: <<ROUND, PROCESS>> -> TIME;
beginRound \* the minimum of the local clocks at the time any process entered a new round
INSTANCE TendermintPBT_002_draft WITH
INSTANCE TendermintPBT WITH
Corr <- {"c1", "c2"},
Faulty <- {"f3", "f4"},
N <- 4,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 5,
MaxTimestamp <- 10,
MaxRound <- 3,
MaxTimestamp <- 7,
MinTimestamp <- 2,
Delay <- 2,
Precision <- 2
Precision <- 2,
PreloadAllFaultyMsgs <- TRUE,
N_GEN <- 5
\* run Apalache with --cinit=CInit
CInit == \* the proposer is arbitrary -- works for safety
Proposer \in [Rounds -> AllProcs]
ArbitraryProposer
=============================================================================

View File

@@ -0,0 +1,68 @@
----------------------------- MODULE MC_PBT_3C_1F -------------------------------
CONSTANT
\* @type: ROUND -> PROCESS;
Proposer
VARIABLES
\* @type: PROCESS -> ROUND;
round, \* a process round number
\* @type: PROCESS -> STEP;
step, \* a process step
\* @type: PROCESS -> DECISION;
decision, \* process decision
\* @type: PROCESS -> VALUE;
lockedValue, \* a locked value
\* @type: PROCESS -> ROUND;
lockedRound, \* a locked round
\* @type: PROCESS -> PROPOSAL;
validValue, \* a valid value
\* @type: PROCESS -> ROUND;
validRound \* a valid round
\* time-related variables
VARIABLES
\* @type: PROCESS -> TIME;
localClock, \* a process local clock: Corr -> Ticks
\* @type: TIME;
realTime \* a reference Newtonian real time
\* book-keeping variables
VARIABLES
\* @type: ROUND -> Set(PROPMESSAGE);
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
\* @type: ROUND -> Set(PREMESSAGE);
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
\* @type: Set(MESSAGE);
evidence, \* the messages that were used by the correct processes to make transitions
\* @type: ACTION;
action, \* we use this variable to see which action was taken
\* @type: <<ROUND,PROCESS>> -> TIME;
proposalReceptionTime \* used to keep track when a process receives a message
\* Invariant support
VARIABLES
\* @type: <<ROUND, PROCESS>> -> TIME;
beginRound \* the minimum of the local clocks at the time any process entered a new round
INSTANCE TendermintPBT WITH
Corr <- {"c1", "c2", "c3"},
Faulty <- {"f4"},
N <- 4,
T <- 1,
ValidValues <- { "v0", "v1" },
InvalidValues <- {"v2"},
MaxRound <- 3,
MaxTimestamp <- 7,
MinTimestamp <- 2,
Delay <- 2,
Precision <- 2,
PreloadAllFaultyMsgs <- TRUE,
N_GEN <- 5
\* run Apalache with --cinit=CInit
CInit == \* the proposer is arbitrary -- works for safety
ArbitraryProposer
=============================================================================

View File

@@ -1,4 +1,4 @@
-------------------- MODULE TendermintPBT_002_draft ---------------------------
-------------------- MODULE TendermintPBT ---------------------------
(*
A TLA+ specification of a simplified Tendermint consensus, with added clocks
and proposer-based timestamps. This TLA+ specification extends and modifies
@@ -12,7 +12,7 @@
Jure Kukovec, Informal Systems, 2022.
*)
EXTENDS Integers, FiniteSets, Apalache, typedefs
EXTENDS Integers, FiniteSets, Apalache, Sequences, typedefs
(********************* PROTOCOL PARAMETERS **********************************)
\* General protocol parameters
@@ -47,6 +47,13 @@ CONSTANTS
ASSUME(N = Cardinality(Corr \union Faulty))
\* Modeling parameter
CONSTANTS
\* @type: Bool;
PreloadAllFaultyMsgs,
\* @type: Int;
N_GEN
(*************************** DEFINITIONS ************************************)
\* @type: Set(PROCESS);
AllProcs == Corr \union Faulty \* the set of all processes
@@ -75,6 +82,14 @@ Decisions == Proposals \X Rounds
\* @type: DECISION;
NilDecision == <<NilProposal, NilRound>>
ArbitraryProposer == Proposer \in [Rounds -> AllProcs]
CorrectProposer == Proposer \in [Rounds -> Corr]
CyclicalProposer ==
LET ProcOrder ==
LET App(s,e) == Append(s,e)
IN ApaFoldSet(App, <<>>, AllProcs)
IN Proposer = [ r \in Rounds |-> ProcOrder[1 + (r % N)] ]
ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
\* a value hash is modeled as identity
\* @type: (t) => t;
@@ -108,13 +123,13 @@ THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
\* @type: (TIME, TIME) => TIME;
Min2(a,b) == IF a <= b THEN a ELSE b
\* @type: (Set(TIME)) => TIME;
Min(S) == FoldSet( Min2, MaxTimestamp, S )
Min(S) == ApaFoldSet( Min2, MaxTimestamp, S )
\* Min(S) == CHOOSE x \in S : \A y \in S : x <= y
\* @type: (TIME, TIME) => TIME;
Max2(a,b) == IF a >= b THEN a ELSE b
\* @type: (Set(TIME)) => TIME;
Max(S) == FoldSet( Max2, NilTimestamp, S )
Max(S) == ApaFoldSet( Max2, NilTimestamp, S )
\* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
\* @type: (Set(MESSAGE)) => Int;
@@ -122,7 +137,7 @@ Card(S) ==
LET
\* @type: (Int, MESSAGE) => Int;
PlusOne(i, m) == i + 1
IN FoldSet( PlusOne, 0, S )
IN ApaFoldSet( PlusOne, 0, S )
(********************* PROTOCOL STATE VARIABLES ******************************)
VARIABLES
@@ -166,33 +181,18 @@ VARIABLES
evidence, \* the messages that were used by the correct processes to make transitions
\* @type: ACTION;
action, \* we use this variable to see which action was taken
\* @type: PROCESS -> Set(PROPMESSAGE);
receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message
\* @type: <<ROUND,PROCESS>> -> TIME;
inspectedProposal \* used to keep track when a process tries to receive a message
proposalReceptionTime \* used to keep track when a process receives a message
\* Action is excluded from the tuple, because it always changes
bookkeepingVars ==
<<msgsPropose, msgsPrevote, msgsPrecommit,
evidence, (*action,*) receivedTimelyProposal,
inspectedProposal>>
evidence, (*action,*) proposalReceptionTime>>
\* Invariant support
VARIABLES
\* @type: ROUND -> TIME;
beginRound, \* the minimum of the local clocks at the time any process entered a new round
\* @type: PROCESS -> TIME;
endConsensus, \* the local time when a decision is made
\* @type: ROUND -> TIME;
lastBeginRound, \* the maximum of the local clocks in each round
\* @type: ROUND -> TIME;
proposalTime, \* the real time when a proposer proposes in a round
\* @type: ROUND -> TIME;
proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
invariantVars ==
<<beginRound, endConsensus, lastBeginRound,
proposalTime, proposalReceivedTime>>
\* @type: <<ROUND, PROCESS>> -> TIME;
beginRound \* the minimum of the local clocks at the time any process entered a new round
(* to see a type invariant, check TendermintAccInv3 *)
@@ -280,6 +280,39 @@ BenignRoundsInMessages(msgfun) ==
\A m \in msgfun[r]:
r = m.round
\* @type: (ROUND -> Set(MESSAGE), Set(MESSAGE)) => Bool;
BenignAndSubset(msgfun, set) ==
/\ \A r \in Rounds:
\* The generated values belong to SUBSET set
/\ msgfun[r] \subseteq set
\* the message function never contains a message for a wrong round
/\ \A m \in msgfun[r]: r = m.round
InitGen ==
/\ msgsPropose \in [Rounds -> Gen(N_GEN)]
/\ msgsPrevote \in [Rounds -> Gen(N_GEN)]
/\ msgsPrecommit \in [Rounds -> Gen(N_GEN)]
/\ BenignAndSubset(msgsPropose, AllFaultyProposals)
/\ BenignAndSubset(msgsPrevote, AllFaultyPrevotes)
/\ BenignAndSubset(msgsPrecommit, AllFaultyPrecommits)
InitPreloadAllMsgs ==
/\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
/\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
/\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
/\ BenignRoundsInMessages(msgsPropose)
/\ BenignRoundsInMessages(msgsPrevote)
/\ BenignRoundsInMessages(msgsPrecommit)
InitMsgs ==
\/ /\ PreloadAllFaultyMsgs
\* /\ InitPreloadAllMsgs
/\ InitGen
\/ /\ ~PreloadAllFaultyMsgs
/\ msgsPropose = [r \in Rounds |-> {}]
/\ msgsPrevote = [r \in Rounds |-> {}]
/\ msgsPrecommit = [r \in Rounds |-> {}]
\* The initial states of the protocol. Some faults can be in the system already.
Init ==
/\ round = [p \in Corr |-> 0]
@@ -291,31 +324,48 @@ Init ==
/\ lockedRound = [p \in Corr |-> NilRound]
/\ validValue = [p \in Corr |-> NilProposal]
/\ validRound = [p \in Corr |-> NilRound]
/\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
/\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
/\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
/\ receivedTimelyProposal = [p \in Corr |-> {}]
/\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp]
/\ BenignRoundsInMessages(msgsPropose)
/\ BenignRoundsInMessages(msgsPrevote)
/\ BenignRoundsInMessages(msgsPrecommit)
/\ InitMsgs
/\ proposalReceptionTime = [r \in Rounds, p \in Corr |-> NilTimestamp]
/\ evidence = {}
/\ action' = "Init"
/\ action = "Init"
/\ beginRound =
[r \in Rounds |->
[r \in Rounds, c \in Corr |->
IF r = 0
THEN Min({localClock[p] : p \in Corr})
THEN localClock[c]
ELSE MaxTimestamp
]
/\ endConsensus = [p \in Corr |-> NilTimestamp]
/\ lastBeginRound =
[r \in Rounds |->
IF r = 0
THEN Max({localClock[p] : p \in Corr})
ELSE NilTimestamp
]
/\ proposalTime = [r \in Rounds |-> NilTimestamp]
/\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
lastBeginRound == [ r \in Rounds |->
Max({beginRound[r,p] : p \in Corr})
]
firstBeginRound == [ r \in Rounds |->
Min({beginRound[r,p] : p \in Corr})
]
\* Faulty processes send messages
FaultyBroadcast ==
/\ ~PreloadAllFaultyMsgs
/\ action' = "FaultyBroadcast"
/\ \E r \in Rounds:
\/ \E msgs \in SUBSET FaultyProposals(r):
/\ msgsPropose' = [msgsPropose EXCEPT ![r] = @ \union msgs]
/\ UNCHANGED <<coreVars, temporalVars, beginRound>>
/\ UNCHANGED
<<(*msgsPropose,*) msgsPrevote, msgsPrecommit,
evidence, (*action,*) proposalReceptionTime>>
\/ \E msgs \in SUBSET FaultyPrevotes(r):
/\ msgsPrevote' = [msgsPrevote EXCEPT ![r] = @ \union msgs]
/\ UNCHANGED <<coreVars, temporalVars, beginRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
evidence, (*action,*) proposalReceptionTime>>
\/ \E msgs \in SUBSET FaultyPrecommits(r):
/\ msgsPrecommit' = [msgsPrecommit EXCEPT ![r] = @ \union msgs]
/\ UNCHANGED <<coreVars, temporalVars, beginRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
evidence, (*action,*) proposalReceptionTime>>
(************************ MESSAGE PASSING ********************************)
\* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool;
@@ -391,8 +441,7 @@ StartRound(p, r) ==
/\ round' = [round EXCEPT ![p] = r]
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
\* We only need to update (last)beginRound[r] once a process enters round `r`
/\ beginRound' = [beginRound EXCEPT ![r] = Min2(@, localClock[p])]
/\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
/\ beginRound' = [beginRound EXCEPT ![r,p] = localClock[p]]
\* lines 14-19, a proposal may be sent later
\* @type: (PROCESS) => Bool;
@@ -403,7 +452,6 @@ InsertProposal(p) ==
\* if the proposer is sending a proposal, then there are no other proposals
\* by the correct processes for the same round
/\ \A m \in msgsPropose[r]: m.src /= p
\* /\ localClock[p] >
/\ \E v \in ValidValues:
LET proposal ==
IF validValue[p] /= NilProposal
@@ -411,17 +459,14 @@ InsertProposal(p) ==
ELSE Proposal(v, localClock[p], r)
IN
/\ BroadcastProposal(p, r, proposal, validRound[p])
/\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
/\ UNCHANGED <<temporalVars, coreVars>>
/\ UNCHANGED
<<(*msgsPropose,*) msgsPrevote, msgsPrecommit,
evidence, receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED
<<beginRound, endConsensus, lastBeginRound,
(*proposalTime,*) proposalReceivedTime>>
evidence, proposalReceptionTime>>
/\ UNCHANGED beginRound
/\ action' = "InsertProposal"
\* a new action used to filter messages that are not on time
\* a new action used to register the proposal and note the reception time.
\* [PBTS-RECEPTION-STEP.0]
\* @type: (PROCESS) => Bool;
ReceiveProposal(p) ==
@@ -439,30 +484,13 @@ ReceiveProposal(p) ==
]
IN
/\ msg \in msgsPropose[round[p]]
/\ inspectedProposal[r,p] = NilTimestamp
/\ msg \notin receivedTimelyProposal[p]
/\ inspectedProposal' = [inspectedProposal EXCEPT ![r,p] = localClock[p]]
/\ LET
isTimely == IsTimely(localClock[p], t)
IN
\/ /\ isTimely
/\ receivedTimelyProposal' = [receivedTimelyProposal EXCEPT ![p] = @ \union {msg}]
/\ LET
isNilTimestamp == proposalReceivedTime[r] = NilTimestamp
IN
\/ /\ isNilTimestamp
/\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
\/ /\ ~isNilTimestamp
/\ UNCHANGED proposalReceivedTime
\/ /\ ~isTimely
/\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
/\ proposalReceptionTime[r,p] = NilTimestamp
/\ proposalReceptionTime' = [proposalReceptionTime EXCEPT ![r,p] = localClock[p]]
/\ UNCHANGED <<temporalVars, coreVars>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
evidence(*, receivedTimelyProposal, inspectedProposal*)>>
/\ UNCHANGED
<<beginRound, endConsensus, lastBeginRound,
proposalTime(*, proposalReceivedTime*)>>
evidence(*, proposalReceptionTime*)>>
/\ UNCHANGED beginRound
/\ action' = "ReceiveProposal"
\* lines 22-27
@@ -487,22 +515,29 @@ UponProposalInPropose(p) ==
validRound |-> NilRound
]
IN
/\ msg \in receivedTimelyProposal[p] \* updated line 22
/\ evidence' = {msg} \union evidence
/\ LET mid == (* line 23 *)
IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
IF
\* Timeliness is checked against the process time, as was
\* recorded in proposalReceptionTime, not as it is now.
\* In the implementation, if the proposal is not timely, then we prevote
\* nil. In the natural-language specification, nothing happens.
\* This specification maintains consistency with the implementation.
/\ IsTimely( proposalReceptionTime[r, p], t) \* updated line 22
/\ IsValid(prop)
/\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
THEN Id(prop)
ELSE NilProposal
IN
BroadcastPrevote(p, r, mid) \* lines 24-26
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED <<temporalVars, beginRound>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
(*evidence,*) proposalReceptionTime>>
/\ action' = "UponProposalInPropose"
\* lines 28-33
@@ -541,13 +576,13 @@ UponProposalInProposeAndPrevote(p) ==
IN
BroadcastPrevote(p, r, mid) \* lines 24-26
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED <<temporalVars, beginRound>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
(*evidence,*) proposalReceptionTime>>
/\ action' = "UponProposalInProposeAndPrevote"
\* lines 34-35 + lines 61-64 (onTimeoutPrevote)
@@ -562,13 +597,13 @@ UponQuorumOfPrevotesAny(p) ==
/\ evidence' = MyEvidence \union evidence
/\ BroadcastPrecommit(p, round[p], NilProposal)
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED <<temporalVars, beginRound>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
(*evidence,*) proposalReceptionTime>>
/\ action' = "UponQuorumOfPrevotesAny"
\* lines 36-46
@@ -610,13 +645,13 @@ UponProposalInPrevoteOrCommitAndPrevote(p) ==
\* lines 42-43
/\ validValue' = [validValue EXCEPT ![p] = prop]
/\ validRound' = [validRound EXCEPT ![p] = r]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED <<temporalVars, beginRound>>
/\ UNCHANGED
<<round, (*step,*) decision(*, lockedValue,
lockedRound, validValue, validRound*)>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
(*evidence,*) proposalReceptionTime>>
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
\* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -631,15 +666,12 @@ UponQuorumOfPrecommitsAny(p) ==
/\ round[p] + 1 \in Rounds
/\ StartRound(p, round[p] + 1)
/\ UNCHANGED temporalVars
/\ UNCHANGED
<<(*beginRound,*) endConsensus, (*lastBeginRound,*)
proposalTime, proposalReceivedTime>>
/\ UNCHANGED
<<(*round, step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
(*evidence,*) proposalReceptionTime>>
/\ action' = "UponQuorumOfPrecommitsAny"
\* lines 49-54
@@ -664,14 +696,13 @@ UponProposalInPrecommitNoDecision(p) ==
]
IN
/\ msg \in msgsPropose[r] \* line 49
/\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
/\ proposalReceptionTime[r,p] /= NilTimestamp \* Keep?
/\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN
/\ Cardinality(PV) >= THRESHOLD2 \* line 49
/\ evidence' = PV \union {msg} \union evidence
/\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* update the decision, line 51
\* The original algorithm does not have 'DECIDED', but it increments the height.
\* We introduced 'DECIDED' here to prevent the process from changing its decision.
/\ endConsensus' = [endConsensus EXCEPT ![p] = localClock[p]]
/\ step' = [step EXCEPT ![p] = "DECIDED"]
/\ UNCHANGED temporalVars
/\ UNCHANGED
@@ -679,10 +710,8 @@ UponProposalInPrecommitNoDecision(p) ==
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ UNCHANGED
<<beginRound, (*endConsensus,*) lastBeginRound,
proposalTime, proposalReceivedTime>>
(*evidence,*) proposalReceptionTime>>
/\ UNCHANGED beginRound
/\ action' = "UponProposalInPrecommitNoDecision"
\* the actions below are not essential for safety, but added for completeness
@@ -694,13 +723,13 @@ OnTimeoutPropose(p) ==
/\ p /= Proposer[round[p]]
/\ BroadcastPrevote(p, round[p], NilProposal)
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED <<temporalVars, beginRound>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
evidence, receivedTimelyProposal, inspectedProposal>>
evidence, proposalReceptionTime>>
/\ action' = "OnTimeoutPropose"
\* lines 44-46
@@ -712,36 +741,34 @@ OnQuorumOfNilPrevotes(p) ==
/\ evidence' = PV \union evidence
/\ BroadcastPrecommit(p, round[p], Id(NilProposal))
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
/\ UNCHANGED <<temporalVars, invariantVars>>
/\ UNCHANGED <<temporalVars, beginRound>>
/\ UNCHANGED
<<round, (*step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
(*evidence,*) proposalReceptionTime>>
/\ action' = "OnQuorumOfNilPrevotes"
\* lines 55-56
\* @type: (PROCESS) => Bool;
OnRoundCatchup(p) ==
\E r \in {rr \in Rounds: rr > round[p]}:
LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
\E MyEvidence \in SUBSET RoundMsgs:
LET Faster == { m.src: m \in MyEvidence } IN
/\ Cardinality(Faster) >= THRESHOLD1
/\ evidence' = MyEvidence \union evidence
/\ StartRound(p, r)
/\ UNCHANGED temporalVars
/\ UNCHANGED
<<(*beginRound,*) endConsensus, (*lastBeginRound,*)
proposalTime, proposalReceivedTime>>
/\ UNCHANGED
<<(*round, step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
/\ action' = "OnRoundCatchup"
\E r \in Rounds:
/\ r > round[p]
/\ LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
\E MyEvidence \in SUBSET RoundMsgs:
LET Faster == { m.src: m \in MyEvidence } IN
/\ Cardinality(Faster) >= THRESHOLD1
/\ evidence' = MyEvidence \union evidence
/\ StartRound(p, r)
/\ UNCHANGED temporalVars
/\ UNCHANGED
<<(*round, step,*) decision, lockedValue,
lockedRound, validValue, validRound>>
/\ UNCHANGED
<<msgsPropose, msgsPrevote, msgsPrecommit,
(*evidence,*) proposalReceptionTime>>
/\ action' = "OnRoundCatchup"
(********************* PROTOCOL TRANSITIONS ******************************)
@@ -753,19 +780,8 @@ AdvanceRealTime ==
/\ t > realTime
/\ realTime' = t
/\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)]
/\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
/\ UNCHANGED <<coreVars, bookkeepingVars, beginRound>>
/\ action' = "AdvanceRealTime"
\* advance the local clock of node p to some larger time t, not necessarily by 1
\* #type: (PROCESS) => Bool;
\* AdvanceLocalClock(p) ==
\* /\ ValidTime(localClock[p])
\* /\ \E t \in Timestamps:
\* /\ t > localClock[p]
\* /\ localClock' = [localClock EXCEPT ![p] = t]
\* /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
\* /\ UNCHANGED realTime
\* /\ action' = "AdvanceLocalClock"
\* process timely messages
\* @type: (PROCESS) => Bool;
@@ -792,6 +808,7 @@ MessageProcessing(p) ==
*)
Next ==
\/ AdvanceRealTime
\/ FaultyBroadcast
\/ /\ SynchronizedLocalClocks
/\ \E p \in Corr: MessageProcessing(p)
@@ -810,76 +827,72 @@ AgreementOnValue ==
/\ decision[p] = Decision(prop, r1)
/\ decision[q] = Decision(prop, r2)
\* [PBTS-CONSENSUS-TIME-VALID.0]
DisagreementOnValue ==
\E p, q \in Corr:
\E p1 \in ValidProposals, p2 \in ValidProposals, r1 \in Rounds, r2 \in Rounds:
/\ p1 /= p2
/\ decision[p] = Decision(p1, r1)
/\ decision[q] = Decision(p2, r2)
\* [PBTS-INV-VALID.0]
ConsensusValidValue ==
\A p \in Corr:
\* decision[p] = Decision(Proposal(v,t,pr), r)
LET prop == decision[p][1] IN
prop /= NilProposal => prop[1] \in ValidValues
\* [PBTS-INV-MONOTONICITY.0]
\* TODO: we would need to compare timestamps of blocks from different height
\* [PBTS-INV-TIMELY.0]
ConsensusTimeValid ==
\A p \in Corr:
\* if a process decides on v and t
\E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds :
\* FIXME: do we need to enforce pr <= dr?
decision[p] = Decision(Proposal(v,t,pr), dr)
\* then
\* TODO: consider tighter bound where beginRound[pr] is replaced
\* w/ MedianOfRound[pr]
=> (/\ beginRound[pr] - Precision - Delay <= t
/\ t <= endConsensus[p] + Precision)
\* then a process found t timely at its proposal round (pr)
=> \E q \in Corr:
LET propRecvTime == proposalReceptionTime[pr, q] IN
(
/\ beginRound[pr, q] <= propRecvTime
/\ beginRound[pr+1, q] >= propRecvTime
/\ IsTimely(propRecvTime, t)
)
\* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
ConsensusSafeValidCorrProp ==
\A v \in ValidValues:
\* and there exists a process that decided on v, t
/\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds :
\* if the proposer in the round is correct
(/\ Proposer[pr] \in Corr
/\ decision[p] = Decision(Proposal(v,t,pr), dr))
\* then t is between the minimal and maximal initial local time
=> /\ beginRound[pr] <= t
/\ t <= lastBeginRound[pr]
IsFirstProposedInRound(prop, src, r) ==
\E msg \in msgsPropose[r]:
/\ msg.proposal = prop
/\ msg.src = src
\* If a proposal is reused this changes from Nil to a valid round
/\ msg.validRound = NilRound
\* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
ConsensusRealTimeValidCorr ==
\A r \in Rounds :
\E p \in Corr, v \in ValidValues, t \in Timestamps, pr \in Rounds:
(/\ decision[p] = Decision(Proposal(v,t,pr), r)
/\ proposalTime[r] /= NilTimestamp)
=> (/\ proposalTime[r] - Precision <= t
/\ t <= proposalTime[r] + Precision)
TimeLiveness ==
\A r \in Rounds \ {MaxRound}, v \in ValidValues:
LET p == Proposer[r] IN
p \in Corr \* Correct process is proposer in round r
=>
\E t \in Timestamps:
LET prop == Proposal(v,t,r) IN
(
/\ IsFirstProposedInRound(prop, p, r) \* p proposes v with some timestamp t in round r
/\ LET tOffset == t + Delay + Precision IN
/\ firstBeginRound[r] <= t
/\ t <= lastBeginRound[r]
/\ lastBeginRound[r] <= tOffset
/\ tOffset <= firstBeginRound[r+1]
) =>
\A q \in Corr:
\* q eventually decides prop
LET dq == decision[q] IN
dq /= NilDecision => dq[1] = prop
\* [PBTS-CONSENSUS-REALTIME-VALID.0]
ConsensusRealTimeValid ==
\A t \in Timestamps, r \in Rounds :
(\E p \in Corr, v \in ValidValues, pr \in Rounds :
decision[p] = Decision(Proposal(v,t,pr), r))
=> /\ proposalReceivedTime[r] - Precision < t
/\ t < proposalReceivedTime[r] + Precision + Delay
DecideAfterMin == TRUE
\* if decide => time > min
\* [PBTS-MSG-FAIR.0]
BoundedDelay ==
\A r \in Rounds :
(/\ proposalTime[r] /= NilTimestamp
/\ proposalTime[r] + Delay < realTime)
=> \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
\* [PBTS-CONSENSUS-TIME-LIVE.0]
ConsensusTimeLive ==
\A r \in Rounds, p \in Corr :
(/\ proposalTime[r] /= NilTimestamp
/\ proposalTime[r] + Delay < realTime
/\ Proposer[r] \in Corr
/\ round[p] <= r)
=> \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p]
\* a conjunction of all invariants
Inv ==
/\ AgreementOnValue
/\ ConsensusValidValue
/\ ConsensusTimeValid
/\ ConsensusSafeValidCorrProp
\* /\ ConsensusRealTimeValid
\* /\ ConsensusRealTimeValidCorr
\* /\ BoundedDelay
\* Liveness ==
\* ConsensusTimeLive
/\ TimeLiveness
=============================================================================

View File

@@ -0,0 +1,789 @@
@!@!@STARTMSG 2262:0 @!@!@
Created by Apalache on Wed May 18 11:06:20 UTC 2022
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2110:1 @!@!@
Invariant is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "Init"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, -1>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, -1>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PROPOSE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "ReceiveProposal"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, -1>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PROPOSE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPropose"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1]}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, -1>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PREVOTE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "ReceiveProposal"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1]}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PREVOTE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrevoteOrCommitAndPrevote"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PRECOMMIT">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPropose"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PREVOTE">>, <<"c2", "PRECOMMIT">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
7: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrecommitNoDecision"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>, <<"c2", <<<<"v0", 3, 0>>, 0>>>>
})
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PREVOTE">>, <<"c2", "DECIDED">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
8: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrevoteOrCommitAndPrevote"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>, <<"c2", <<<<"v0", 3, 0>>, 0>>>>
})
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "v1">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PRECOMMIT">>, <<"c2", "DECIDED">> })
/\ validRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"v1", 2, 0>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
9: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrecommitNoDecision"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"v1", 2, 0>>, 0>>>>, <<"c2", <<<<"v0", 3, 0>>, 0>>>> })
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "v1">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "DECIDED">>, <<"c2", "DECIDED">> })
/\ validRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"v1", 2, 0>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@

View File

@@ -0,0 +1,789 @@
@!@!@STARTMSG 2262:0 @!@!@
Created by Apalache on Wed May 18 11:06:20 UTC 2022
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2110:1 @!@!@
Invariant is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "Init"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, -1>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, -1>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PROPOSE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "ReceiveProposal"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, -1>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PROPOSE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPropose"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1]}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, -1>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PREVOTE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "ReceiveProposal"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = {[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1]}
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "None">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f3",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PREVOTE">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", -1>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"None", -1, -1>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrevoteOrCommitAndPrevote"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PROPOSE">>, <<"c2", "PRECOMMIT">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPropose"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>,
<<"c2", <<<<"None", -1, -1>>, -1>>>> })
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PREVOTE">>, <<"c2", "PRECOMMIT">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
7: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrecommitNoDecision"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>, <<"c2", <<<<"v0", 3, 0>>, 0>>>>
})
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "None">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PREVOTE">>, <<"c2", "DECIDED">> })
/\ validRound = SetAsFun({ <<"c1", -1>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"None", -1, -1>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
8: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrevoteOrCommitAndPrevote"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"None", -1, -1>>, -1>>>>, <<"c2", <<<<"v0", 3, 0>>, 0>>>>
})
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "v1">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "PRECOMMIT">>, <<"c2", "DECIDED">> })
/\ validRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"v1", 2, 0>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
9: <Next>
/\ Proposer = SetAsFun({ <<0, "f4">>, <<1, "f4">>, <<2, "f4">>, <<3, "f4">> })
/\ action = "UponProposalInPrecommitNoDecision"
/\ beginRound = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, 7>>,
<<<<1, "c1">>, 7>>,
<<<<2, "c2">>, 7>>,
<<<<1, "c2">>, 7>>,
<<<<3, "c2">>, 7>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, 7>> })
/\ decision = SetAsFun({ <<"c1", <<<<"v1", 2, 0>>, 0>>>>, <<"c2", <<<<"v0", 3, 0>>, 0>>>> })
/\ evidence = { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1],
[proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
/\ localClock = SetAsFun({ <<"c1", 3>>, <<"c2", 2>> })
/\ lockedRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ lockedValue = SetAsFun({ <<"c1", "v1">>, <<"c2", "v0">> })
/\ msgsPrecommit = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "c2",
type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PRECOMMIT"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PRECOMMIT"] }
>>,
<<1, {}>>,
<<
2, {[id |-> <<"v2", 3, 2>>, round |-> 2, src |-> "f3", type |-> "PRECOMMIT"]}
>>,
<<
3, {[id |-> <<"v2", 7, 3>>, round |-> 3, src |-> "f4", type |-> "PRECOMMIT"]}
>> })
/\ msgsPrevote = SetAsFun({ <<
0, { [id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "c2", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v0", 3, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "c1", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f3", type |-> "PREVOTE"],
[id |-> <<"v1", 2, 0>>, round |-> 0, src |-> "f4", type |-> "PREVOTE"] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ msgsPropose = SetAsFun({ <<
0, { [proposal |-> <<"v0", 3, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> 2],
[proposal |-> <<"v1", 2, 0>>,
round |-> 0,
src |-> "f4",
type |-> "PROPOSAL",
validRound |-> -1] }
>>,
<<1, {}>>,
<<2, {}>>,
<<3, {}>> })
/\ proposalReceptionTime = SetAsFun({ <<<<0, "c1">>, 3>>,
<<<<2, "c1">>, -1>>,
<<<<1, "c1">>, -1>>,
<<<<2, "c2">>, -1>>,
<<<<1, "c2">>, -1>>,
<<<<3, "c2">>, -1>>,
<<<<0, "c2">>, 2>>,
<<<<3, "c1">>, -1>> })
/\ realTime = 0
/\ round = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ step = SetAsFun({ <<"c1", "DECIDED">>, <<"c2", "DECIDED">> })
/\ validRound = SetAsFun({ <<"c1", 0>>, <<"c2", 0>> })
/\ validValue = SetAsFun({ <<"c1", <<"v1", 2, 0>>>>, <<"c2", <<"v0", 3, 0>>>> })
@!@!@ENDMSG 2217 @!@!@

View File

@@ -0,0 +1,896 @@
--------------------------- MODULE 04_OutInlinePass ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
CONSTANT
(*
@type: (Int -> Str);
*)
Proposer
VARIABLE
(*
@type: (Str -> <<<<Str, Int, Int>>, Int>>);
*)
decision
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrecommit
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
beginRound
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrevote
VARIABLE
(*
@type: Str;
*)
action
VARIABLE
(*
@type: (Str -> Int);
*)
lockedRound
VARIABLE
(*
@type: (Int -> Set([proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
msgsPropose
VARIABLE
(*
@type: (Str -> Int);
*)
validRound
VARIABLE
(*
@type: (Str -> Str);
*)
step
VARIABLE
(*
@type: (Str -> Str);
*)
lockedValue
VARIABLE
(*
@type: (Str -> <<Str, Int, Int>>);
*)
validValue
VARIABLE
(*
@type: Int;
*)
realTime
VARIABLE
(*
@type: (Str -> Int);
*)
round
VARIABLE
(*
@type: Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
evidence
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
proposalReceptionTime
VARIABLE
(*
@type: (Str -> Int);
*)
localClock
(*
@type: (() => Bool);
*)
CInit == Proposer \in [(0 .. 3) -> ({ "c1", "c2" } \union { "f3", "f4" })]
(*
@type: (() => Bool);
*)
Inv ==
(\A p$22 \in { "c1", "c2" }:
\A q$6 \in { "c1", "c2" }:
decision[p$22] /= <<<<"None", (-1), (-1)>>, (-1)>>
/\ decision[q$6] /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (\E v$10 \in { "v0", "v1" }:
\E t$10 \in 0 .. 7:
\E pr$5 \in 0 .. 3:
\E r1$3 \in 0 .. 3:
\E r2$3 \in 0 .. 3:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_8 == <<v$10, t$10, pr$5>>
IN
decision[p$22] = <<(prop_si_8), r1$3>>
/\ decision[q$6] = <<(prop_si_8), r2$3>>))
/\ (\A p$23 \in { "c1", "c2" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_9 == decision[p$23][1]
IN
prop_si_9 /= <<"None", (-1), (-1)>> => (prop_si_9)[1] \in { "v0", "v1" })
/\ (\A p$24 \in { "c1", "c2" }:
\E v$11 \in { "v0", "v1" }:
\E t$11 \in 0 .. 7:
\E pr$6 \in 0 .. 3:
\E dr$2 \in 0 .. 3:
decision[p$24] = <<<<v$11, t$11, pr$6>>, dr$2>>
=> (\E q$7 \in { "c1", "c2" }:
LET (*
@type: (() => Int);
*)
propRecvTime_si_2 == proposalReceptionTime[pr$6, q$7]
IN
beginRound[pr$6, q$7] <= propRecvTime_si_2
/\ beginRound[(pr$6 + 1), q$7] >= propRecvTime_si_2
/\ (propRecvTime_si_2 >= t$11 - 2
/\ propRecvTime_si_2 <= (t$11 + 2) + 2)))
/\ (\A r$31 \in 0 .. 3 \ {3}:
\A v$12 \in { "v0", "v1" }:
LET (*@type: (() => Str); *) p_si_25 == Proposer[r$31] IN
p_si_25 \in { "c1", "c2" }
=> (\E t$12 \in 0 .. 7:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_10 == <<v$12, t$12, r$31>>
IN
(\E msg$8 \in msgsPropose[r$31]:
msg$8["proposal"] = prop_si_10
/\ msg$8["src"] = p_si_25
/\ msg$8["validRound"] = -1)
/\ LET (*@type: (() => Int); *) tOffset_si_2 == (t$12 + 2) + 2 IN
[
r$32 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_4(a_si_7, b_si_7) == IF a$7 <= b$7 THEN a$7 ELSE b$7
IN
Min2$4, 7, {
beginRound[r$32, p$26]:
p$26 \in { "c1", "c2" }
})
][
r$31
]
<= t$12
/\ t$12
<= [
r$33 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_4(a_si_8, b_si_8) ==
IF a$8 >= b$8 THEN a$8 ELSE b$8
IN
Max2$4, (-1), {
beginRound[r$33, p$27]:
p$27 \in { "c1", "c2" }
})
][
r$31
]
/\ [
r$34 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_5(a_si_9, b_si_9) == IF a$9 >= b$9 THEN a$9 ELSE b$9
IN
Max2$5, (-1), {
beginRound[r$34, p$28]:
p$28 \in { "c1", "c2" }
})
][
r$31
]
<= tOffset_si_2
/\ tOffset_si_2
<= [
r$35 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_5(a_si_10, b_si_10) ==
IF a$10 <= b$10 THEN a$10 ELSE b$10
IN
Min2$5, 7, {
beginRound[r$35, p$29]:
p$29 \in { "c1", "c2" }
})
][
(r$31 + 1)
]
=> (\A q$8 \in { "c1", "c2" }:
LET (*
@type: (() => <<<<Str, Int, Int>>, Int>>);
*)
dq_si_2 == decision[q$8]
IN
dq_si_2 /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (dq_si_2)[1] = prop_si_10)))
(*
@type: (() => Bool);
*)
Init ==
round = [ p$10 \in { "c1", "c2" } |-> 0 ]
/\ localClock \in [{ "c1", "c2" } -> (2 .. 2 + 2)]
/\ realTime = 0
/\ step = [ p$11 \in { "c1", "c2" } |-> "PROPOSE" ]
/\ decision
= [ p$12 \in { "c1", "c2" } |-> <<<<"None", (-1), (-1)>>, (-1)>> ]
/\ lockedValue = [ p$13 \in { "c1", "c2" } |-> "None" ]
/\ lockedRound = [ p$14 \in { "c1", "c2" } |-> -1 ]
/\ validValue = [ p$15 \in { "c1", "c2" } |-> <<"None", (-1), (-1)>> ]
/\ validRound = [ p$16 \in { "c1", "c2" } |-> -1 ]
/\ ((TRUE
/\ (msgsPropose \in [(0 .. 3) -> Gen(5)]
/\ msgsPrevote \in [(0 .. 3) -> Gen(5)]
/\ msgsPrecommit \in [(0 .. 3) -> Gen(5)]
/\ ((\A r$43 \in 0 .. 3:
msgsPropose[r$43]
\subseteq [type: {"PROPOSAL"},
src: { "f3", "f4" },
round: 0 .. 3,
proposal:
({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]
/\ (\A m$29 \in msgsPropose[r$43]: r$43 = m$29["round"])))
/\ ((\A r$44 \in 0 .. 3:
msgsPrevote[r$44]
\subseteq [type: {"PREVOTE"},
src: { "f3", "f4" },
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$30 \in msgsPrevote[r$44]: r$44 = m$30["round"])))
/\ ((\A r$45 \in 0 .. 3:
msgsPrecommit[r$45]
\subseteq [type: {"PRECOMMIT"},
src: { "f3", "f4" },
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$31 \in msgsPrecommit[r$45]: r$45 = m$31["round"])))))
\/ (~TRUE
/\ msgsPropose = [ r$46 \in 0 .. 3 |-> {} ]
/\ msgsPrevote = [ r$47 \in 0 .. 3 |-> {} ]
/\ msgsPrecommit = [ r$48 \in 0 .. 3 |-> {} ]))
/\ proposalReceptionTime = [ r_p$1 \in (0 .. 3) \X { "c1", "c2" } |-> -1 ]
/\ evidence = {}
/\ action = "Init"
/\ beginRound
= [
r_c$1 \in (0 .. 3) \X { "c1", "c2" } |->
IF r_c$1[1] = 0 THEN localClock[r_c$1[2]] ELSE 7
]
(*
@type: (() => Bool);
*)
Next ==
(realTime < 7
/\ (\E t$18 \in 0 .. 7:
t$18 > realTime
/\ realTime' = t$18
/\ localClock'
= [ p$30 \in { "c1", "c2" } |-> localClock[p$30] + t$18 - realTime ])
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>
/\ <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>'
= <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>
/\ beginRound' := beginRound)
/\ action' = "AdvanceRealTime")
\/ (~TRUE
/\ action' = "FaultyBroadcast"
/\ (\E r$49 \in 0 .. 3:
(\E msgs$4 \in SUBSET ([type: {"PROPOSAL"},
src: { "f3", "f4" },
round: {r$49},
proposal: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]):
msgsPropose'
= [
msgsPropose EXCEPT
![r$49] = msgsPropose[r$49] \union msgs$4
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$5 \in SUBSET ([type: {"PREVOTE"},
src: { "f3", "f4" },
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrevote'
= [
msgsPrevote EXCEPT
![r$49] = msgsPrevote[r$49] \union msgs$5
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$6 \in SUBSET ([type: {"PRECOMMIT"},
src: { "f3", "f4" },
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r$49] = msgsPrecommit[r$49] \union msgs$6
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))))
\/ ((\A p$31 \in { "c1", "c2" }:
\A q$9 \in { "c1", "c2" }:
p$31 /= q$9
=> (localClock[p$31] >= localClock[q$9]
/\ localClock[p$31] - localClock[q$9] < 2)
\/ (localClock[p$31] < localClock[q$9]
/\ localClock[q$9] - localClock[p$31] < 2))
/\ (\E p$17 \in { "c1", "c2" }:
LET (*@type: (() => Int); *) r_si_50 == round[p$17] IN
p$17 = Proposer[(r_si_50)]
/\ step[p$17] = "PROPOSE"
/\ (\A m$32 \in msgsPropose[(r_si_50)]: m$32["src"] /= p$17)
/\ (\E v$19 \in { "v0", "v1" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
proposal_si_3 ==
IF validValue[p$17] /= <<"None", (-1), (-1)>>
THEN validValue[p$17]
ELSE <<v$19, localClock[p$17], (r_si_50)>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
newMsg_si_18 ==
[type |-> "PROPOSAL",
src |-> p$17,
round |-> r_si_50,
proposal |-> proposal_si_3,
validRound |-> validRound[p$17]]
IN
msgsPropose'
= [
msgsPropose EXCEPT
![r_si_50] =
msgsPropose[(r_si_50)] \union {(newMsg_si_18)}
])
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "InsertProposal"
\/ (\E v$20 \in { "v0", "v1" } \union {"v2"}:
\E t$19 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_51 == round[p$17] IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_14 ==
[type |-> "PROPOSAL",
src |-> Proposer[round[p$17]],
round |-> round[p$17],
proposal |-> <<v$20, t$19, (r_si_51)>>,
validRound |-> -1]
IN
msg_si_14 \in msgsPropose[round[p$17]]
/\ proposalReceptionTime[(r_si_51), p$17] = -1
/\ proposalReceptionTime'
= [
proposalReceptionTime EXCEPT
![<<(r_si_51), p$17>>] = localClock[p$17]
]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence)
/\ beginRound' := beginRound
/\ action' = "ReceiveProposal")
\/ (\E v$21 \in { "v0", "v1" } \union {"v2"}:
\E t$20 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_52 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_15 == <<v$21, t$20, (r_si_52)>>
IN
step[p$17] = "PROPOSE"
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_15 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_52)],
round |-> r_si_52,
proposal |-> prop_si_15,
validRound |-> -1]
IN
evidence' = {(msg_si_15)} \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_5 ==
IF (proposalReceptionTime[(r_si_52), p$17] >= t$20 - 2
/\ proposalReceptionTime[(r_si_52), p$17]
<= (t$20 + 2) + 2)
/\ prop_si_15 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] = -1 \/ lockedValue[p$17] = v$21)
THEN prop_si_15
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_19 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_52,
id |-> mid_si_5]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_52] =
msgsPrevote[(r_si_52)] \union {(newMsg_si_19)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPropose")
\/ (\E v$22 \in { "v0", "v1" } \union {"v2"}:
\E t$21 \in 0 .. 7:
\E vr$7 \in 0 .. 3:
\E pr$9 \in 0 .. 3:
LET (*@type: (() => Int); *) r_si_53 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_16 == <<v$22, t$21, pr$9>>
IN
((step[p$17] = "PROPOSE" /\ 0 <= vr$7) /\ vr$7 < r_si_53)
/\ pr$9 <= vr$7
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_16 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_53)],
round |-> r_si_53,
proposal |-> prop_si_16,
validRound |-> vr$7]
IN
msg_si_16 \in msgsPropose[(r_si_53)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_9 ==
{ m$33 \in msgsPrevote[vr$7]: m$33["id"] = prop_si_16 }
IN
Cardinality((PV_si_9)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_9 \union {(msg_si_16)}) \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_6 ==
IF prop_si_16 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] <= vr$7
\/ lockedValue[p$17] = v$22)
THEN prop_si_16
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_20 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_53,
id |-> mid_si_6]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_53] =
msgsPrevote[(r_si_53)] \union {(newMsg_si_20)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInProposeAndPrevote")
\/ (step[p$17] = "PREVOTE"
/\ (\E MyEvidence$7 \in SUBSET (msgsPrevote[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Voters_si_3 == { m$34["src"]: m$34 \in MyEvidence$7 }
IN
Cardinality((Voters_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$7 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_21 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_21)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrevotesAny"))
\/ (\E v$23 \in { "v0", "v1" }:
\E t$22 \in 0 .. 7:
\E vr$8 \in 0 .. 3 \union {(-1)}:
LET (*@type: (() => Int); *) r_si_54 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_17 == <<v$23, t$22, (r_si_54)>>
IN
step[p$17] \in { "PREVOTE", "PRECOMMIT" }
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_17 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_54)],
round |-> r_si_54,
proposal |-> prop_si_17,
validRound |-> vr$8]
IN
msg_si_17 \in msgsPropose[(r_si_54)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_10 ==
{
m$35 \in msgsPrevote[(r_si_54)]:
m$35["id"] = prop_si_17
}
IN
Cardinality((PV_si_10)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_10 \union {(msg_si_17)}) \union evidence
/\ (IF step[p$17] = "PREVOTE"
THEN lockedValue' = [ lockedValue EXCEPT ![p$17] = v$23 ]
/\ lockedRound' = [ lockedRound EXCEPT ![p$17] = r_si_54 ]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_22 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> r_si_54,
id |-> prop_si_17]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r_si_54] =
msgsPrecommit[(r_si_54)] \union {(newMsg_si_22)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
ELSE lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ msgsPrecommit' := msgsPrecommit
/\ step' := step)
/\ validValue' = [ validValue EXCEPT ![p$17] = prop_si_17 ]
/\ validRound' = [ validRound EXCEPT ![p$17] = r_si_54 ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round /\ decision' := decision)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote")
\/ ((\E MyEvidence$8 \in SUBSET (msgsPrecommit[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Committers_si_3 == { m$36["src"]: m$36 \in MyEvidence$8 }
IN
Cardinality((Committers_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$8 \union evidence
/\ round[p$17] + 1 \in 0 .. 3
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = round[p$17] + 1 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<(round[p$17] + 1), p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrecommitsAny"))
\/ (decision[p$17] = <<<<"None", (-1), (-1)>>, (-1)>>
/\ (\E v$24 \in { "v0", "v1" }:
\E t$23 \in 0 .. 7:
\E r$55 \in 0 .. 3:
\E pr$10 \in 0 .. 3:
\E vr$9 \in 0 .. 3 \union {(-1)}:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_18 == <<v$24, t$23, pr$10>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_18 ==
[type |-> "PROPOSAL",
src |-> Proposer[r$55],
round |-> r$55,
proposal |-> prop_si_18,
validRound |-> vr$9]
IN
msg_si_18 \in msgsPropose[r$55]
/\ proposalReceptionTime[r$55, p$17] /= -1
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_11 ==
{
m$37 \in msgsPrecommit[r$55]:
m$37["id"] = prop_si_18
}
IN
Cardinality((PV_si_11)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_11 \union {(msg_si_18)}) \union evidence
/\ decision'
= [
decision EXCEPT
![p$17] = <<(prop_si_18), r$55>>
]
/\ step' = [ step EXCEPT ![p$17] = "DECIDED" ]
/\ <<localClock, realTime>>'
= <<localClock, realTime>>
/\ (round' := round
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "UponProposalInPrecommitNoDecision"))
\/ (step[p$17] = "PROPOSE"
/\ p$17 /= Proposer[round[p$17]]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_23 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![round[p$17]] =
msgsPrevote[round[p$17]] \union {(newMsg_si_23)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnTimeoutPropose")
\/ (step[p$17] = "PREVOTE"
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_12 ==
{
m$38 \in msgsPrevote[round[p$17]]:
m$38["id"] = <<"None", (-1), (-1)>>
}
IN
Cardinality((PV_si_12)) >= 2 * 1 + 1
/\ evidence' = PV_si_12 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_24 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_24)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnQuorumOfNilPrevotes")
\/ (\E r$56 \in 0 .. 3:
r$56 > round[p$17]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
RoundMsgs_si_3 ==
(msgsPropose[r$56] \union msgsPrevote[r$56])
\union msgsPrecommit[r$56]
IN
\E MyEvidence$9 \in SUBSET RoundMsgs_si_3:
LET (*
@type: (() => Set(Str));
*)
Faster_si_3 == { m$39["src"]: m$39 \in MyEvidence$9 }
IN
Cardinality((Faster_si_3)) >= 1 + 1
/\ evidence' = MyEvidence$9 \union evidence
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = r$56 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<r$56, p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnRoundCatchup")))
================================================================================

View File

@@ -0,0 +1,950 @@
--------------------------- MODULE 05_OutPrimingPass ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
CONSTANT
(*
@type: (Int -> Str);
*)
Proposer
VARIABLE
(*
@type: (Str -> <<<<Str, Int, Int>>, Int>>);
*)
decision
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrecommit
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
beginRound
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrevote
VARIABLE
(*
@type: Str;
*)
action
VARIABLE
(*
@type: (Str -> Int);
*)
lockedRound
VARIABLE
(*
@type: (Int -> Set([proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
msgsPropose
VARIABLE
(*
@type: (Str -> Int);
*)
validRound
VARIABLE
(*
@type: (Str -> Str);
*)
step
VARIABLE
(*
@type: (Str -> Str);
*)
lockedValue
VARIABLE
(*
@type: (Str -> <<Str, Int, Int>>);
*)
validValue
VARIABLE
(*
@type: Int;
*)
realTime
VARIABLE
(*
@type: (Str -> Int);
*)
round
VARIABLE
(*
@type: Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
evidence
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
proposalReceptionTime
VARIABLE
(*
@type: (Str -> Int);
*)
localClock
(*
@type: (() => Bool);
*)
CInit == Proposer \in [(0 .. 3) -> ({ "c1", "c2" } \union { "f3", "f4" })]
(*
@type: (() => Bool);
*)
Inv ==
(\A p$22 \in { "c1", "c2" }:
\A q$6 \in { "c1", "c2" }:
decision[p$22] /= <<<<"None", (-1), (-1)>>, (-1)>>
/\ decision[q$6] /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (\E v$10 \in { "v0", "v1" }:
\E t$10 \in 0 .. 7:
\E pr$5 \in 0 .. 3:
\E r1$3 \in 0 .. 3:
\E r2$3 \in 0 .. 3:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_8 == <<v$10, t$10, pr$5>>
IN
decision[p$22] = <<(prop_si_8), r1$3>>
/\ decision[q$6] = <<(prop_si_8), r2$3>>))
/\ (\A p$23 \in { "c1", "c2" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_9 == decision[p$23][1]
IN
prop_si_9 /= <<"None", (-1), (-1)>> => (prop_si_9)[1] \in { "v0", "v1" })
/\ (\A p$24 \in { "c1", "c2" }:
\E v$11 \in { "v0", "v1" }:
\E t$11 \in 0 .. 7:
\E pr$6 \in 0 .. 3:
\E dr$2 \in 0 .. 3:
decision[p$24] = <<<<v$11, t$11, pr$6>>, dr$2>>
=> (\E q$7 \in { "c1", "c2" }:
LET (*
@type: (() => Int);
*)
propRecvTime_si_2 == proposalReceptionTime[pr$6, q$7]
IN
beginRound[pr$6, q$7] <= propRecvTime_si_2
/\ beginRound[(pr$6 + 1), q$7] >= propRecvTime_si_2
/\ (propRecvTime_si_2 >= t$11 - 2
/\ propRecvTime_si_2 <= (t$11 + 2) + 2)))
/\ (\A r$31 \in 0 .. 3 \ {3}:
\A v$12 \in { "v0", "v1" }:
LET (*@type: (() => Str); *) p_si_25 == Proposer[r$31] IN
p_si_25 \in { "c1", "c2" }
=> (\E t$12 \in 0 .. 7:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_10 == <<v$12, t$12, r$31>>
IN
(\E msg$8 \in msgsPropose[r$31]:
msg$8["proposal"] = prop_si_10
/\ msg$8["src"] = p_si_25
/\ msg$8["validRound"] = -1)
/\ LET (*@type: (() => Int); *) tOffset_si_2 == (t$12 + 2) + 2 IN
[
r$32 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_4(a_si_7, b_si_7) == IF a$7 <= b$7 THEN a$7 ELSE b$7
IN
Min2$4, 7, {
beginRound[r$32, p$26]:
p$26 \in { "c1", "c2" }
})
][
r$31
]
<= t$12
/\ t$12
<= [
r$33 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_4(a_si_8, b_si_8) ==
IF a$8 >= b$8 THEN a$8 ELSE b$8
IN
Max2$4, (-1), {
beginRound[r$33, p$27]:
p$27 \in { "c1", "c2" }
})
][
r$31
]
/\ [
r$34 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_5(a_si_9, b_si_9) == IF a$9 >= b$9 THEN a$9 ELSE b$9
IN
Max2$5, (-1), {
beginRound[r$34, p$28]:
p$28 \in { "c1", "c2" }
})
][
r$31
]
<= tOffset_si_2
/\ tOffset_si_2
<= [
r$35 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_5(a_si_10, b_si_10) ==
IF a$10 <= b$10 THEN a$10 ELSE b$10
IN
Min2$5, 7, {
beginRound[r$35, p$29]:
p$29 \in { "c1", "c2" }
})
][
(r$31 + 1)
]
=> (\A q$8 \in { "c1", "c2" }:
LET (*
@type: (() => <<<<Str, Int, Int>>, Int>>);
*)
dq_si_2 == decision[q$8]
IN
dq_si_2 /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (dq_si_2)[1] = prop_si_10)))
(*
@type: (() => Bool);
*)
Init ==
round = [ p$10 \in { "c1", "c2" } |-> 0 ]
/\ localClock \in [{ "c1", "c2" } -> (2 .. 2 + 2)]
/\ realTime = 0
/\ step = [ p$11 \in { "c1", "c2" } |-> "PROPOSE" ]
/\ decision
= [ p$12 \in { "c1", "c2" } |-> <<<<"None", (-1), (-1)>>, (-1)>> ]
/\ lockedValue = [ p$13 \in { "c1", "c2" } |-> "None" ]
/\ lockedRound = [ p$14 \in { "c1", "c2" } |-> -1 ]
/\ validValue = [ p$15 \in { "c1", "c2" } |-> <<"None", (-1), (-1)>> ]
/\ validRound = [ p$16 \in { "c1", "c2" } |-> -1 ]
/\ ((TRUE
/\ (msgsPropose \in [(0 .. 3) -> Gen(5)]
/\ msgsPrevote \in [(0 .. 3) -> Gen(5)]
/\ msgsPrecommit \in [(0 .. 3) -> Gen(5)]
/\ ((\A r$43 \in 0 .. 3:
msgsPropose[r$43]
\subseteq [type: {"PROPOSAL"},
src: { "f3", "f4" },
round: 0 .. 3,
proposal:
({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]
/\ (\A m$29 \in msgsPropose[r$43]: r$43 = m$29["round"])))
/\ ((\A r$44 \in 0 .. 3:
msgsPrevote[r$44]
\subseteq [type: {"PREVOTE"},
src: { "f3", "f4" },
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$30 \in msgsPrevote[r$44]: r$44 = m$30["round"])))
/\ ((\A r$45 \in 0 .. 3:
msgsPrecommit[r$45]
\subseteq [type: {"PRECOMMIT"},
src: { "f3", "f4" },
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$31 \in msgsPrecommit[r$45]: r$45 = m$31["round"])))))
\/ (~TRUE
/\ msgsPropose = [ r$46 \in 0 .. 3 |-> {} ]
/\ msgsPrevote = [ r$47 \in 0 .. 3 |-> {} ]
/\ msgsPrecommit = [ r$48 \in 0 .. 3 |-> {} ]))
/\ proposalReceptionTime = [ r_p$1 \in (0 .. 3) \X { "c1", "c2" } |-> -1 ]
/\ evidence = {}
/\ action = "Init"
/\ beginRound
= [
r_c$1 \in (0 .. 3) \X { "c1", "c2" } |->
IF r_c$1[1] = 0 THEN localClock[r_c$1[2]] ELSE 7
]
(*
@type: (() => Bool);
*)
Next ==
(realTime < 7
/\ (\E t$18 \in 0 .. 7:
t$18 > realTime
/\ realTime' = t$18
/\ localClock'
= [ p$30 \in { "c1", "c2" } |-> localClock[p$30] + t$18 - realTime ])
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>
/\ <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>'
= <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>
/\ beginRound' := beginRound)
/\ action' = "AdvanceRealTime")
\/ (~TRUE
/\ action' = "FaultyBroadcast"
/\ (\E r$49 \in 0 .. 3:
(\E msgs$4 \in SUBSET ([type: {"PROPOSAL"},
src: { "f3", "f4" },
round: {r$49},
proposal: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]):
msgsPropose'
= [
msgsPropose EXCEPT
![r$49] = msgsPropose[r$49] \union msgs$4
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$5 \in SUBSET ([type: {"PREVOTE"},
src: { "f3", "f4" },
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrevote'
= [
msgsPrevote EXCEPT
![r$49] = msgsPrevote[r$49] \union msgs$5
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$6 \in SUBSET ([type: {"PRECOMMIT"},
src: { "f3", "f4" },
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r$49] = msgsPrecommit[r$49] \union msgs$6
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))))
\/ ((\A p$31 \in { "c1", "c2" }:
\A q$9 \in { "c1", "c2" }:
p$31 /= q$9
=> (localClock[p$31] >= localClock[q$9]
/\ localClock[p$31] - localClock[q$9] < 2)
\/ (localClock[p$31] < localClock[q$9]
/\ localClock[q$9] - localClock[p$31] < 2))
/\ (\E p$17 \in { "c1", "c2" }:
LET (*@type: (() => Int); *) r_si_50 == round[p$17] IN
p$17 = Proposer[(r_si_50)]
/\ step[p$17] = "PROPOSE"
/\ (\A m$32 \in msgsPropose[(r_si_50)]: m$32["src"] /= p$17)
/\ (\E v$19 \in { "v0", "v1" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
proposal_si_3 ==
IF validValue[p$17] /= <<"None", (-1), (-1)>>
THEN validValue[p$17]
ELSE <<v$19, localClock[p$17], (r_si_50)>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
newMsg_si_18 ==
[type |-> "PROPOSAL",
src |-> p$17,
round |-> r_si_50,
proposal |-> proposal_si_3,
validRound |-> validRound[p$17]]
IN
msgsPropose'
= [
msgsPropose EXCEPT
![r_si_50] =
msgsPropose[(r_si_50)] \union {(newMsg_si_18)}
])
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "InsertProposal"
\/ (\E v$20 \in { "v0", "v1" } \union {"v2"}:
\E t$19 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_51 == round[p$17] IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_14 ==
[type |-> "PROPOSAL",
src |-> Proposer[round[p$17]],
round |-> round[p$17],
proposal |-> <<v$20, t$19, (r_si_51)>>,
validRound |-> -1]
IN
msg_si_14 \in msgsPropose[round[p$17]]
/\ proposalReceptionTime[(r_si_51), p$17] = -1
/\ proposalReceptionTime'
= [
proposalReceptionTime EXCEPT
![<<(r_si_51), p$17>>] = localClock[p$17]
]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence)
/\ beginRound' := beginRound
/\ action' = "ReceiveProposal")
\/ (\E v$21 \in { "v0", "v1" } \union {"v2"}:
\E t$20 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_52 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_15 == <<v$21, t$20, (r_si_52)>>
IN
step[p$17] = "PROPOSE"
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_15 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_52)],
round |-> r_si_52,
proposal |-> prop_si_15,
validRound |-> -1]
IN
evidence' = {(msg_si_15)} \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_5 ==
IF (proposalReceptionTime[(r_si_52), p$17] >= t$20 - 2
/\ proposalReceptionTime[(r_si_52), p$17]
<= (t$20 + 2) + 2)
/\ prop_si_15 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] = -1 \/ lockedValue[p$17] = v$21)
THEN prop_si_15
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_19 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_52,
id |-> mid_si_5]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_52] =
msgsPrevote[(r_si_52)] \union {(newMsg_si_19)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPropose")
\/ (\E v$22 \in { "v0", "v1" } \union {"v2"}:
\E t$21 \in 0 .. 7:
\E vr$7 \in 0 .. 3:
\E pr$9 \in 0 .. 3:
LET (*@type: (() => Int); *) r_si_53 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_16 == <<v$22, t$21, pr$9>>
IN
((step[p$17] = "PROPOSE" /\ 0 <= vr$7) /\ vr$7 < r_si_53)
/\ pr$9 <= vr$7
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_16 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_53)],
round |-> r_si_53,
proposal |-> prop_si_16,
validRound |-> vr$7]
IN
msg_si_16 \in msgsPropose[(r_si_53)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_9 ==
{ m$33 \in msgsPrevote[vr$7]: m$33["id"] = prop_si_16 }
IN
Cardinality((PV_si_9)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_9 \union {(msg_si_16)}) \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_6 ==
IF prop_si_16 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] <= vr$7
\/ lockedValue[p$17] = v$22)
THEN prop_si_16
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_20 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_53,
id |-> mid_si_6]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_53] =
msgsPrevote[(r_si_53)] \union {(newMsg_si_20)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInProposeAndPrevote")
\/ (step[p$17] = "PREVOTE"
/\ (\E MyEvidence$7 \in SUBSET (msgsPrevote[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Voters_si_3 == { m$34["src"]: m$34 \in MyEvidence$7 }
IN
Cardinality((Voters_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$7 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_21 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_21)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrevotesAny"))
\/ (\E v$23 \in { "v0", "v1" }:
\E t$22 \in 0 .. 7:
\E vr$8 \in 0 .. 3 \union {(-1)}:
LET (*@type: (() => Int); *) r_si_54 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_17 == <<v$23, t$22, (r_si_54)>>
IN
step[p$17] \in { "PREVOTE", "PRECOMMIT" }
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_17 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_54)],
round |-> r_si_54,
proposal |-> prop_si_17,
validRound |-> vr$8]
IN
msg_si_17 \in msgsPropose[(r_si_54)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_10 ==
{
m$35 \in msgsPrevote[(r_si_54)]:
m$35["id"] = prop_si_17
}
IN
Cardinality((PV_si_10)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_10 \union {(msg_si_17)}) \union evidence
/\ (IF step[p$17] = "PREVOTE"
THEN lockedValue' = [ lockedValue EXCEPT ![p$17] = v$23 ]
/\ lockedRound' = [ lockedRound EXCEPT ![p$17] = r_si_54 ]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_22 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> r_si_54,
id |-> prop_si_17]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r_si_54] =
msgsPrecommit[(r_si_54)] \union {(newMsg_si_22)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
ELSE lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ msgsPrecommit' := msgsPrecommit
/\ step' := step)
/\ validValue' = [ validValue EXCEPT ![p$17] = prop_si_17 ]
/\ validRound' = [ validRound EXCEPT ![p$17] = r_si_54 ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round /\ decision' := decision)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote")
\/ ((\E MyEvidence$8 \in SUBSET (msgsPrecommit[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Committers_si_3 == { m$36["src"]: m$36 \in MyEvidence$8 }
IN
Cardinality((Committers_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$8 \union evidence
/\ round[p$17] + 1 \in 0 .. 3
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = round[p$17] + 1 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<(round[p$17] + 1), p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrecommitsAny"))
\/ (decision[p$17] = <<<<"None", (-1), (-1)>>, (-1)>>
/\ (\E v$24 \in { "v0", "v1" }:
\E t$23 \in 0 .. 7:
\E r$55 \in 0 .. 3:
\E pr$10 \in 0 .. 3:
\E vr$9 \in 0 .. 3 \union {(-1)}:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_18 == <<v$24, t$23, pr$10>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_18 ==
[type |-> "PROPOSAL",
src |-> Proposer[r$55],
round |-> r$55,
proposal |-> prop_si_18,
validRound |-> vr$9]
IN
msg_si_18 \in msgsPropose[r$55]
/\ proposalReceptionTime[r$55, p$17] /= -1
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_11 ==
{
m$37 \in msgsPrecommit[r$55]:
m$37["id"] = prop_si_18
}
IN
Cardinality((PV_si_11)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_11 \union {(msg_si_18)}) \union evidence
/\ decision'
= [
decision EXCEPT
![p$17] = <<(prop_si_18), r$55>>
]
/\ step' = [ step EXCEPT ![p$17] = "DECIDED" ]
/\ <<localClock, realTime>>'
= <<localClock, realTime>>
/\ (round' := round
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "UponProposalInPrecommitNoDecision"))
\/ (step[p$17] = "PROPOSE"
/\ p$17 /= Proposer[round[p$17]]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_23 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![round[p$17]] =
msgsPrevote[round[p$17]] \union {(newMsg_si_23)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnTimeoutPropose")
\/ (step[p$17] = "PREVOTE"
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_12 ==
{
m$38 \in msgsPrevote[round[p$17]]:
m$38["id"] = <<"None", (-1), (-1)>>
}
IN
Cardinality((PV_si_12)) >= 2 * 1 + 1
/\ evidence' = PV_si_12 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_24 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_24)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnQuorumOfNilPrevotes")
\/ (\E r$56 \in 0 .. 3:
r$56 > round[p$17]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
RoundMsgs_si_3 ==
(msgsPropose[r$56] \union msgsPrevote[r$56])
\union msgsPrecommit[r$56]
IN
\E MyEvidence$9 \in SUBSET RoundMsgs_si_3:
LET (*
@type: (() => Set(Str));
*)
Faster_si_3 == { m$39["src"]: m$39 \in MyEvidence$9 }
IN
Cardinality((Faster_si_3)) >= 1 + 1
/\ evidence' = MyEvidence$9 \union evidence
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = r$56 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<r$56, p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnRoundCatchup")))
CInitPrimed ==
Proposer' \in [(0 .. 3) -> ({ "c1", "c2" } \union { "f3", "f4" })]
InitPrimed ==
round' = [ p$10 \in { "c1", "c2" } |-> 0 ]
/\ localClock' \in [{ "c1", "c2" } -> (2 .. 2 + 2)]
/\ realTime' = 0
/\ step' = [ p$11 \in { "c1", "c2" } |-> "PROPOSE" ]
/\ decision'
= [ p$12 \in { "c1", "c2" } |-> <<<<"None", (-1), (-1)>>, (-1)>> ]
/\ lockedValue' = [ p$13 \in { "c1", "c2" } |-> "None" ]
/\ lockedRound' = [ p$14 \in { "c1", "c2" } |-> -1 ]
/\ validValue' = [ p$15 \in { "c1", "c2" } |-> <<"None", (-1), (-1)>> ]
/\ validRound' = [ p$16 \in { "c1", "c2" } |-> -1 ]
/\ ((TRUE
/\ (msgsPropose' \in [(0 .. 3) -> Gen(5)]
/\ msgsPrevote' \in [(0 .. 3) -> Gen(5)]
/\ msgsPrecommit' \in [(0 .. 3) -> Gen(5)]
/\ ((\A r$43 \in 0 .. 3:
msgsPropose'[r$43]
\subseteq [type: {"PROPOSAL"},
src: { "f3", "f4" },
round: 0 .. 3,
proposal:
({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]
/\ (\A m$29 \in msgsPropose'[r$43]: r$43 = m$29["round"])))
/\ ((\A r$44 \in 0 .. 3:
msgsPrevote'[r$44]
\subseteq [type: {"PREVOTE"},
src: { "f3", "f4" },
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$30 \in msgsPrevote'[r$44]: r$44 = m$30["round"])))
/\ ((\A r$45 \in 0 .. 3:
msgsPrecommit'[r$45]
\subseteq [type: {"PRECOMMIT"},
src: { "f3", "f4" },
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$31 \in msgsPrecommit'[r$45]: r$45 = m$31["round"])))))
\/ (~TRUE
/\ msgsPropose' = [ r$46 \in 0 .. 3 |-> {} ]
/\ msgsPrevote' = [ r$47 \in 0 .. 3 |-> {} ]
/\ msgsPrecommit' = [ r$48 \in 0 .. 3 |-> {} ]))
/\ proposalReceptionTime' = [ r_p$1 \in (0 .. 3) \X { "c1", "c2" } |-> -1 ]
/\ evidence' = {}
/\ action' = "Init"
/\ beginRound'
= [
r_c$1 \in (0 .. 3) \X { "c1", "c2" } |->
IF r_c$1[1] = 0 THEN localClock'[r_c$1[2]] ELSE 7
]
================================================================================

View File

@@ -0,0 +1,5 @@
Logging is disabled (Z3SolverContext.debug = false). Activate with --debug.
;; sat.random_seed = 0
;; smt.random_seed = 0
;; fp.spacer.random_seed = 0
;; sls.random_seed = 0

View File

@@ -0,0 +1 @@
check --length=8 --inv=Inv --cinit=CInit --discard-disabled=false MC_PBT_2C_2F.tla

View File

@@ -0,0 +1,900 @@
--------------------------- MODULE 04_OutInlinePass ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
CONSTANT
(*
@type: (Int -> Str);
*)
Proposer
VARIABLE
(*
@type: (Str -> <<<<Str, Int, Int>>, Int>>);
*)
decision
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrecommit
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
beginRound
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrevote
VARIABLE
(*
@type: Str;
*)
action
VARIABLE
(*
@type: (Str -> Int);
*)
lockedRound
VARIABLE
(*
@type: (Int -> Set([proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
msgsPropose
VARIABLE
(*
@type: (Str -> Int);
*)
validRound
VARIABLE
(*
@type: (Str -> Str);
*)
step
VARIABLE
(*
@type: (Str -> Str);
*)
lockedValue
VARIABLE
(*
@type: (Str -> <<Str, Int, Int>>);
*)
validValue
VARIABLE
(*
@type: Int;
*)
realTime
VARIABLE
(*
@type: (Str -> Int);
*)
round
VARIABLE
(*
@type: Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
evidence
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
proposalReceptionTime
VARIABLE
(*
@type: (Str -> Int);
*)
localClock
(*
@type: (() => Bool);
*)
CInit == Proposer \in [(0 .. 3) -> ({ "c1", "c2", "c3" } \union {"f4"})]
(*
@type: (() => Bool);
*)
Inv ==
(\A p$22 \in { "c1", "c2", "c3" }:
\A q$6 \in { "c1", "c2", "c3" }:
decision[p$22] /= <<<<"None", (-1), (-1)>>, (-1)>>
/\ decision[q$6] /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (\E v$10 \in { "v0", "v1" }:
\E t$10 \in 0 .. 7:
\E pr$5 \in 0 .. 3:
\E r1$3 \in 0 .. 3:
\E r2$3 \in 0 .. 3:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_8 == <<v$10, t$10, pr$5>>
IN
decision[p$22] = <<(prop_si_8), r1$3>>
/\ decision[q$6] = <<(prop_si_8), r2$3>>))
/\ (\A p$23 \in { "c1", "c2", "c3" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_9 == decision[p$23][1]
IN
prop_si_9 /= <<"None", (-1), (-1)>> => (prop_si_9)[1] \in { "v0", "v1" })
/\ (\A p$24 \in { "c1", "c2", "c3" }:
\E v$11 \in { "v0", "v1" }:
\E t$11 \in 0 .. 7:
\E pr$6 \in 0 .. 3:
\E dr$2 \in 0 .. 3:
decision[p$24] = <<<<v$11, t$11, pr$6>>, dr$2>>
=> (\E q$7 \in { "c1", "c2", "c3" }:
LET (*
@type: (() => Int);
*)
propRecvTime_si_2 == proposalReceptionTime[pr$6, q$7]
IN
beginRound[pr$6, q$7] <= propRecvTime_si_2
/\ beginRound[(pr$6 + 1), q$7] >= propRecvTime_si_2
/\ (propRecvTime_si_2 >= t$11 - 2
/\ propRecvTime_si_2 <= (t$11 + 2) + 2)))
/\ (\A r$31 \in 0 .. 3 \ {3}:
\A v$12 \in { "v0", "v1" }:
LET (*@type: (() => Str); *) p_si_25 == Proposer[r$31] IN
p_si_25 \in { "c1", "c2", "c3" }
=> (\E t$12 \in 0 .. 7:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_10 == <<v$12, t$12, r$31>>
IN
(\E msg$8 \in msgsPropose[r$31]:
msg$8["proposal"] = prop_si_10
/\ msg$8["src"] = p_si_25
/\ msg$8["validRound"] = -1)
/\ LET (*@type: (() => Int); *) tOffset_si_2 == (t$12 + 2) + 2 IN
[
r$32 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_4(a_si_7, b_si_7) == IF a$7 <= b$7 THEN a$7 ELSE b$7
IN
Min2$4, 7, {
beginRound[r$32, p$26]:
p$26 \in { "c1", "c2", "c3" }
})
][
r$31
]
<= t$12
/\ t$12
<= [
r$33 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_4(a_si_8, b_si_8) ==
IF a$8 >= b$8 THEN a$8 ELSE b$8
IN
Max2$4, (-1), {
beginRound[r$33, p$27]:
p$27 \in { "c1", "c2", "c3" }
})
][
r$31
]
/\ [
r$34 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_5(a_si_9, b_si_9) == IF a$9 >= b$9 THEN a$9 ELSE b$9
IN
Max2$5, (-1), {
beginRound[r$34, p$28]:
p$28 \in { "c1", "c2", "c3" }
})
][
r$31
]
<= tOffset_si_2
/\ tOffset_si_2
<= [
r$35 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_5(a_si_10, b_si_10) ==
IF a$10 <= b$10 THEN a$10 ELSE b$10
IN
Min2$5, 7, {
beginRound[r$35, p$29]:
p$29 \in { "c1", "c2", "c3" }
})
][
(r$31 + 1)
]
=> (\A q$8 \in { "c1", "c2", "c3" }:
LET (*
@type: (() => <<<<Str, Int, Int>>, Int>>);
*)
dq_si_2 == decision[q$8]
IN
dq_si_2 /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (dq_si_2)[1] = prop_si_10)))
(*
@type: (() => Bool);
*)
Init ==
round = [ p$10 \in { "c1", "c2", "c3" } |-> 0 ]
/\ localClock \in [{ "c1", "c2", "c3" } -> (2 .. 2 + 2)]
/\ realTime = 0
/\ step = [ p$11 \in { "c1", "c2", "c3" } |-> "PROPOSE" ]
/\ decision
= [ p$12 \in { "c1", "c2", "c3" } |-> <<<<"None", (-1), (-1)>>, (-1)>> ]
/\ lockedValue = [ p$13 \in { "c1", "c2", "c3" } |-> "None" ]
/\ lockedRound = [ p$14 \in { "c1", "c2", "c3" } |-> -1 ]
/\ validValue = [ p$15 \in { "c1", "c2", "c3" } |-> <<"None", (-1), (-1)>> ]
/\ validRound = [ p$16 \in { "c1", "c2", "c3" } |-> -1 ]
/\ ((TRUE
/\ (msgsPropose \in [(0 .. 3) -> Gen(5)]
/\ msgsPrevote \in [(0 .. 3) -> Gen(5)]
/\ msgsPrecommit \in [(0 .. 3) -> Gen(5)]
/\ ((\A r$43 \in 0 .. 3:
msgsPropose[r$43]
\subseteq [type: {"PROPOSAL"},
src: {"f4"},
round: 0 .. 3,
proposal:
({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]
/\ (\A m$29 \in msgsPropose[r$43]: r$43 = m$29["round"])))
/\ ((\A r$44 \in 0 .. 3:
msgsPrevote[r$44]
\subseteq [type: {"PREVOTE"},
src: {"f4"},
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$30 \in msgsPrevote[r$44]: r$44 = m$30["round"])))
/\ ((\A r$45 \in 0 .. 3:
msgsPrecommit[r$45]
\subseteq [type: {"PRECOMMIT"},
src: {"f4"},
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$31 \in msgsPrecommit[r$45]: r$45 = m$31["round"])))))
\/ (~TRUE
/\ msgsPropose = [ r$46 \in 0 .. 3 |-> {} ]
/\ msgsPrevote = [ r$47 \in 0 .. 3 |-> {} ]
/\ msgsPrecommit = [ r$48 \in 0 .. 3 |-> {} ]))
/\ proposalReceptionTime
= [ r_p$1 \in (0 .. 3) \X { "c1", "c2", "c3" } |-> -1 ]
/\ evidence = {}
/\ action = "Init"
/\ beginRound
= [
r_c$1 \in (0 .. 3) \X { "c1", "c2", "c3" } |->
IF r_c$1[1] = 0 THEN localClock[r_c$1[2]] ELSE 7
]
(*
@type: (() => Bool);
*)
Next ==
(realTime < 7
/\ (\E t$18 \in 0 .. 7:
t$18 > realTime
/\ realTime' = t$18
/\ localClock'
= [
p$30 \in { "c1", "c2", "c3" } |->
localClock[p$30] + t$18 - realTime
])
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>
/\ <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>'
= <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>
/\ beginRound' := beginRound)
/\ action' = "AdvanceRealTime")
\/ (~TRUE
/\ action' = "FaultyBroadcast"
/\ (\E r$49 \in 0 .. 3:
(\E msgs$4 \in SUBSET ([type: {"PROPOSAL"},
src: {"f4"},
round: {r$49},
proposal: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]):
msgsPropose'
= [
msgsPropose EXCEPT
![r$49] = msgsPropose[r$49] \union msgs$4
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$5 \in SUBSET ([type: {"PREVOTE"},
src: {"f4"},
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrevote'
= [
msgsPrevote EXCEPT
![r$49] = msgsPrevote[r$49] \union msgs$5
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$6 \in SUBSET ([type: {"PRECOMMIT"},
src: {"f4"},
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r$49] = msgsPrecommit[r$49] \union msgs$6
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))))
\/ ((\A p$31 \in { "c1", "c2", "c3" }:
\A q$9 \in { "c1", "c2", "c3" }:
p$31 /= q$9
=> (localClock[p$31] >= localClock[q$9]
/\ localClock[p$31] - localClock[q$9] < 2)
\/ (localClock[p$31] < localClock[q$9]
/\ localClock[q$9] - localClock[p$31] < 2))
/\ (\E p$17 \in { "c1", "c2", "c3" }:
LET (*@type: (() => Int); *) r_si_50 == round[p$17] IN
p$17 = Proposer[(r_si_50)]
/\ step[p$17] = "PROPOSE"
/\ (\A m$32 \in msgsPropose[(r_si_50)]: m$32["src"] /= p$17)
/\ (\E v$19 \in { "v0", "v1" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
proposal_si_3 ==
IF validValue[p$17] /= <<"None", (-1), (-1)>>
THEN validValue[p$17]
ELSE <<v$19, localClock[p$17], (r_si_50)>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
newMsg_si_18 ==
[type |-> "PROPOSAL",
src |-> p$17,
round |-> r_si_50,
proposal |-> proposal_si_3,
validRound |-> validRound[p$17]]
IN
msgsPropose'
= [
msgsPropose EXCEPT
![r_si_50] =
msgsPropose[(r_si_50)] \union {(newMsg_si_18)}
])
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "InsertProposal"
\/ (\E v$20 \in { "v0", "v1" } \union {"v2"}:
\E t$19 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_51 == round[p$17] IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_14 ==
[type |-> "PROPOSAL",
src |-> Proposer[round[p$17]],
round |-> round[p$17],
proposal |-> <<v$20, t$19, (r_si_51)>>,
validRound |-> -1]
IN
msg_si_14 \in msgsPropose[round[p$17]]
/\ proposalReceptionTime[(r_si_51), p$17] = -1
/\ proposalReceptionTime'
= [
proposalReceptionTime EXCEPT
![<<(r_si_51), p$17>>] = localClock[p$17]
]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence)
/\ beginRound' := beginRound
/\ action' = "ReceiveProposal")
\/ (\E v$21 \in { "v0", "v1" } \union {"v2"}:
\E t$20 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_52 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_15 == <<v$21, t$20, (r_si_52)>>
IN
step[p$17] = "PROPOSE"
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_15 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_52)],
round |-> r_si_52,
proposal |-> prop_si_15,
validRound |-> -1]
IN
evidence' = {(msg_si_15)} \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_5 ==
IF (proposalReceptionTime[(r_si_52), p$17] >= t$20 - 2
/\ proposalReceptionTime[(r_si_52), p$17]
<= (t$20 + 2) + 2)
/\ prop_si_15 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] = -1 \/ lockedValue[p$17] = v$21)
THEN prop_si_15
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_19 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_52,
id |-> mid_si_5]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_52] =
msgsPrevote[(r_si_52)] \union {(newMsg_si_19)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPropose")
\/ (\E v$22 \in { "v0", "v1" } \union {"v2"}:
\E t$21 \in 0 .. 7:
\E vr$7 \in 0 .. 3:
\E pr$9 \in 0 .. 3:
LET (*@type: (() => Int); *) r_si_53 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_16 == <<v$22, t$21, pr$9>>
IN
((step[p$17] = "PROPOSE" /\ 0 <= vr$7) /\ vr$7 < r_si_53)
/\ pr$9 <= vr$7
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_16 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_53)],
round |-> r_si_53,
proposal |-> prop_si_16,
validRound |-> vr$7]
IN
msg_si_16 \in msgsPropose[(r_si_53)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_9 ==
{ m$33 \in msgsPrevote[vr$7]: m$33["id"] = prop_si_16 }
IN
Cardinality((PV_si_9)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_9 \union {(msg_si_16)}) \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_6 ==
IF prop_si_16 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] <= vr$7
\/ lockedValue[p$17] = v$22)
THEN prop_si_16
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_20 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_53,
id |-> mid_si_6]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_53] =
msgsPrevote[(r_si_53)] \union {(newMsg_si_20)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInProposeAndPrevote")
\/ (step[p$17] = "PREVOTE"
/\ (\E MyEvidence$7 \in SUBSET (msgsPrevote[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Voters_si_3 == { m$34["src"]: m$34 \in MyEvidence$7 }
IN
Cardinality((Voters_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$7 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_21 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_21)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrevotesAny"))
\/ (\E v$23 \in { "v0", "v1" }:
\E t$22 \in 0 .. 7:
\E vr$8 \in 0 .. 3 \union {(-1)}:
LET (*@type: (() => Int); *) r_si_54 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_17 == <<v$23, t$22, (r_si_54)>>
IN
step[p$17] \in { "PREVOTE", "PRECOMMIT" }
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_17 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_54)],
round |-> r_si_54,
proposal |-> prop_si_17,
validRound |-> vr$8]
IN
msg_si_17 \in msgsPropose[(r_si_54)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_10 ==
{
m$35 \in msgsPrevote[(r_si_54)]:
m$35["id"] = prop_si_17
}
IN
Cardinality((PV_si_10)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_10 \union {(msg_si_17)}) \union evidence
/\ (IF step[p$17] = "PREVOTE"
THEN lockedValue' = [ lockedValue EXCEPT ![p$17] = v$23 ]
/\ lockedRound' = [ lockedRound EXCEPT ![p$17] = r_si_54 ]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_22 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> r_si_54,
id |-> prop_si_17]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r_si_54] =
msgsPrecommit[(r_si_54)] \union {(newMsg_si_22)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
ELSE lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ msgsPrecommit' := msgsPrecommit
/\ step' := step)
/\ validValue' = [ validValue EXCEPT ![p$17] = prop_si_17 ]
/\ validRound' = [ validRound EXCEPT ![p$17] = r_si_54 ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round /\ decision' := decision)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote")
\/ ((\E MyEvidence$8 \in SUBSET (msgsPrecommit[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Committers_si_3 == { m$36["src"]: m$36 \in MyEvidence$8 }
IN
Cardinality((Committers_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$8 \union evidence
/\ round[p$17] + 1 \in 0 .. 3
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = round[p$17] + 1 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<(round[p$17] + 1), p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrecommitsAny"))
\/ (decision[p$17] = <<<<"None", (-1), (-1)>>, (-1)>>
/\ (\E v$24 \in { "v0", "v1" }:
\E t$23 \in 0 .. 7:
\E r$55 \in 0 .. 3:
\E pr$10 \in 0 .. 3:
\E vr$9 \in 0 .. 3 \union {(-1)}:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_18 == <<v$24, t$23, pr$10>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_18 ==
[type |-> "PROPOSAL",
src |-> Proposer[r$55],
round |-> r$55,
proposal |-> prop_si_18,
validRound |-> vr$9]
IN
msg_si_18 \in msgsPropose[r$55]
/\ proposalReceptionTime[r$55, p$17] /= -1
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_11 ==
{
m$37 \in msgsPrecommit[r$55]:
m$37["id"] = prop_si_18
}
IN
Cardinality((PV_si_11)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_11 \union {(msg_si_18)}) \union evidence
/\ decision'
= [
decision EXCEPT
![p$17] = <<(prop_si_18), r$55>>
]
/\ step' = [ step EXCEPT ![p$17] = "DECIDED" ]
/\ <<localClock, realTime>>'
= <<localClock, realTime>>
/\ (round' := round
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "UponProposalInPrecommitNoDecision"))
\/ (step[p$17] = "PROPOSE"
/\ p$17 /= Proposer[round[p$17]]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_23 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![round[p$17]] =
msgsPrevote[round[p$17]] \union {(newMsg_si_23)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnTimeoutPropose")
\/ (step[p$17] = "PREVOTE"
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_12 ==
{
m$38 \in msgsPrevote[round[p$17]]:
m$38["id"] = <<"None", (-1), (-1)>>
}
IN
Cardinality((PV_si_12)) >= 2 * 1 + 1
/\ evidence' = PV_si_12 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_24 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_24)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnQuorumOfNilPrevotes")
\/ (\E r$56 \in 0 .. 3:
r$56 > round[p$17]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
RoundMsgs_si_3 ==
(msgsPropose[r$56] \union msgsPrevote[r$56])
\union msgsPrecommit[r$56]
IN
\E MyEvidence$9 \in SUBSET RoundMsgs_si_3:
LET (*
@type: (() => Set(Str));
*)
Faster_si_3 == { m$39["src"]: m$39 \in MyEvidence$9 }
IN
Cardinality((Faster_si_3)) >= 1 + 1
/\ evidence' = MyEvidence$9 \union evidence
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = r$56 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<r$56, p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnRoundCatchup")))
================================================================================

View File

@@ -0,0 +1,955 @@
--------------------------- MODULE 05_OutPrimingPass ---------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
CONSTANT
(*
@type: (Int -> Str);
*)
Proposer
VARIABLE
(*
@type: (Str -> <<<<Str, Int, Int>>, Int>>);
*)
decision
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrecommit
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
beginRound
VARIABLE
(*
@type: (Int -> Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
msgsPrevote
VARIABLE
(*
@type: Str;
*)
action
VARIABLE
(*
@type: (Str -> Int);
*)
lockedRound
VARIABLE
(*
@type: (Int -> Set([proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
msgsPropose
VARIABLE
(*
@type: (Str -> Int);
*)
validRound
VARIABLE
(*
@type: (Str -> Str);
*)
step
VARIABLE
(*
@type: (Str -> Str);
*)
lockedValue
VARIABLE
(*
@type: (Str -> <<Str, Int, Int>>);
*)
validValue
VARIABLE
(*
@type: Int;
*)
realTime
VARIABLE
(*
@type: (Str -> Int);
*)
round
VARIABLE
(*
@type: Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
evidence
VARIABLE
(*
@type: (<<Int, Str>> -> Int);
*)
proposalReceptionTime
VARIABLE
(*
@type: (Str -> Int);
*)
localClock
(*
@type: (() => Bool);
*)
CInit == Proposer \in [(0 .. 3) -> ({ "c1", "c2", "c3" } \union {"f4"})]
(*
@type: (() => Bool);
*)
Inv ==
(\A p$22 \in { "c1", "c2", "c3" }:
\A q$6 \in { "c1", "c2", "c3" }:
decision[p$22] /= <<<<"None", (-1), (-1)>>, (-1)>>
/\ decision[q$6] /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (\E v$10 \in { "v0", "v1" }:
\E t$10 \in 0 .. 7:
\E pr$5 \in 0 .. 3:
\E r1$3 \in 0 .. 3:
\E r2$3 \in 0 .. 3:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_8 == <<v$10, t$10, pr$5>>
IN
decision[p$22] = <<(prop_si_8), r1$3>>
/\ decision[q$6] = <<(prop_si_8), r2$3>>))
/\ (\A p$23 \in { "c1", "c2", "c3" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_9 == decision[p$23][1]
IN
prop_si_9 /= <<"None", (-1), (-1)>> => (prop_si_9)[1] \in { "v0", "v1" })
/\ (\A p$24 \in { "c1", "c2", "c3" }:
\E v$11 \in { "v0", "v1" }:
\E t$11 \in 0 .. 7:
\E pr$6 \in 0 .. 3:
\E dr$2 \in 0 .. 3:
decision[p$24] = <<<<v$11, t$11, pr$6>>, dr$2>>
=> (\E q$7 \in { "c1", "c2", "c3" }:
LET (*
@type: (() => Int);
*)
propRecvTime_si_2 == proposalReceptionTime[pr$6, q$7]
IN
beginRound[pr$6, q$7] <= propRecvTime_si_2
/\ beginRound[(pr$6 + 1), q$7] >= propRecvTime_si_2
/\ (propRecvTime_si_2 >= t$11 - 2
/\ propRecvTime_si_2 <= (t$11 + 2) + 2)))
/\ (\A r$31 \in 0 .. 3 \ {3}:
\A v$12 \in { "v0", "v1" }:
LET (*@type: (() => Str); *) p_si_25 == Proposer[r$31] IN
p_si_25 \in { "c1", "c2", "c3" }
=> (\E t$12 \in 0 .. 7:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_10 == <<v$12, t$12, r$31>>
IN
(\E msg$8 \in msgsPropose[r$31]:
msg$8["proposal"] = prop_si_10
/\ msg$8["src"] = p_si_25
/\ msg$8["validRound"] = -1)
/\ LET (*@type: (() => Int); *) tOffset_si_2 == (t$12 + 2) + 2 IN
[
r$32 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_4(a_si_7, b_si_7) == IF a$7 <= b$7 THEN a$7 ELSE b$7
IN
Min2$4, 7, {
beginRound[r$32, p$26]:
p$26 \in { "c1", "c2", "c3" }
})
][
r$31
]
<= t$12
/\ t$12
<= [
r$33 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_4(a_si_8, b_si_8) ==
IF a$8 >= b$8 THEN a$8 ELSE b$8
IN
Max2$4, (-1), {
beginRound[r$33, p$27]:
p$27 \in { "c1", "c2", "c3" }
})
][
r$31
]
/\ [
r$34 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Max2_si_5(a_si_9, b_si_9) == IF a$9 >= b$9 THEN a$9 ELSE b$9
IN
Max2$5, (-1), {
beginRound[r$34, p$28]:
p$28 \in { "c1", "c2", "c3" }
})
][
r$31
]
<= tOffset_si_2
/\ tOffset_si_2
<= [
r$35 \in 0 .. 3 |->
ApaFoldSet(LET (*
@type: ((Int, Int) => Int);
*)
Min2_si_5(a_si_10, b_si_10) ==
IF a$10 <= b$10 THEN a$10 ELSE b$10
IN
Min2$5, 7, {
beginRound[r$35, p$29]:
p$29 \in { "c1", "c2", "c3" }
})
][
(r$31 + 1)
]
=> (\A q$8 \in { "c1", "c2", "c3" }:
LET (*
@type: (() => <<<<Str, Int, Int>>, Int>>);
*)
dq_si_2 == decision[q$8]
IN
dq_si_2 /= <<<<"None", (-1), (-1)>>, (-1)>>
=> (dq_si_2)[1] = prop_si_10)))
(*
@type: (() => Bool);
*)
Init ==
round = [ p$10 \in { "c1", "c2", "c3" } |-> 0 ]
/\ localClock \in [{ "c1", "c2", "c3" } -> (2 .. 2 + 2)]
/\ realTime = 0
/\ step = [ p$11 \in { "c1", "c2", "c3" } |-> "PROPOSE" ]
/\ decision
= [ p$12 \in { "c1", "c2", "c3" } |-> <<<<"None", (-1), (-1)>>, (-1)>> ]
/\ lockedValue = [ p$13 \in { "c1", "c2", "c3" } |-> "None" ]
/\ lockedRound = [ p$14 \in { "c1", "c2", "c3" } |-> -1 ]
/\ validValue = [ p$15 \in { "c1", "c2", "c3" } |-> <<"None", (-1), (-1)>> ]
/\ validRound = [ p$16 \in { "c1", "c2", "c3" } |-> -1 ]
/\ ((TRUE
/\ (msgsPropose \in [(0 .. 3) -> Gen(5)]
/\ msgsPrevote \in [(0 .. 3) -> Gen(5)]
/\ msgsPrecommit \in [(0 .. 3) -> Gen(5)]
/\ ((\A r$43 \in 0 .. 3:
msgsPropose[r$43]
\subseteq [type: {"PROPOSAL"},
src: {"f4"},
round: 0 .. 3,
proposal:
({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]
/\ (\A m$29 \in msgsPropose[r$43]: r$43 = m$29["round"])))
/\ ((\A r$44 \in 0 .. 3:
msgsPrevote[r$44]
\subseteq [type: {"PREVOTE"},
src: {"f4"},
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$30 \in msgsPrevote[r$44]: r$44 = m$30["round"])))
/\ ((\A r$45 \in 0 .. 3:
msgsPrecommit[r$45]
\subseteq [type: {"PRECOMMIT"},
src: {"f4"},
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$31 \in msgsPrecommit[r$45]: r$45 = m$31["round"])))))
\/ (~TRUE
/\ msgsPropose = [ r$46 \in 0 .. 3 |-> {} ]
/\ msgsPrevote = [ r$47 \in 0 .. 3 |-> {} ]
/\ msgsPrecommit = [ r$48 \in 0 .. 3 |-> {} ]))
/\ proposalReceptionTime
= [ r_p$1 \in (0 .. 3) \X { "c1", "c2", "c3" } |-> -1 ]
/\ evidence = {}
/\ action = "Init"
/\ beginRound
= [
r_c$1 \in (0 .. 3) \X { "c1", "c2", "c3" } |->
IF r_c$1[1] = 0 THEN localClock[r_c$1[2]] ELSE 7
]
(*
@type: (() => Bool);
*)
Next ==
(realTime < 7
/\ (\E t$18 \in 0 .. 7:
t$18 > realTime
/\ realTime' = t$18
/\ localClock'
= [
p$30 \in { "c1", "c2", "c3" } |->
localClock[p$30] + t$18 - realTime
])
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>
/\ <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>'
= <<
msgsPropose, msgsPrevote, msgsPrecommit, evidence, proposalReceptionTime
>>
/\ beginRound' := beginRound)
/\ action' = "AdvanceRealTime")
\/ (~TRUE
/\ action' = "FaultyBroadcast"
/\ (\E r$49 \in 0 .. 3:
(\E msgs$4 \in SUBSET ([type: {"PROPOSAL"},
src: {"f4"},
round: {r$49},
proposal: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]):
msgsPropose'
= [
msgsPropose EXCEPT
![r$49] = msgsPropose[r$49] \union msgs$4
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$5 \in SUBSET ([type: {"PREVOTE"},
src: {"f4"},
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrevote'
= [
msgsPrevote EXCEPT
![r$49] = msgsPrevote[r$49] \union msgs$5
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))
\/ (\E msgs$6 \in SUBSET ([type: {"PRECOMMIT"},
src: {"f4"},
round: {r$49},
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]):
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r$49] = msgsPrecommit[r$49] \union msgs$6
]
/\ (<<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime))))
\/ ((\A p$31 \in { "c1", "c2", "c3" }:
\A q$9 \in { "c1", "c2", "c3" }:
p$31 /= q$9
=> (localClock[p$31] >= localClock[q$9]
/\ localClock[p$31] - localClock[q$9] < 2)
\/ (localClock[p$31] < localClock[q$9]
/\ localClock[q$9] - localClock[p$31] < 2))
/\ (\E p$17 \in { "c1", "c2", "c3" }:
LET (*@type: (() => Int); *) r_si_50 == round[p$17] IN
p$17 = Proposer[(r_si_50)]
/\ step[p$17] = "PROPOSE"
/\ (\A m$32 \in msgsPropose[(r_si_50)]: m$32["src"] /= p$17)
/\ (\E v$19 \in { "v0", "v1" }:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
proposal_si_3 ==
IF validValue[p$17] /= <<"None", (-1), (-1)>>
THEN validValue[p$17]
ELSE <<v$19, localClock[p$17], (r_si_50)>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
newMsg_si_18 ==
[type |-> "PROPOSAL",
src |-> p$17,
round |-> r_si_50,
proposal |-> proposal_si_3,
validRound |-> validRound[p$17]]
IN
msgsPropose'
= [
msgsPropose EXCEPT
![r_si_50] =
msgsPropose[(r_si_50)] \union {(newMsg_si_18)}
])
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue, validRound
>>)
/\ (msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "InsertProposal"
\/ (\E v$20 \in { "v0", "v1" } \union {"v2"}:
\E t$19 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_51 == round[p$17] IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_14 ==
[type |-> "PROPOSAL",
src |-> Proposer[round[p$17]],
round |-> round[p$17],
proposal |-> <<v$20, t$19, (r_si_51)>>,
validRound |-> -1]
IN
msg_si_14 \in msgsPropose[round[p$17]]
/\ proposalReceptionTime[(r_si_51), p$17] = -1
/\ proposalReceptionTime'
= [
proposalReceptionTime EXCEPT
![<<(r_si_51), p$17>>] = localClock[p$17]
]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>'
= <<
round, step, decision, lockedValue, lockedRound, validValue,
validRound
>>)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence)
/\ beginRound' := beginRound
/\ action' = "ReceiveProposal")
\/ (\E v$21 \in { "v0", "v1" } \union {"v2"}:
\E t$20 \in 0 .. 7:
LET (*@type: (() => Int); *) r_si_52 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_15 == <<v$21, t$20, (r_si_52)>>
IN
step[p$17] = "PROPOSE"
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_15 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_52)],
round |-> r_si_52,
proposal |-> prop_si_15,
validRound |-> -1]
IN
evidence' = {(msg_si_15)} \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_5 ==
IF (proposalReceptionTime[(r_si_52), p$17] >= t$20 - 2
/\ proposalReceptionTime[(r_si_52), p$17]
<= (t$20 + 2) + 2)
/\ prop_si_15 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] = -1 \/ lockedValue[p$17] = v$21)
THEN prop_si_15
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_19 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_52,
id |-> mid_si_5]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_52] =
msgsPrevote[(r_si_52)] \union {(newMsg_si_19)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPropose")
\/ (\E v$22 \in { "v0", "v1" } \union {"v2"}:
\E t$21 \in 0 .. 7:
\E vr$7 \in 0 .. 3:
\E pr$9 \in 0 .. 3:
LET (*@type: (() => Int); *) r_si_53 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_16 == <<v$22, t$21, pr$9>>
IN
((step[p$17] = "PROPOSE" /\ 0 <= vr$7) /\ vr$7 < r_si_53)
/\ pr$9 <= vr$7
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_16 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_53)],
round |-> r_si_53,
proposal |-> prop_si_16,
validRound |-> vr$7]
IN
msg_si_16 \in msgsPropose[(r_si_53)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_9 ==
{ m$33 \in msgsPrevote[vr$7]: m$33["id"] = prop_si_16 }
IN
Cardinality((PV_si_9)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_9 \union {(msg_si_16)}) \union evidence
/\ LET (*
@type: (() => <<Str, Int, Int>>);
*)
mid_si_6 ==
IF prop_si_16 \in { "v0", "v1" } \X (2 .. 7) \X (0 .. 3)
/\ (lockedRound[p$17] <= vr$7
\/ lockedValue[p$17] = v$22)
THEN prop_si_16
ELSE <<"None", (-1), (-1)>>
IN
LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_20 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> r_si_53,
id |-> mid_si_6]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![r_si_53] =
msgsPrevote[(r_si_53)] \union {(newMsg_si_20)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInProposeAndPrevote")
\/ (step[p$17] = "PREVOTE"
/\ (\E MyEvidence$7 \in SUBSET (msgsPrevote[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Voters_si_3 == { m$34["src"]: m$34 \in MyEvidence$7 }
IN
Cardinality((Voters_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$7 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_21 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_21)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrevotesAny"))
\/ (\E v$23 \in { "v0", "v1" }:
\E t$22 \in 0 .. 7:
\E vr$8 \in 0 .. 3 \union {(-1)}:
LET (*@type: (() => Int); *) r_si_54 == round[p$17] IN
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_17 == <<v$23, t$22, (r_si_54)>>
IN
step[p$17] \in { "PREVOTE", "PRECOMMIT" }
/\ LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_17 ==
[type |-> "PROPOSAL",
src |-> Proposer[(r_si_54)],
round |-> r_si_54,
proposal |-> prop_si_17,
validRound |-> vr$8]
IN
msg_si_17 \in msgsPropose[(r_si_54)]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_10 ==
{
m$35 \in msgsPrevote[(r_si_54)]:
m$35["id"] = prop_si_17
}
IN
Cardinality((PV_si_10)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_10 \union {(msg_si_17)}) \union evidence
/\ (IF step[p$17] = "PREVOTE"
THEN lockedValue' = [ lockedValue EXCEPT ![p$17] = v$23 ]
/\ lockedRound' = [ lockedRound EXCEPT ![p$17] = r_si_54 ]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_22 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> r_si_54,
id |-> prop_si_17]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![r_si_54] =
msgsPrecommit[(r_si_54)] \union {(newMsg_si_22)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
ELSE lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ msgsPrecommit' := msgsPrecommit
/\ step' := step)
/\ validValue' = [ validValue EXCEPT ![p$17] = prop_si_17 ]
/\ validRound' = [ validRound EXCEPT ![p$17] = r_si_54 ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round /\ decision' := decision)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote")
\/ ((\E MyEvidence$8 \in SUBSET (msgsPrecommit[round[p$17]]):
LET (*
@type: (() => Set(Str));
*)
Committers_si_3 == { m$36["src"]: m$36 \in MyEvidence$8 }
IN
Cardinality((Committers_si_3)) >= 2 * 1 + 1
/\ evidence' = MyEvidence$8 \union evidence
/\ round[p$17] + 1 \in 0 .. 3
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = round[p$17] + 1 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<(round[p$17] + 1), p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "UponQuorumOfPrecommitsAny"))
\/ (decision[p$17] = <<<<"None", (-1), (-1)>>, (-1)>>
/\ (\E v$24 \in { "v0", "v1" }:
\E t$23 \in 0 .. 7:
\E r$55 \in 0 .. 3:
\E pr$10 \in 0 .. 3:
\E vr$9 \in 0 .. 3 \union {(-1)}:
LET (*
@type: (() => <<Str, Int, Int>>);
*)
prop_si_18 == <<v$24, t$23, pr$10>>
IN
LET (*
@type: (() => [proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]);
*)
msg_si_18 ==
[type |-> "PROPOSAL",
src |-> Proposer[r$55],
round |-> r$55,
proposal |-> prop_si_18,
validRound |-> vr$9]
IN
msg_si_18 \in msgsPropose[r$55]
/\ proposalReceptionTime[r$55, p$17] /= -1
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_11 ==
{
m$37 \in msgsPrecommit[r$55]:
m$37["id"] = prop_si_18
}
IN
Cardinality((PV_si_11)) >= 2 * 1 + 1
/\ evidence'
= (PV_si_11 \union {(msg_si_18)}) \union evidence
/\ decision'
= [
decision EXCEPT
![p$17] = <<(prop_si_18), r$55>>
]
/\ step' = [ step EXCEPT ![p$17] = "DECIDED" ]
/\ <<localClock, realTime>>'
= <<localClock, realTime>>
/\ (round' := round
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ beginRound' := beginRound
/\ action' = "UponProposalInPrecommitNoDecision"))
\/ (step[p$17] = "PROPOSE"
/\ p$17 /= Proposer[round[p$17]]
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_23 ==
[type |-> "PREVOTE",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrevote'
= [
msgsPrevote EXCEPT
![round[p$17]] =
msgsPrevote[round[p$17]] \union {(newMsg_si_23)}
]
/\ step' = [ step EXCEPT ![p$17] = "PREVOTE" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrecommit' := msgsPrecommit
/\ evidence' := evidence
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnTimeoutPropose")
\/ (step[p$17] = "PREVOTE"
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]));
*)
PV_si_12 ==
{
m$38 \in msgsPrevote[round[p$17]]:
m$38["id"] = <<"None", (-1), (-1)>>
}
IN
Cardinality((PV_si_12)) >= 2 * 1 + 1
/\ evidence' = PV_si_12 \union evidence
/\ LET (*
@type: (() => [id: <<Str, Int, Int>>, round: Int, src: Str, type: Str]);
*)
newMsg_si_24 ==
[type |-> "PRECOMMIT",
src |-> p$17,
round |-> round[p$17],
id |-> <<"None", (-1), (-1)>>]
IN
msgsPrecommit'
= [
msgsPrecommit EXCEPT
![round[p$17]] =
msgsPrecommit[round[p$17]] \union {(newMsg_si_24)}
]
/\ step' = [ step EXCEPT ![p$17] = "PRECOMMIT" ]
/\ (<<localClock, realTime>>' = <<localClock, realTime>>
/\ beginRound' := beginRound)
/\ (round' := round
/\ decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnQuorumOfNilPrevotes")
\/ (\E r$56 \in 0 .. 3:
r$56 > round[p$17]
/\ LET (*
@type: (() => Set([id: <<Str, Int, Int>>, proposal: <<Str, Int, Int>>, round: Int, src: Str, type: Str, validRound: Int]));
*)
RoundMsgs_si_3 ==
(msgsPropose[r$56] \union msgsPrevote[r$56])
\union msgsPrecommit[r$56]
IN
\E MyEvidence$9 \in SUBSET RoundMsgs_si_3:
LET (*
@type: (() => Set(Str));
*)
Faster_si_3 == { m$39["src"]: m$39 \in MyEvidence$9 }
IN
Cardinality((Faster_si_3)) >= 1 + 1
/\ evidence' = MyEvidence$9 \union evidence
/\ (step[p$17] /= "DECIDED"
/\ round' = [ round EXCEPT ![p$17] = r$56 ]
/\ step' = [ step EXCEPT ![p$17] = "PROPOSE" ]
/\ beginRound'
= [
beginRound EXCEPT
![<<r$56, p$17>>] = localClock[p$17]
])
/\ <<localClock, realTime>>' = <<localClock, realTime>>
/\ (decision' := decision
/\ lockedValue' := lockedValue
/\ lockedRound' := lockedRound
/\ validValue' := validValue
/\ validRound' := validRound)
/\ (msgsPropose' := msgsPropose
/\ msgsPrevote' := msgsPrevote
/\ msgsPrecommit' := msgsPrecommit
/\ proposalReceptionTime' := proposalReceptionTime)
/\ action' = "OnRoundCatchup")))
CInitPrimed == Proposer' \in [(0 .. 3) -> ({ "c1", "c2", "c3" } \union {"f4"})]
InitPrimed ==
round' = [ p$10 \in { "c1", "c2", "c3" } |-> 0 ]
/\ localClock' \in [{ "c1", "c2", "c3" } -> (2 .. 2 + 2)]
/\ realTime' = 0
/\ step' = [ p$11 \in { "c1", "c2", "c3" } |-> "PROPOSE" ]
/\ decision'
= [ p$12 \in { "c1", "c2", "c3" } |-> <<<<"None", (-1), (-1)>>, (-1)>> ]
/\ lockedValue' = [ p$13 \in { "c1", "c2", "c3" } |-> "None" ]
/\ lockedRound' = [ p$14 \in { "c1", "c2", "c3" } |-> -1 ]
/\ validValue'
= [ p$15 \in { "c1", "c2", "c3" } |-> <<"None", (-1), (-1)>> ]
/\ validRound' = [ p$16 \in { "c1", "c2", "c3" } |-> -1 ]
/\ ((TRUE
/\ (msgsPropose' \in [(0 .. 3) -> Gen(5)]
/\ msgsPrevote' \in [(0 .. 3) -> Gen(5)]
/\ msgsPrecommit' \in [(0 .. 3) -> Gen(5)]
/\ ((\A r$43 \in 0 .. 3:
msgsPropose'[r$43]
\subseteq [type: {"PROPOSAL"},
src: {"f4"},
round: 0 .. 3,
proposal:
({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3),
validRound: 0 .. 3 \union {(-1)}]
/\ (\A m$29 \in msgsPropose'[r$43]: r$43 = m$29["round"])))
/\ ((\A r$44 \in 0 .. 3:
msgsPrevote'[r$44]
\subseteq [type: {"PREVOTE"},
src: {"f4"},
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$30 \in msgsPrevote'[r$44]: r$44 = m$30["round"])))
/\ ((\A r$45 \in 0 .. 3:
msgsPrecommit'[r$45]
\subseteq [type: {"PRECOMMIT"},
src: {"f4"},
round: 0 .. 3,
id: ({ "v0", "v1" } \union {"v2"}) \X (0 .. 7) \X (0 .. 3)]
/\ (\A m$31 \in msgsPrecommit'[r$45]: r$45 = m$31["round"])))))
\/ (~TRUE
/\ msgsPropose' = [ r$46 \in 0 .. 3 |-> {} ]
/\ msgsPrevote' = [ r$47 \in 0 .. 3 |-> {} ]
/\ msgsPrecommit' = [ r$48 \in 0 .. 3 |-> {} ]))
/\ proposalReceptionTime'
= [ r_p$1 \in (0 .. 3) \X { "c1", "c2", "c3" } |-> -1 ]
/\ evidence' = {}
/\ action' = "Init"
/\ beginRound'
= [
r_c$1 \in (0 .. 3) \X { "c1", "c2", "c3" } |->
IF r_c$1[1] = 0 THEN localClock'[r_c$1[2]] ELSE 7
]
================================================================================

View File

@@ -0,0 +1,5 @@
Logging is disabled (Z3SolverContext.debug = false). Activate with --debug.
;; sat.random_seed = 0
;; smt.random_seed = 0
;; fp.spacer.random_seed = 0
;; sls.random_seed = 0

View File

@@ -0,0 +1 @@
check --length=8 --inv=Inv --cinit=CInit --discard-disabled=false MC_PBT_3C_1F.tla

View File

@@ -0,0 +1,34 @@
Architecture: x86_64
CPU op-mode(s): 32-bit, 64-bit
Byte Order: Little Endian
Address sizes: 40 bits physical, 48 bits virtual
CPU(s): 4
On-line CPU(s) list: 0-3
Thread(s) per core: 1
Core(s) per socket: 4
Socket(s): 1
NUMA node(s): 1
Vendor ID: GenuineIntel
CPU family: 6
Model: 85
Model name: Intel(R) Xeon(R) Gold 6248 CPU @ 2.50GHz
Stepping: 7
CPU MHz: 2494.140
BogoMIPS: 4988.28
Virtualization: VT-x
Hypervisor vendor: KVM
Virtualization type: full
L1d cache: 128 KiB
L1i cache: 128 KiB
L2 cache: 16 MiB
NUMA node0 CPU(s): 0-3
Vulnerability Itlb multihit: KVM: Mitigation: Split huge pages
Vulnerability L1tf: Not affected
Vulnerability Mds: Not affected
Vulnerability Meltdown: Not affected
Vulnerability Spec store bypass: Mitigation; Speculative Store Bypass disabled via prctl and seccomp
Vulnerability Spectre v1: Mitigation; usercopy/swapgs barriers and __user pointer sanitization
Vulnerability Spectre v2: Mitigation; Enhanced IBRS, IBPB conditional, RSB filling
Vulnerability Srbds: Not affected
Vulnerability Tsx async abort: Not affected
Flags: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush mmx fxsr sse sse2 ht syscall nx pdpe1gb rdtscp lm constant_tsc arch_perfmon rep_good nopl cpuid tsc_known_freq pni pclmulqdq vmx ssse3 fma cx16 pcid sse4_1 sse4_2 x2apic movbe popcnt tsc_deadline_timer aes xsave avx f16c rdrand hypervisor lahf_lm abm 3dnowprefetch cpuid_fault invpcid_single ssbd ibrs ibpb ibrs_enhanced tpr_shadow vnmi flexpriority ept vpid ept_ad fsgsbase bmi1 avx2 smep bmi2 erms invpcid avx512f avx512dq rdseed adx smap clflushopt clwb avx512cd avx512bw avx512vl xsaveopt xsavec xgetbv1 pku ospke avx512_vnni arch_capabilities

View File

@@ -0,0 +1,9 @@
# Experiment Log
This file summarizes the history of Apalache experiments for the PBTS specification.
| Date | Commit | Command | Runtime [h:min:s] | Machine | Notes |
|---|---|---|---|---|---|
| May 11, 2022 | cd48156f662af8fc325a6478dfa34de6be0e36c8 | [run.txt](./experiment_data/May2022/MC_PBT_3C_1F.tla/run.txt) | 74:39:2 | [machine.txt](./experiment_data/May2022/machine.txt) | No invariant violation in 8 steps |
| May 16, 2022 | cd48156f662af8fc325a6478dfa34de6be0e36c8 | [run.txt](./experiment_data/May2022/MC_PBT_2C_2F.tla/run.txt) | 48:31:29 | [machine.txt](./experiment_data/May2022/machine.txt) | [Counterexample](experiment_data/May2022/MC_PBT_2C_2F.tla/counterexample.tla) found (expected) |

View File

@@ -0,0 +1,37 @@
# How to run tests
The script `runApalache.sh` runs Apalache against one of the model files in this repository. This document describes how to use it.
1. Get Apalache, by following [these](https://apalache.informal.systems/docs/apalache/installation/index.html) instructions. Summarized:
1. `git clone https://github.com/informalsystems/apalache.git`
2. `make package`
2. Define an environment variable `APALACHE_HOME` and set it to the directory where you cloned the repository (resp. unpacked the prebuilt release). `$APALACHE_HOME/bin/apalache-mc` should point to the run script.
3. Call `runApalache.sh CMD N CM DD` where:
1. `CMD` is the command. Either "check" or "typecheck". Default: "typecheck"
2. `N` is the number of steps if `CMD=check`. Ignored if `CMD=typecheck`. Default: 10
3. `MC` is a Boolean flag that controls whether the model cehcked has a majoricty of correct processes. Default: true
4. `DD` is a Boolean flag that controls Apalache's `--discard-disabled` flag (See [here](https://apalache.informal.systems/docs/apalache/running.html)). Ignored if `CMD=typecheck`. Default: false
The results will be written to `_apalache-out` (see the [Apalache documentation](https://apalache.informal.systems/docs/adr/009adr-outputs.html)).
Example:
```sh
runApalache.sh check 2
```
Checks 2 steps of `MC_PBT_3C_1F.tla` and
```sh
runApalache.sh check 10 false
```
Checks 10 steps of `MC_PBT_2C_2F.tla`
# Updating the experiments log
After running a particularly significant test, copy the raw outputs from
`_apalache-out` to `experiment_data` and update `experiment_log.md` accordingly.
See `experiment_data/May2022` for a suggested directory layout.
Make sure to copy at least the `detailed.log` and `run.txt` files, as well as any counterexample files, if present.

View File

@@ -0,0 +1,37 @@
#!/usr/bin/env bash
set -euo pipefail
# Works in all cases except running from jar on Windows
EXE=$APALACHE_HOME/bin/apalache-mc
CMD=${1:-typecheck}
N=${2:-10}
MC=${3:-true}
DD=${4:-false}
SCRIPT_DIR=$( cd -- "$( dirname -- "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )
CFG=$SCRIPT_DIR/.apalache.cfg
if [[ $1 == "check" ]]; then
FLAGS="--length=$N --inv=Inv --cinit=CInit --discard-disabled=$DD"
else
FLAGS=""
fi
if ! [[ -f "$CFG" ]]; then
echo "out-dir: \"$SCRIPT_DIR/_apalache-out\"" >> $CFG
echo "write-intermediate: true" >> $CFG
fi
if [[ "$MC" = false ]]; then
# Run 2c2f
$EXE $CMD $FLAGS MC_PBT_2C_2F.tla
else
# Run 3c1f
$EXE $CMD $FLAGS MC_PBT_3C_1F.tla
fi

View File

@@ -261,7 +261,7 @@ This specification describes the changes needed to be done to the Tendermint con
[proposertla]: ../tla/TendermintPBT_001_draft.tla
[bfttime]: ../../bft-time.md
[bfttime]: ../bft-time.md
[tlatender]: https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md
[lcspec]: ../../light-client/
[arXiv]: https://arxiv.org/abs/1807.04938

View File

@@ -14,7 +14,7 @@ Specification of the Tendermint consensus protocol.
- [Consensus Paper](./consensus-paper) - Latex paper on
[arxiv](https://arxiv.org/abs/1807.04938) describing the
core Tendermint consensus state machine with proofs of safety and termination.
- [BFT Time](./bft-time.md) - How the timestamp in a Tendermint
- [Block Time](./time.md) - How the Time field in a Tendermint
block header is computed in a Byzantine Fault Tolerant manner
- [Creating Proposal](./creating-proposal.md) - How a proposer
creates a block proposal for consensus

51
spec/consensus/time.md Normal file
View File

@@ -0,0 +1,51 @@
---
order: 2
---
# Block Time
Tendermint provides a deterministic, Byzantine fault-tolerant, source of time,
with bounded relation with the real time.
Time in Tendermint is defined by the `Time` field present in the header of
committed blocks, which satisfies the following properties:
- **Monotonicity**: `Time` is monotonically increasing. That is,
given a header `H1` of a block at height `h1`
and a header `H2` of a block at height `h2 > h1`,
it is guaranteed that `H1.Time < H2.Time`.
- **Time-validity**: the `Time` of a block was considered valid, according with the
[timely][pbts_timely] predicate, by at least one correct validator. This
means that correct validators have attested that the block `Time` is compatible
with the real time at which the block was produced.
The evaluation of the `timely` predicates involves comparing the `Time`
assigned to the block by its proposer with the local time at which a validator
receives the proposed block.
If the block Time and the block receive time are within the same *time window*,
the validator accepts the proposed block; otherwise, the block is rejected.
The *time window* boundaries are defined by two [consensus parameters][parameters]:
- `Precision`: the acceptable upper-bound of clock drift among all the
validators on a Tendermint network. More precisely, the maximum acceptable
difference on the time values simultaneous read by any two correct validators
from their local clocks.
- `MessageDelay`: the maximum acceptable end-to-end delay for delivering a
`Proposal` message to all correct validators.
This is a fixed-size message broadcast by the proposer of block that
includes the proposed block unique `BlockID` and `Time`.
Validators are therefore assumed to be equipped with **synchronized clocks**.
The `Precision` parameter defines the worst-case precision achieved by the
adopted clock synchronization mechanism.
For the sake of time validity, this parameter essentially restricts how much
"in the future" a block Time can be, while the `MessageDelay` parameter mainly
restricts how much "in the past" a block Time can be.
For additional information on how block Times are produced and validated,
refer to the Proposer-Based TimeStamps (PBTS) [spec][pbts].
[pbts]: ./proposer-based-timestamp/README.md
[pbts_timely]: ./proposer-based-timestamp/pbts-sysmodel_002_draft.md#pbts-timely0
[parameters]: ../abci/apps.md#consensus-parameters