Skip to content

Commit 893a0ed

Browse files
committed
Add proposed fix for desync bug elastic#3
1 parent 33cbeda commit 893a0ed

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

ReplicaEngine/tla/ReplicaEngine.tla

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -381,6 +381,13 @@ begin
381381
versionMap_entry := [ type |-> UPDATE, seqno |-> req.seqno ];
382382
else
383383
versionMap_isUnsafe := TRUE;
384+
385+
if /\ versionMap_entry /= NULL
386+
/\ versionMap_entry.type = DELETE
387+
/\ versionMap_entry.seqno < req.seqno
388+
then
389+
versionMap_entry := NULL; \* Desync bug #3 (no PR number yet)
390+
end if;
384391
end if;
385392
end if;
386393

0 commit comments

Comments
 (0)