Remove drop abstraction
[qlock.git] / tla / StackLock.tla
1  ----------------- MODULE StackLock  ----------------
2 EXTENDS Naturals, TLC, Sequences
3
4 CONSTANT NULL
5
6 (*--fair algorithm lockAlg
7     variables
8         Locks = [
9             Stack |-> [ Id \in 1..NUM_LOCKS |-> <<>> ],
10             Lock |-> [ Id \in 1..NUM_LOCKS |-> FALSE ]
11             ],
12         rVal = [ Id \in 1..NUM_PROCESSES |-> NULL ],
13         Nodes = [ Id \in 1..NUM_PROCESSES |-> NULL ];
14     
15     define
16         NUM_PROCESSES == 2
17         NUM_LOCKS == 1
18         L == 1
19     end define;
20     
21     procedure lock(Lock)
22     begin
23         PUSH_NODE:
24             print <<self, "lock">>;
25             Nodes[self] := FALSE;
26             call push(Lock, self);
27         FLUSH_LOCK:
28             call flush(Lock);
29         WAIT:
30             call wait(self);
31             return;
32     end procedure;
33     
34     procedure unlock(Lock)
35     begin
36         POP:
37             print <<self, "unlock">>;
38             call pop(Lock);
39         CHECK_POP:
40             if rVal[self] /= NULL then
41                 call signal(rVal[self]);
42                 return;
43             end if;
44         RELEASE:
45             call release(Lock);
46         FLUSH_LOCK:
47             call flush(Lock);
48             return;
49     end procedure;
50     
51     procedure flush(Lock)
52     begin
53         DEBUG:
54             print <<self, "flush">>;
55         LOOP:
56             while Locks.Stack[Lock] /= <<>> do
57                 TRY_ACQUIRE:
58                     call try_acquire(Lock);
59                 CHECK_ACQUIRE:
60                     if ~rVal[self] then
61                         return;
62                     end if;
63                 POP:
64                     call pop(Lock);
65                 CHECK_POP:
66                     if rVal[self]/= NULL then
67                         call signal(rVal[self]);
68                         return;
69                     end if;
70                 RELEASE:
71                     call release(Lock);
72              end while;
73              return;
74     end procedure;
75     
76     procedure try_acquire(Lock)
77     begin
78         A:
79             print <<self, "try_acquire", Locks.Lock[Lock]>>;
80             if Locks.Lock[Lock] then
81                 rVal[self] := FALSE;
82             else
83                 Locks.Lock[Lock] := TRUE;
84                 rVal[self] := TRUE;
85             end if;
86         B:
87             print <<self, "end_try_acquire", Locks.Lock[Lock]>>;
88             return;
89     end procedure;
90     
91     procedure release(Lock)
92     begin
93         A:
94             print <<self, "release">>;
95             assert Locks.Lock[Lock];
96             Locks.Lock[Lock] := FALSE;
97             return;
98     end procedure;
99     
100     procedure push(Stack, Node)
101     begin
102         A:
103             print <<self, "push">>;
104             Locks.Stack[Stack] := Append(Locks.Stack[Stack], Node);
105             return;
106     end procedure;
107     
108     procedure pop(Stack)
109     begin
110         A:
111             print <<self, "pop">>;
112             if Locks.Stack[Stack] /= <<>> then
113                 rVal[self] := Head(Locks.Stack[Stack]);
114                 Locks.Stack[Stack] := Tail(Locks.Stack[Stack]);
115                 return;
116             end if;
117         B:
118             rVal[self] := NULL;
119             return;
120     end procedure;
121
122     procedure wait(Node)
123     begin
124         A:
125             print <<self, "wait">>;
126             await Nodes[self];
127             Nodes[self] := NULL;
128             return;
129     end procedure;
130     
131     procedure signal(Node)
132     begin
133         A:
134             print <<self, "signal">>;
135             assert Nodes[Node] = FALSE;
136             Nodes[Node] := TRUE;
137             return;
138     end procedure;
139     
140     fair+ process p \in 1..NUM_PROCESSES
141     begin
142         A:
143             print <<self, "start">>; 
144             call lock(L);
145         CS:
146             assert \A i \in 1..NUM_PROCESSES : (i = self) => (pc[i] = "CS");
147         E:
148             call unlock(L);
149         DEBUG_END:
150             print <<self, "finish">>; 
151     end process;
152 end algorithm;
153 *)
154 \* BEGIN TRANSLATION
155 \* Label FLUSH_LOCK of procedure lock at line 28 col 13 changed to FLUSH_LOCK_
156 \* Label POP of procedure unlock at line 37 col 13 changed to POP_
157 \* Label CHECK_POP of procedure unlock at line 40 col 13 changed to CHECK_POP_
158 \* Label RELEASE of procedure unlock at line 45 col 13 changed to RELEASE_
159 \* Label A of procedure try_acquire at line 79 col 13 changed to A_
160 \* Label B of procedure try_acquire at line 87 col 13 changed to B_
161 \* Label A of procedure release at line 94 col 13 changed to A_r
162 \* Label A of procedure push at line 103 col 13 changed to A_p
163 \* Label A of procedure pop at line 111 col 13 changed to A_po
164 \* Label A of procedure wait at line 125 col 13 changed to A_w
165 \* Label A of procedure signal at line 134 col 13 changed to A_s
166 \* Parameter Lock of procedure lock at line 21 col 20 changed to Lock_
167 \* Parameter Lock of procedure unlock at line 34 col 22 changed to Lock_u
168 \* Parameter Lock of procedure flush at line 51 col 21 changed to Lock_f
169 \* Parameter Lock of procedure try_acquire at line 76 col 27 changed to Lock_t
170 \* Parameter Stack of procedure push at line 100 col 20 changed to Stack_
171 \* Parameter Node of procedure push at line 100 col 27 changed to Node_
172 \* Parameter Node of procedure wait at line 122 col 20 changed to Node_w
173 CONSTANT defaultInitValue
174 VARIABLES Locks, rVal, Nodes, pc, stack
175
176 (* define statement *)
177 NUM_PROCESSES == 2
178 NUM_LOCKS == 1
179 L == 1
180
181 VARIABLES Lock_, Lock_u, Lock_f, Lock_t, Lock, Stack_, Node_, Stack, Node_w, 
182           Node
183
184 vars == << Locks, rVal, Nodes, pc, stack, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
185            Stack_, Node_, Stack, Node_w, Node >>
186
187 ProcSet == (1..NUM_PROCESSES)
188
189 Init == (* Global variables *)
190         /\ Locks =     [
191                    Stack |-> [ Id \in 1..NUM_LOCKS |-> <<>> ],
192                    Lock |-> [ Id \in 1..NUM_LOCKS |-> FALSE ]
193                    ]
194         /\ rVal = [ Id \in 1..NUM_PROCESSES |-> NULL ]
195         /\ Nodes = [ Id \in 1..NUM_PROCESSES |-> NULL ]
196         (* Procedure lock *)
197         /\ Lock_ = [ self \in ProcSet |-> defaultInitValue]
198         (* Procedure unlock *)
199         /\ Lock_u = [ self \in ProcSet |-> defaultInitValue]
200         (* Procedure flush *)
201         /\ Lock_f = [ self \in ProcSet |-> defaultInitValue]
202         (* Procedure try_acquire *)
203         /\ Lock_t = [ self \in ProcSet |-> defaultInitValue]
204         (* Procedure release *)
205         /\ Lock = [ self \in ProcSet |-> defaultInitValue]
206         (* Procedure push *)
207         /\ Stack_ = [ self \in ProcSet |-> defaultInitValue]
208         /\ Node_ = [ self \in ProcSet |-> defaultInitValue]
209         (* Procedure pop *)
210         /\ Stack = [ self \in ProcSet |-> defaultInitValue]
211         (* Procedure wait *)
212         /\ Node_w = [ self \in ProcSet |-> defaultInitValue]
213         (* Procedure signal *)
214         /\ Node = [ self \in ProcSet |-> defaultInitValue]
215         /\ stack = [self \in ProcSet |-> << >>]
216         /\ pc = [self \in ProcSet |-> "A"]
217
218 PUSH_NODE(self) == /\ pc[self] = "PUSH_NODE"
219                    /\ PrintT(<<self, "lock">>)
220                    /\ Nodes' = [Nodes EXCEPT ![self] = FALSE]
221                    /\ /\ Node_' = [Node_ EXCEPT ![self] = self]
222                       /\ Stack_' = [Stack_ EXCEPT ![self] = Lock_[self]]
223                       /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "push",
224                                                                pc        |->  "FLUSH_LOCK_",
225                                                                Stack_    |->  Stack_[self],
226                                                                Node_     |->  Node_[self] ] >>
227                                                            \o stack[self]]
228                    /\ pc' = [pc EXCEPT ![self] = "A_p"]
229                    /\ UNCHANGED << Locks, rVal, Lock_, Lock_u, Lock_f, Lock_t, 
230                                    Lock, Stack, Node_w, Node >>
231
232 FLUSH_LOCK_(self) == /\ pc[self] = "FLUSH_LOCK_"
233                      /\ /\ Lock_f' = [Lock_f EXCEPT ![self] = Lock_[self]]
234                         /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "flush",
235                                                                  pc        |->  "WAIT",
236                                                                  Lock_f    |->  Lock_f[self] ] >>
237                                                              \o stack[self]]
238                      /\ pc' = [pc EXCEPT ![self] = "DEBUG"]
239                      /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_t, 
240                                      Lock, Stack_, Node_, Stack, Node_w, Node >>
241
242 WAIT(self) == /\ pc[self] = "WAIT"
243               /\ /\ Node_w' = [Node_w EXCEPT ![self] = self]
244                  /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "wait",
245                                                           pc        |->  Head(stack[self]).pc,
246                                                           Node_w    |->  Node_w[self] ] >>
247                                                       \o Tail(stack[self])]
248               /\ pc' = [pc EXCEPT ![self] = "A_w"]
249               /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
250                               Lock_t, Lock, Stack_, Node_, Stack, Node >>
251
252 lock(self) == PUSH_NODE(self) \/ FLUSH_LOCK_(self) \/ WAIT(self)
253
254 POP_(self) == /\ pc[self] = "POP_"
255               /\ PrintT(<<self, "unlock">>)
256               /\ /\ Stack' = [Stack EXCEPT ![self] = Lock_u[self]]
257                  /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "pop",
258                                                           pc        |->  "CHECK_POP_",
259                                                           Stack     |->  Stack[self] ] >>
260                                                       \o stack[self]]
261               /\ pc' = [pc EXCEPT ![self] = "A_po"]
262               /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
263                               Lock_t, Lock, Stack_, Node_, Node_w, Node >>
264
265 CHECK_POP_(self) == /\ pc[self] = "CHECK_POP_"
266                     /\ IF rVal[self] /= NULL
267                           THEN /\ /\ Node' = [Node EXCEPT ![self] = rVal[self]]
268                                   /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "signal",
269                                                                            pc        |->  Head(stack[self]).pc,
270                                                                            Node      |->  Node[self] ] >>
271                                                                        \o Tail(stack[self])]
272                                /\ pc' = [pc EXCEPT ![self] = "A_s"]
273                           ELSE /\ pc' = [pc EXCEPT ![self] = "RELEASE_"]
274                                /\ UNCHANGED << stack, Node >>
275                     /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
276                                     Lock_t, Lock, Stack_, Node_, Stack, Node_w >>
277
278 RELEASE_(self) == /\ pc[self] = "RELEASE_"
279                   /\ /\ Lock' = [Lock EXCEPT ![self] = Lock_u[self]]
280                      /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "release",
281                                                               pc        |->  "FLUSH_LOCK",
282                                                               Lock      |->  Lock[self] ] >>
283                                                           \o stack[self]]
284                   /\ pc' = [pc EXCEPT ![self] = "A_r"]
285                   /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
286                                   Lock_t, Stack_, Node_, Stack, Node_w, Node >>
287
288 FLUSH_LOCK(self) == /\ pc[self] = "FLUSH_LOCK"
289                     /\ /\ Lock_f' = [Lock_f EXCEPT ![self] = Lock_u[self]]
290                        /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "flush",
291                                                                 pc        |->  Head(stack[self]).pc,
292                                                                 Lock_f    |->  Lock_f[self] ] >>
293                                                             \o Tail(stack[self])]
294                     /\ pc' = [pc EXCEPT ![self] = "DEBUG"]
295                     /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_t, 
296                                     Lock, Stack_, Node_, Stack, Node_w, Node >>
297
298 unlock(self) == POP_(self) \/ CHECK_POP_(self) \/ RELEASE_(self)
299                    \/ FLUSH_LOCK(self)
300
301 DEBUG(self) == /\ pc[self] = "DEBUG"
302                /\ PrintT(<<self, "flush">>)
303                /\ pc' = [pc EXCEPT ![self] = "LOOP"]
304                /\ UNCHANGED << Locks, rVal, Nodes, stack, Lock_, Lock_u, 
305                                Lock_f, Lock_t, Lock, Stack_, Node_, Stack, 
306                                Node_w, Node >>
307
308 LOOP(self) == /\ pc[self] = "LOOP"
309               /\ IF Locks.Stack[Lock_f[self]] /= <<>>
310                     THEN /\ pc' = [pc EXCEPT ![self] = "TRY_ACQUIRE"]
311                          /\ UNCHANGED << stack, Lock_f >>
312                     ELSE /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
313                          /\ Lock_f' = [Lock_f EXCEPT ![self] = Head(stack[self]).Lock_f]
314                          /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
315               /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_t, Lock, 
316                               Stack_, Node_, Stack, Node_w, Node >>
317
318 TRY_ACQUIRE(self) == /\ pc[self] = "TRY_ACQUIRE"
319                      /\ /\ Lock_t' = [Lock_t EXCEPT ![self] = Lock_f[self]]
320                         /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "try_acquire",
321                                                                  pc        |->  "CHECK_ACQUIRE",
322                                                                  Lock_t    |->  Lock_t[self] ] >>
323                                                              \o stack[self]]
324                      /\ pc' = [pc EXCEPT ![self] = "A_"]
325                      /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
326                                      Lock, Stack_, Node_, Stack, Node_w, Node >>
327
328 CHECK_ACQUIRE(self) == /\ pc[self] = "CHECK_ACQUIRE"
329                        /\ IF ~rVal[self]
330                              THEN /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
331                                   /\ Lock_f' = [Lock_f EXCEPT ![self] = Head(stack[self]).Lock_f]
332                                   /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
333                              ELSE /\ pc' = [pc EXCEPT ![self] = "POP"]
334                                   /\ UNCHANGED << stack, Lock_f >>
335                        /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, 
336                                        Lock_t, Lock, Stack_, Node_, Stack, 
337                                        Node_w, Node >>
338
339 POP(self) == /\ pc[self] = "POP"
340              /\ /\ Stack' = [Stack EXCEPT ![self] = Lock_f[self]]
341                 /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "pop",
342                                                          pc        |->  "CHECK_POP",
343                                                          Stack     |->  Stack[self] ] >>
344                                                      \o stack[self]]
345              /\ pc' = [pc EXCEPT ![self] = "A_po"]
346              /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, Lock_t, 
347                              Lock, Stack_, Node_, Node_w, Node >>
348
349 CHECK_POP(self) == /\ pc[self] = "CHECK_POP"
350                    /\ IF rVal[self]/= NULL
351                          THEN /\ /\ Node' = [Node EXCEPT ![self] = rVal[self]]
352                                  /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "signal",
353                                                                           pc        |->  Head(stack[self]).pc,
354                                                                           Node      |->  Node[self] ] >>
355                                                                       \o Tail(stack[self])]
356                               /\ pc' = [pc EXCEPT ![self] = "A_s"]
357                          ELSE /\ pc' = [pc EXCEPT ![self] = "RELEASE"]
358                               /\ UNCHANGED << stack, Node >>
359                    /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
360                                    Lock_t, Lock, Stack_, Node_, Stack, Node_w >>
361
362 RELEASE(self) == /\ pc[self] = "RELEASE"
363                  /\ /\ Lock' = [Lock EXCEPT ![self] = Lock_f[self]]
364                     /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "release",
365                                                              pc        |->  "LOOP",
366                                                              Lock      |->  Lock[self] ] >>
367                                                          \o stack[self]]
368                  /\ pc' = [pc EXCEPT ![self] = "A_r"]
369                  /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, 
370                                  Lock_t, Stack_, Node_, Stack, Node_w, Node >>
371
372 flush(self) == DEBUG(self) \/ LOOP(self) \/ TRY_ACQUIRE(self)
373                   \/ CHECK_ACQUIRE(self) \/ POP(self) \/ CHECK_POP(self)
374                   \/ RELEASE(self)
375
376 A_(self) == /\ pc[self] = "A_"
377             /\ PrintT(<<self, "try_acquire", Locks.Lock[Lock_t[self]]>>)
378             /\ IF Locks.Lock[Lock_t[self]]
379                   THEN /\ rVal' = [rVal EXCEPT ![self] = FALSE]
380                        /\ Locks' = Locks
381                   ELSE /\ Locks' = [Locks EXCEPT !.Lock[Lock_t[self]] = TRUE]
382                        /\ rVal' = [rVal EXCEPT ![self] = TRUE]
383             /\ pc' = [pc EXCEPT ![self] = "B_"]
384             /\ UNCHANGED << Nodes, stack, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
385                             Stack_, Node_, Stack, Node_w, Node >>
386
387 B_(self) == /\ pc[self] = "B_"
388             /\ PrintT(<<self, "end_try_acquire", Locks.Lock[Lock_t[self]]>>)
389             /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
390             /\ Lock_t' = [Lock_t EXCEPT ![self] = Head(stack[self]).Lock_t]
391             /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
392             /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_u, Lock_f, Lock, 
393                             Stack_, Node_, Stack, Node_w, Node >>
394
395 try_acquire(self) == A_(self) \/ B_(self)
396
397 A_r(self) == /\ pc[self] = "A_r"
398              /\ PrintT(<<self, "release">>)
399              /\ Assert(Locks.Lock[Lock[self]], 
400                        "Failure of assertion at line 95, column 13.")
401              /\ Locks' = [Locks EXCEPT !.Lock[Lock[self]] = FALSE]
402              /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
403              /\ Lock' = [Lock EXCEPT ![self] = Head(stack[self]).Lock]
404              /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
405              /\ UNCHANGED << rVal, Nodes, Lock_, Lock_u, Lock_f, Lock_t, 
406                              Stack_, Node_, Stack, Node_w, Node >>
407
408 release(self) == A_r(self)
409
410 A_p(self) == /\ pc[self] = "A_p"
411              /\ PrintT(<<self, "push">>)
412              /\ Locks' = [Locks EXCEPT !.Stack[Stack_[self]] = Append(Locks.Stack[Stack_[self]], Node_[self])]
413              /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
414              /\ Stack_' = [Stack_ EXCEPT ![self] = Head(stack[self]).Stack_]
415              /\ Node_' = [Node_ EXCEPT ![self] = Head(stack[self]).Node_]
416              /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
417              /\ UNCHANGED << rVal, Nodes, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
418                              Stack, Node_w, Node >>
419
420 push(self) == A_p(self)
421
422 A_po(self) == /\ pc[self] = "A_po"
423               /\ PrintT(<<self, "pop">>)
424               /\ IF Locks.Stack[Stack[self]] /= <<>>
425                     THEN /\ rVal' = [rVal EXCEPT ![self] = Head(Locks.Stack[Stack[self]])]
426                          /\ Locks' = [Locks EXCEPT !.Stack[Stack[self]] = Tail(Locks.Stack[Stack[self]])]
427                          /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
428                          /\ Stack' = [Stack EXCEPT ![self] = Head(stack[self]).Stack]
429                          /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
430                     ELSE /\ pc' = [pc EXCEPT ![self] = "B"]
431                          /\ UNCHANGED << Locks, rVal, stack, Stack >>
432               /\ UNCHANGED << Nodes, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
433                               Stack_, Node_, Node_w, Node >>
434
435 B(self) == /\ pc[self] = "B"
436            /\ rVal' = [rVal EXCEPT ![self] = NULL]
437            /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
438            /\ Stack' = [Stack EXCEPT ![self] = Head(stack[self]).Stack]
439            /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
440            /\ UNCHANGED << Locks, Nodes, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
441                            Stack_, Node_, Node_w, Node >>
442
443 pop(self) == A_po(self) \/ B(self)
444
445 A_w(self) == /\ pc[self] = "A_w"
446              /\ PrintT(<<self, "wait">>)
447              /\ Nodes[self]
448              /\ Nodes' = [Nodes EXCEPT ![self] = NULL]
449              /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
450              /\ Node_w' = [Node_w EXCEPT ![self] = Head(stack[self]).Node_w]
451              /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
452              /\ UNCHANGED << Locks, rVal, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
453                              Stack_, Node_, Stack, Node >>
454
455 wait(self) == A_w(self)
456
457 A_s(self) == /\ pc[self] = "A_s"
458              /\ PrintT(<<self, "signal">>)
459              /\ Assert(Nodes[Node[self]] = FALSE, 
460                        "Failure of assertion at line 135, column 13.")
461              /\ Nodes' = [Nodes EXCEPT ![Node[self]] = TRUE]
462              /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
463              /\ Node' = [Node EXCEPT ![self] = Head(stack[self]).Node]
464              /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
465              /\ UNCHANGED << Locks, rVal, Lock_, Lock_u, Lock_f, Lock_t, Lock, 
466                              Stack_, Node_, Stack, Node_w >>
467
468 signal(self) == A_s(self)
469
470 A(self) == /\ pc[self] = "A"
471            /\ PrintT(<<self, "start">>)
472            /\ /\ Lock_' = [Lock_ EXCEPT ![self] = L]
473               /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "lock",
474                                                        pc        |->  "CS",
475                                                        Lock_     |->  Lock_[self] ] >>
476                                                    \o stack[self]]
477            /\ pc' = [pc EXCEPT ![self] = "PUSH_NODE"]
478            /\ UNCHANGED << Locks, rVal, Nodes, Lock_u, Lock_f, Lock_t, Lock, 
479                            Stack_, Node_, Stack, Node_w, Node >>
480
481 CS(self) == /\ pc[self] = "CS"
482             /\ Assert(\A i \in 1..NUM_PROCESSES : (i = self) => (pc[i] = "CS"), 
483                       "Failure of assertion at line 146, column 13.")
484             /\ pc' = [pc EXCEPT ![self] = "E"]
485             /\ UNCHANGED << Locks, rVal, Nodes, stack, Lock_, Lock_u, Lock_f, 
486                             Lock_t, Lock, Stack_, Node_, Stack, Node_w, Node >>
487
488 E(self) == /\ pc[self] = "E"
489            /\ /\ Lock_u' = [Lock_u EXCEPT ![self] = L]
490               /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "unlock",
491                                                        pc        |->  "DEBUG_END",
492                                                        Lock_u    |->  Lock_u[self] ] >>
493                                                    \o stack[self]]
494            /\ pc' = [pc EXCEPT ![self] = "POP_"]
495            /\ UNCHANGED << Locks, rVal, Nodes, Lock_, Lock_f, Lock_t, Lock, 
496                            Stack_, Node_, Stack, Node_w, Node >>
497
498 DEBUG_END(self) == /\ pc[self] = "DEBUG_END"
499                    /\ PrintT(<<self, "finish">>)
500                    /\ pc' = [pc EXCEPT ![self] = "Done"]
501                    /\ UNCHANGED << Locks, rVal, Nodes, stack, Lock_, Lock_u, 
502                                    Lock_f, Lock_t, Lock, Stack_, Node_, Stack, 
503                                    Node_w, Node >>
504
505 p(self) == A(self) \/ CS(self) \/ E(self) \/ DEBUG_END(self)
506
507 Next == (\E self \in ProcSet:  \/ lock(self) \/ unlock(self) \/ flush(self)
508                                \/ try_acquire(self) \/ release(self)
509                                \/ push(self) \/ pop(self) \/ wait(self)
510                                \/ signal(self))
511            \/ (\E self \in 1..NUM_PROCESSES: p(self))
512            \/ (* Disjunct to prevent deadlock on termination *)
513               ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
514
515 Spec == /\ Init /\ [][Next]_vars
516         /\ WF_vars(Next)
517         /\ \A self \in 1..NUM_PROCESSES : /\ SF_vars(p(self))
518                                           /\ SF_vars(lock(self))
519                                           /\ SF_vars(unlock(self))
520                                           /\ SF_vars(flush(self))
521                                           /\ SF_vars(try_acquire(self))
522                                           /\ SF_vars(release(self))
523                                           /\ SF_vars(push(self))
524                                           /\ SF_vars(pop(self))
525                                           /\ SF_vars(wait(self))
526                                           /\ SF_vars(signal(self))
527
528 Termination == <>(\A self \in ProcSet: pc[self] = "Done")
529
530 \* END TRANSLATION
531
532 ====