diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla index 3350366cbb..ed5d298c89 100644 --- a/safekeeper/spec/ProposerAcceptorReconfig.tla +++ b/safekeeper/spec/ProposerAcceptorReconfig.tla @@ -169,9 +169,11 @@ ProposerSwitchConf(p, a) == \* Do CAS on the conf store, starting change into the new_members conf. StartChange(new_members) == - /\ Cardinality(new_members) = 1 \* Possible only if we don't already have the change in progress. /\ conf_store.newMembers = NULL + /\ Cardinality(new_members) = 1 + \* Not necessary, but reduces space a bit. + /\ new_members /= conf_store.members /\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> new_members] /\ UNCHANGED <>