ongardie / raft.tla Goto Github PK

I think that there are some issues about Timeout(i) transition. When one server timeout and starts a new election, it is supposed to voted itself firstly. It should set votedFor[i] = i and votesGranted[i] = {i}.

Can you include the TLA+ config you use in this repo?

I don't think there's a correctness issue with AppendEntries, but I think there's a simple way to make verification (by proof) easier. In particular, it would be useful to add a check to this line to test if prevLogIndex <= Len(log[i]). I believe that this check is unnecessary, but verifying this adds substantial complexity to the type invariant for the system. Is there any downside to adding the check?

Can I get the source code for raft tla.Whatever the code is there is after pluscal translation & I didnt find the code before translation.Will u help me with that.

Can I get the source code for raft tla. Whatever the code is there is after pluscal translation & I didnt find the code before translation.Will u help me with that.

I don't think that DropMessage is defined correctly. In particular, it does not actually remove messages from the variables messages. Instead, it decrements the counter for the given message, if it already exists in messages. This has two issues:

• messages is not a function from Message to Nat, as the comment above message suggests. Instead, it is a function from Message to Int.
• Receive only requires that the received message be in the domain of messages, which means that it can continue to receive messages that have been dropped (even if their count drops below zero).

When i use TLC to model check the raft specification, i find that there is a situation that the cluster has two leaders with different term, i.e, one leader with currentTerm 4, the other leader with currentTerm 5. And I think that only the leader with currentTerm 5 can receive a client request to add v to log, but in Raft specification, the Timeout(i) transition doesn't restrict it, so the leader with currentTerm 4 can also receive the client request.