vsr-tlaplus icon indicating copy to clipboard operation
vsr-tlaplus copied to clipboard

Do not update view number in SendGetState

Open haraldng opened this issue 2 years ago • 0 comments

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:

  1. The rep_last_normal_view should not be updated when sending the GetState here: https://github.com/Vanlightly/vsr-tlaplus/blob/main/vsr-revisited/paper/VSR.tla#L509
  2. The view_number in the GetState message should be rep_last_normal_view here: https://github.com/Vanlightly/vsr-tlaplus/blob/main/vsr-revisited/paper/VSR.tla#L511

haraldng avatar Nov 28 '22 20:11 haraldng