.

2READ

+https://ilyasergey.net/CS6213/week-03-bft.html
+
 A New Solution of Dijkstra's Concurrent Programming Problem
 http://lamport.azurewebsites.net/pubs/pubs.html#bakery
 
-
 Time, Clocks and the Ordering of Events in a Distributed System
 http://lamport.azurewebsites.net/pubs/pubs.html#time-clocks
 

KBackery.tla

@@ -58,7 +58,7 @@ CONSTANT N  \* number of processes
 \*   Y: (t1,1)<(t2,2)   ...
 \*       |              ...
 \*       v              ...
-\*      <CS             ...         <-- ~ME(cs)
+\*      <CS             ...         <- ~ME(cs)
 \*
 \*
 \* FIX: Introduce inentry[i] and before Lwait_jbehind wait for proc[j] to first
@@ -68,7 +68,7 @@ CONSTANT N  \* number of processes
 \* 4. Check wait[i]/wait[j] for race.
 \* No variables are assigned in wait => there cannot be any race here.
 
-
+--------
 
 (*******
 --algorithm KBackery