This commit is contained in:
Amaury Chamayou 2024-03-05 16:04:52 +00:00 коммит произвёл GitHub
Родитель 604fc2aa5d
Коммит bbf9c9c66c
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: B5690EEEBB952194
1 изменённых файлов: 1 добавлений и 1 удалений

Просмотреть файл

@ -775,7 +775,7 @@ ChangeConfigurationInt(i, newConfiguration) ==
\* Note that the sentIndex is set to the log entry *before* the reconfiguration was added
\* This is to allow the send AE action to send an initial heartbeat which matches the implementation
/\ LET
addedNodes == newConfiguration \ CurrentConfiguration(i)
addedNodes == newConfiguration \ MaxConfiguration(i)
newSentIndex == [ k \in Servers |-> IF k \in addedNodes THEN Len(log[i]) ELSE sentIndex[i][k]]
IN sentIndex' = [sentIndex EXCEPT ![i] = newSentIndex]
/\ removedFromConfiguration' = removedFromConfiguration \cup (MaxConfiguration(i) \ newConfiguration)