Different Implementation of ChangeEnsemble between BookKeeperProtocol and BookKeeperProtocolWithLimbo.

[thetumbled]

Hi, I have a question about the different Implementation of ChangeEnsemble between BookKeeperProtocol and BookKeeperProtocolWithLimbo. The ChangeEnsemble operator in BookKeeperProtocolWithLimbo is defined as follows, which only select one faied bookie and add a seemingly unnecessary check ValidNextFragment. I wonder whether it is a bug or a different implementation due to the new feature limbo? I will appreciate it if you could help to answer this question, thanks.

ChangeEnsemble(c, recovery) ==
    /\ NoPendingResends(c)
    /\ \/ recovery
       \/ ~recovery /\ c.meta_version = meta_version
    /\ \E bookie \in c.curr_fragment.ensemble :
        /\ WriteTimeoutForBookie(messages, bookie, recovery)
        /\ EnsembleAvailable(c.curr_fragment.ensemble \ {bookie}, {bookie})
        /\ ValidNextFragment(c.lac + 1)
        /\ LET new_ensemble   == SelectEnsemble(c.curr_fragment.ensemble \ {bookie}, {bookie})
               first_entry_id == c.lac + 1
           IN LET updated_fragments == UpdatedFragments(c, first_entry_id, new_ensemble)
              IN
                \* only update the metadata if not in ledger recovery
                /\ IF recovery 
                   THEN UNCHANGED << meta_version, meta_fragments >>
                   ELSE /\ meta_fragments' = updated_fragments
                        /\ meta_version' = meta_version + 1
                /\ clients' = [clients EXCEPT ![c.id] =  
                                    [c EXCEPT !.meta_version  = IF recovery THEN @ ELSE meta_version + 1,
                                              !.confirmed     = [id \in DOMAIN c.confirmed |->
                                                                   IF id >= first_entry_id
                                                                   THEN c.confirmed[id] \ {bookie}
                                                                   ELSE c.confirmed[id]],
                                              !.fragments     = updated_fragments,
                                              !.curr_fragment = Last(updated_fragments)]]
                /\ ClearWriteTimeout(bookie, recovery)