.

KBackery.tla

+------------------------------ MODULE KBackery ------------------------------
+
+CONSTANT N  \* number of processes
+
+
+(*******
+--algorithm KBackery
+variables
+\*  > *[i] is located on memory unit of proc[i]
+    ticket  = [i \in 1..N |-> 0]      \* ticket=0 means "inactive"  XXX or `^\infty^' ?
+    inentry = [i \in 1..N |-> FALSE]  \* T while in entry. To avoid ~ME(cs) on wait/entry race
+
+process(i \in 1..N)
+variable j \in Nat
+{
+    while (TRUE)  {
+\*  > get a ticket
+        inentry[i] := TRUE
+        ticket[i]  := 1 + max(ticket[j]  \A j \in 1..N)  \* NOTE race wrt reading ticket[j]
+        inentry[i] := FALSE
+
+\*  > wait till when got ticket is < all other tickets
+        for  j \in 1..N  {
+            \* 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:
+            while (inentry[j])
+                goto Lwait_entry;
+
+            \* wait for proc[i] is ahead of proc[j].
+    Lwait_mytick:
+            while (~(ticket[j]=0 \/ (ticket[i],i) < (ticket[j],j)))
+                goto Lwait_mytick;
+        }
+
+\*  > service
+    cs: skip
+
+\*  > end - recycle the ticket
+        ticket[i] := 0
+    }
+}
+*******)
+
+=============================================================================

KBackery.toolbox/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>KBackery</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>KBackery.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/KBackery.tla</locationURI>
+		</link>
+	</linkedResources>
+</projectDescription>

KBackery.toolbox/.settings/org.lamport.tla.toolbox.prefs

+ProjectRootFile=PARENT-1-PROJECT_LOC/KBackery.tla
+eclipse.preferences.version=1

kbackery.txt

+	process(i)
+	ticket[i] := 0
+
+получить талончик
+
+	ticket[i] := 1 + max(ticket[j]