% 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[loop above] node {$t_2: \
                \begin{aligned} 
                    \tau&= x > 0  \Land 1 \leq u \leq 3 \\
                    \eta(x)&= x - u
                \end{aligned}$} ()
                (l1) edge node {$t_3: \tau = x \leq 0$}      (l2)
                    ;
\end{tikzpicture}