Refactoring: advance local check point separately

Author: DaveCTurner

versionmap/tla/versionmap.tla

@@ -159,64 +159,53 @@ begin
                    /\  indexing_seqno  = NULL \/ indexing_seqno        < replication_request.seqno
                    /\  lucene.document = NULL \/ lucene.document.seqno < replication_request.seqno
         then
-                   
+   
+            if replication_request.append_only
+            then
+                (* fast path *)
+                lucene.buffered_operation := replication_request;
+            else
+                append_only_unsafe_up_to := replication_request.seqno;
+            
+                if replication_request.type = INDEX
+                then
+                    lucene.buffered_operation := replication_request;
+                    indexing_seqno := replication_request.seqno;    
+                elsif replication_request.type = DELETE
+                then
+                    lucene.buffered_operation := [ type |-> DELETE ];
+                    deletion_seqno := replication_request.seqno;
+                end if;                
+            end if;
+                                
             if replication_request.seqno > local_check_point + 1
             then
                 (* cannot advance local check point *)
                 seqnos_above_local_check_point := seqnos_above_local_check_point
                     \union {replication_request.seqno};
 
             else
+            
+                AdvanceLocalCheckPoint:
+                
                 (* advance local check point *)
                 local_check_point := CHOOSE n \in (local_check_point .. next_seqno):
                                                 /\ n > local_check_point
                                                 /\ (n + 1) \notin seqnos_above_local_check_point
                                                 /\ ((local_check_point + 2) .. n) \subseteq seqnos_above_local_check_point;
                 seqnos_above_local_check_point := { n \in seqnos_above_local_check_point: local_check_point < n };
-            end if;
-                    
-            if replication_request.append_only
-            then
-                lucene.buffered_operation := replication_request;
+                
                 if deletion_seqno /= NULL /\ deletion_seqno <= local_check_point
                 then
                     deletion_seqno := NULL;
                 end if;
-             else
-                if replication_request.type = INDEX
-                then
-                    lucene.buffered_operation := replication_request;
-                    if replication_request.seqno <= local_check_point
-                    then 
-                        indexing_seqno := NULL;
-                    else
-                        indexing_seqno := replication_request.seqno;
-                    end if;
-                    
-                    if deletion_seqno /= NULL /\ deletion_seqno <= local_check_point
-                    then
-                        deletion_seqno := NULL;
-                    end if;
-                    
-                elsif replication_request.type = DELETE
-                then
-                    lucene.buffered_operation := [ type |-> DELETE ];
-                    if replication_request.seqno <= local_check_point
-                    then 
-                        deletion_seqno := NULL;
-                    else
-                        deletion_seqno := replication_request.seqno;
-                    end if;
-                                       
-                    if indexing_seqno /= NULL /\ indexing_seqno <= local_check_point
-                    then 
-                        indexing_seqno := NULL;
-                    end if;
-                    
-                end if;
 
-                append_only_unsafe_up_to := replication_request.seqno;
+                if indexing_seqno /= NULL /\ indexing_seqno <= local_check_point
+                then 
+                    indexing_seqno := NULL;
+                end if;
             end if;
+               
         end if;
     end while;
     lucene.state := CLOSED;
@@ -520,5 +509,5 @@ VersionMapContainsNoEntriesBeforeLocalCheckPoint == /\ \/ deletion_seqno = NULL
 
 =============================================================================
 \* Modification History
-\* Last modified Fri Feb 16 16:00:45 GMT 2018 by davidturner
+\* Last modified Fri Feb 16 16:22:27 GMT 2018 by davidturner
 \* Created Tue Feb 13 13:02:51 GMT 2018 by davidturner