ZOOKEEPER-4892: Keep self vote in sync in FastLeaderElection TLA receiveVotes

[arup-chauhan]

Description

This PR is the first incremental change for ZOOKEEPER-4892.

Scope is intentionally limited to FastLeaderElection TLA vote-state synchronization.
When a server updates its proposal in LOOKING flow, its self entry in receiveVotes[i][i] must reflect the same current vote. I have not changed the Java runtime code and change is limited to TLA model consistency for self-vote tracking.

This is PR-1 of a planned 2-PR sequence for ZOOKEEPER-4892. PR-2 will cover quorum vote-set/counting alignment (VoteSet/HasQuorums).

Changes

• Updated RvPut(...) in zookeeper-specifications/system-spec/zk-3.7/FastLeaderElection.tla:
  • synchronizes receiveVotes[i][i] with currentVote'[i]
  • keeps self round/state/version aligned during receive-vote updates
• Updated RvClearAndPut(...):
  • explicitly sets self entry (v = i) to currentVote'[i]
  • keeps existing behavior for source vote insertion and reset of other entries

Validation

• mvn -q -DskipTests install
• mvn -q -pl zookeeper-server -DskipTests compile
• TLC notes:
  • Spec parses and semantically processes.
  • Existing model currently has an unbounded CHOOSE at NullPoint in base file, which blocks full BFS model checking.
  • A temporary local bounded-NullPoint run was used to complete TLC simulation sanity.