|
|
|---|
|
|
|
|---|
Transitions for round advancement.
Here we define the system state changes caused by
This just increments the round number of a 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.