From 7a580627fc5e722517a0d77d5cca4160ad86f1d7 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Fri, 29 Nov 2024 17:38:11 +0300 Subject: [PATCH] fixup! AccSwitchConf, AbortChange, AccReset --- safekeeper/spec/ProposerAcceptorStatic.tla | 25 ++++++++++++---------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index 8df33cba40..162996ca8d 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -177,6 +177,19 @@ TypeOk == \* Initial \******************************************************************************** +InitAcc == + [ + \* There will be no leader in zero term, 1 is the first + \* real. + term |-> 0, + \* Again, leader in term 0 doesn't exist, but we initialize + \* term histories with it to always have common point in + \* them. Lsn is 1 because TLA+ sequences are indexed from 1 + \* (we don't want to truncate WAL out of range). + termHistory |-> << [term |-> 0, lsn |-> 1] >>, + wal |-> << >> + ] + Init == /\ prop_state = [p \in proposers |-> [ state |-> "campaign", @@ -186,17 +199,7 @@ Init == wal |-> << >>, nextSendLsn |-> EmptyF ]] - /\ acc_state = [a \in acceptors |-> [ - \* There will be no leader in zero term, 1 is the first - \* real. - term |-> 0, - \* Again, leader in term 0 doesn't exist, but we initialize - \* term histories with it to always have common point in - \* them. Lsn is 1 because TLA+ sequences are indexed from 1 - \* (we don't want to truncate WAL out of range). - termHistory |-> << [term |-> 0, lsn |-> 1] >>, - wal |-> << >> - ]] + /\ acc_state = [a \in acceptors |-> InitAcc] /\ committed = {} /\ elected_history = EmptyF