\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{}
%\addtolength{\textwidth}{12em}
\begin{popup}
\subsection*{The Big-Step Bakery Algorithm}

\begin{nopcal}
--algorithm BigStepBakery 
{  variable num = [i \in Procs |-> 0] ;
   process (pr \in Procs)
     variable unchecked = {} ; 
     {  ncs: while (TRUE)             
               {  enter: with (i \in { j \in Nat : \A q \in Procs : j > num[q] })
                           {  num[self] := i  } ;  
                         unchecked := Procs \ {self} ;          
                  wait:  while (unchecked # {}) 
                           {  with (q \in unchecked) 
                                {  await \/ num[q] = 0
                                         \/ <<num[self], self>> \prec <<num[q], q>> ;
                                   unchecked := unchecked \ {q}
                                }
                           } ;
                  cs:    skip ;   (* critical section *)
                  exit:  num[self] := 0 
               }
     } 
} 
\end{nopcal}
\begin{tlatex}
\@x{ {\p@mmalgorithm} BigStepBakery}%
 \@x{ {\p@lbrace}\@s{4.1} {\p@variable} num \.{=} [ i \.{\in} Procs
 \.{\mapsto} 0 ] {\p@semicolon}}%
\@x{\@s{13.68} {\p@process} {\p@lparen} pr \.{\in} Procs {\p@rparen}}%
\@x{\@s{21.88} {\p@variable} unchecked \.{=} \{ \} {\p@semicolon}}%
 \@x{\@s{21.88} {\p@lbrace}\@s{4.1} ncs\@s{.5}\textrm{:}\@s{3} {\p@while}
 {\p@lparen} {\TRUE} {\p@rparen}}%
 \@x{\@s{65.17} {\p@lbrace}\@s{4.1} enter\@s{.5}\textrm{:}\@s{3} {\p@with}
 {\p@lparen} i \.{\in} \{ j \.{\in} Nat \.{:} \A\, q \.{\in} Procs \.{:} j
 \.{>} num [ q ] \} {\p@rparen}}%
 \@x{\@s{116.77} {\p@lbrace}\@s{4.1} num [ self ] \.{:=} i\@s{4.1} {\p@rbrace}
 {\p@semicolon}}%
 \@x{\@s{108.57} unchecked \.{:=} Procs \.{\,\backslash\,} \{ self \}
 {\p@semicolon}}%
 \@x{\@s{78.85} wait\@s{.5}\textrm{:}\@s{3}\@s{4.34} {\p@while} {\p@lparen}
 unchecked \.{\neq} \{ \} {\p@rparen}}%
 \@x{\@s{116.77} {\p@lbrace}\@s{4.1} {\p@with} {\p@lparen} q \.{\in} unchecked
 {\p@rparen}}%
\@x{\@s{138.65} {\p@lbrace}\@s{4.1} {\p@await} \.{\lor} num [ q ] \.{=} 0}%
 \@x{\@s{182.68} \.{\lor} {\langle} num [ self ] ,\, self {\rangle} \.{\prec}
 {\langle} num [ q ] ,\, q {\rangle} {\p@semicolon}}%
\@x{\@s{152.34} unchecked \.{:=} unchecked \.{\,\backslash\,} \{ q \}}%
\@x{\@s{138.65} {\p@rbrace}}%
\@x{\@s{116.77} {\p@rbrace} {\p@semicolon}}%
 \@x{\@s{78.85} cs\@s{.5}\textrm{:}\@s{3}\@s{13.92} {\p@skip}
 {\p@semicolon}\@s{8.2}}%
\@y{%
  critical section 
}%
\@xx{}%
\@x{\@s{78.85} exit\@s{.5}\textrm{:}\@s{3}\@s{6.86} num [ self ] \.{:=} 0}%
\@x{\@s{65.17} {\p@rbrace}}%
\@x{\@s{21.88} {\p@rbrace}}%
\@x{ {\p@rbrace}}%
\end{tlatex}
\end{popup}
\makepopup