Skip to content

Commit c739e22

Browse files
authored
fix: Fix typo mistake committed (#2584)
1 parent 2eacbbc commit c739e22

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tla+/consensus-commit/README.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ rCommit(r) == /\ rState[r] = "prepared"
2727
/\ rState' = [rState EXCEPT ![r] = "committed"]
2828
/\ cState' = cState
2929
```
30-
says that if a resource `r` is in the "prepared" state and the coordinator is in the "committed" state, then `r` can move into a "commmitted" state while the coordinator state does not change. The last line is absolutely neccessary as each state transition must describe the state of the "world".
30+
says that if a resource `r` is in the "prepared" state and the coordinator is in the "committed" state, then `r` can move into a "committed" state while the coordinator state does not change. The last line is absolutely neccessary as each state transition must describe the state of the "world".
3131

3232
If the protocol is correct, then the the formula `Consistent` should be true at every state. This formula consists of a conjunction of two conditions:
3333
1. If the coordinator is "committed" then no resource should be in the "initialized" or "aborted" state.

0 commit comments

Comments
 (0)