зеркало из https://github.com/microsoft/CCF.git
Fixing QuorumLogInv in TLA+ spec (#4859)
This commit is contained in:
Родитель
21e0d911de
Коммит
5d720ddab5
|
@ -1025,7 +1025,7 @@ LogMatchingInv ==
|
|||
\* of at least one server in every quorum
|
||||
QuorumLogInv ==
|
||||
\A i \in Servers :
|
||||
\A S \in Quorums[GetServerSetForIndex(i, commitIndex[i])] :
|
||||
\A S \in Quorums[CurrentConfiguration(i)] :
|
||||
\E j \in S :
|
||||
IsPrefix(Committed(i), log[j])
|
||||
|
||||
|
|
Загрузка…
Ссылка в новой задаче