Skip to content
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

Jump to bottom

Revise TLA spec. #4

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Revise TLA spec. #4

wants to merge 1 commit into from

Conversation

jinlmsft
Copy link

The following revision is made.

  1. The clientRequests become a variable, which uniquely identified each request received by server.
  2. Only valid message is evaluated, to reduce state space.
  3. Add test to see if there are more than one Leader per term in the cluster.
  4. Add test to see if the committedLog is consistent.

@jinlmsft
Revise TLA spec.
bae0bc1 
The following revision is made.

1. The clientRequests become a variable, which uniquely identified each request received by server.
2. Only valid message is evaluated, to reduce state space.
3. Add test to see if there are more than one Leader per term in the cluster.
4. Add test to see if the committedLog is consistent.
@ongardie
Copy link
Owner

Thanks @jinlmsft. Looks like there's a few little things in here, mostly good but probably needing to be teased apart and cleaned up. Given that I'm not actively working on the spec, I'll leave this PR open more or less indefinitely and link to it from the README. Hopefully people that are trying to apply the model checker will look here.

@ongardie
Copy link
Owner

Updated README in 34cdd49.

@jinlmsft
Copy link
Author

OK. Thanks,

Jin

From: Diego Ongaro [mailto:[email protected]]
Sent: Monday, August 22, 2016 1:12 PM
To: ongardie/raft.tla [email protected]
Cc: jinlmsft [email protected]; Mention [email protected]
Subject: Re: [ongardie/raft.tla] Revise TLA spec. (#4)

Thanks @jinlmsfthttps://github.com/jinlmsft. Looks like there's a few little things in here, mostly good but probably needing to be teased apart and cleaned up. Given that I'm not actively working on the spec, I'll leave this PR open more or less indefinitely and link to it from the README. Hopefully people that are trying to apply the model checker will look here.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHubhttps://github.com//pull/4#issuecomment-241534606, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AG7diKSsORmFvEmLnLXLX7MaAk-Agm3gks5qigKHgaJpZM4JqMWI.

@siddontang siddontang mentioned this pull request Jan 31, 2018
Merged
@deardeng
Copy link

jinlmsft

@jinlmsft jinlmsft
hi，I used what you provided Raft_Term_Not_Persisted.tla , but the result of running is not what you mentioned in the video,
image
image
Please help me. What's wrong with it？

lemmy added a commit to lemmy/CCF that referenced this pull request Nov 3, 2022
@lemmy
Remove unused variable committedLog.
9ab520f 
The variable committedLog is not part of the original Raft specification
but was introduced later in the still open pull request
ongardie/raft.tla#4.
lemmy added a commit to lemmy/CCF that referenced this pull request Nov 3, 2022
@lemmy
Remove unused variable committedLog.
c037cd7 
The variable committedLog is not part of the original Raft specification
but was introduced later in the still open pull request
ongardie/raft.tla#4.
@ongardie ongardie mentioned this pull request Oct 14, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@jinlmsft @ongardie @deardeng