.

KBackery.tla

@@ -28,7 +28,7 @@ variable j \in Nat
             while (inentry[j])
                 goto Lwait_jset;
 
-            \* wait for proc[i] is ahead of proc[j].
+            \* wait for when proc[i] is ahead of proc[j].
     Lwait_jbehind:
             while (~(ticket[j]=0 \/ (ticket[i],i) < (ticket[j],j)))
                 goto Lwait_jbehind;