% TeX root = ../main.tex

\begin{tikzpicture}[program,initial left]
    \node[state,initial]    (l0)                       {$\ell_0$};
    \node[state] (l1) [right=4cm of l0] {$\ell_1$};
    \node[state] (l2) [right=4cm of l1] {$\ell_2$};

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