Skip to content

Commit dc6470a

Browse files
josef-widderlemmy
authored andcommitted
Change loop step from 'l' to '1' in pseudo code comment of Bakery.tla
There is a typo (transcription error from the paper). Signed-off-by: Josef Widder <josef@informal.systems>
1 parent ec17f2a commit dc6470a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

specifications/Bakery-Boulangerie/Bakery.tla

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
(* L1: choosing [i] := 1 ; *)
1313
(* number[i] := 1 + maximum (number[1],..., number[N]); *)
1414
(* choosing[i] := 0; *)
15-
(* for j = 1 step l until N do *)
15+
(* for j = 1 step 1 until N do *)
1616
(* begin *)
1717
(* L2: if choosing[j] /= 0 then goto L2; *)
1818
(* L3: if number[j] /= 0 and (number [j], j) < (number[i],i) *)

0 commit comments

Comments
 (0)