|
|
|---|
|
|
|
|---|
Transitions for round advancement.
Here we define the system state transitions
caused by
A round advancement event involves just one correct validator.
This just increments the round number of the validator by one. The round advancement logic in AleoBFT is more complex, but our simple model suffices for many properties of interest, which, if proved for our model with the simpler round advancement logic, also hold in a model with a more complex round advancement logic, whose possible behaviors are a subset of the ones of this model with simple round advancement logic.
A round advancement event does not involve the network.