vsr-tlaplus
vsr-tlaplus copied to clipboard
Do not update view number in SendGetState
As we previously discussed, the lack of details in the VR paper leaves some implementation details open.
The differences in my interpretation of the state transfer are:
- The
rep_last_normal_view
should not be updated when sending theGetState
here: https://github.com/Vanlightly/vsr-tlaplus/blob/main/vsr-revisited/paper/VSR.tla#L509 - The
view_number
in theGetState
message should berep_last_normal_view
here: https://github.com/Vanlightly/vsr-tlaplus/blob/main/vsr-revisited/paper/VSR.tla#L511