search

ongardie / raft.tla

TLA+ specification for the Raft consensus algorithm
465 stars 73 forks source link

fix: Receive() can receive dropped messages #15

Closed liang636600 closed 2 months ago

liang636600 commented 2 months ago

Hi @ongardie, I'd be happy to submit a PR for Issue #2 . close #2

ongardie commented 2 months ago

Thanks @liang636600! This fix looks reasonable to me, but as I mentioned in #2, I haven't touched TLA+ for many years.

@dricketts or @wego1236 (or anyone else more familiar with TLA+), would you mind reviewing this small fix?

liang636600 commented 2 months ago

Hello, @ongardie, @dricketts, @wego1236, I also conducted a simple test. The test involves performing a Send(m) action followed by a Discard(m) action. I wrote a basic TLA+ code and used TLC to generate state graphs. Figure 1 shows the state graph generated using the original WithoutMessage action, while Figure 2 shows the state graph generated after I modified the WithoutMessage action.

before

Figure 1. The state graph generated using the original WithoutMessage action.

after

Figure 2. The state graph generated after modifying WithoutMessage.

As you can see, in the original state graph, when a message's counter reaches zero, the message still remains in the messages variable. However, after modifying the WithoutMessage action, the state graph shows that the messages variable is empty, which leads me to believe the modification is correct. I hope this can also assist with your review.

ongardie commented 2 months ago

Ok, I'm going ahead and merging this now.