Skip to content

ZOOKEEPER-4903: An Inconsistency of `lastProcessed` variable in Spec and Impl #2232

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

fwhdzh wants to merge 1 commit into apache:master

from fwhdzh:ZK-4903

+1 −1

Open

ZOOKEEPER-4903: An Inconsistency of `lastProcessed` variable in Spec and Impl #2232

Changes from all commits

Commits

Show all changes

Select commit

ZOOKEEPER-4903: An Inconsistency of `lastProcessed` variable in Spec ...

fwhdzh Mar 7, 2025

File filter

Filter by extension

Conversations

Jump to

Jump to file

Failed to load files.

Loading

Diff view

Diff view

2 changes: 1 addition & 1 deletion zookeeper-specifications/system-spec/zk-3.7/ZkV3_7_0.tla

Show comments View file Open in desktop

Original file line number	Diff line number	Diff line change
Expand Up		@@ -1279,7 +1279,7 @@ WriteToTxnLog(i) == IF \/ connectInfo[i].syncMode = DIFF

		\* See lastProposed in Leader for details.
		LastProposed(i) == IF Len(history[i]) = 0 THEN [ index \|-> 0,
	zxid \|-> <<0, 0>> ]
	zxid \|-> <<Maximum({tempMaxEpoch[i], 0}), 0>> ]
		ELSE
		LET lastIndex == Len(history[i])
		entry == history[i][lastIndex]
Expand Down