% TeX root = ../main.tex

\begin{tikzpicture}[program,font=\scriptsize]
    \node[state,initial]    (l0)                       {$\ell_0$};
    \node[state]            (l1)    [below = of l0]    {$\ell_1$};
    \node[state]            (l2)    [below = of l1]    {$\ell_2$};

    \path[->]   (l0)      edge                  node[swap]      {$t_1: \tau = \texttt{true}$}       (l1)
                (l1)      edge                  node[swap]      {$t_3: \tau = x \leq 0$}            (l2)
                          edge [loop right]     node      {%
                              $t_2: \begin{aligned}
                                  \tau &= x > 0 \\ \eta(x)&= x+1
                              \end{aligned}$ } () 
                              ;
\end{tikzpicture}