.

KBackery.tla

@@ -24,14 +24,14 @@ variable j \in Nat
             \* wait while proc[j] completes its entry, if it was in there, to make
             \* sure that ticket[j] becomes settled if it was wait[i]/entry[j] race.
             \* NOTE wait[i]/entry[j] race is only possible if entry[i]/entry[j] race precedes it.
-    Lwait_entry:
+    Lwait_jset:
             while (inentry[j])
-                goto Lwait_entry;
+                goto Lwait_jset;
 
             \* wait for proc[i] is ahead of proc[j].
-    Lwait_mytick:
+    Lwait_jbehind:
             while (~(ticket[j]=0 \/ (ticket[i],i) < (ticket[j],j)))
-                goto Lwait_mytick;
+                goto Lwait_jbehind;
         }
 
 \*  > service