% TeX root = ../main.tex
\begin{tikzpicture}[program,initial above,font=\scriptsize]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state] (l1) [below=2cm of l0] {$l_1$};
    \node[state] (l2) [below=3cm of l1] {$l_2$};

    \path[->]   
        (l0) edge node { $t_0: \eta(x) = u $ } (l1)
        (l1) edge [out=150,in=210,looseness=10] node[swap]{$\begin{aligned}
            t_1:& \\\tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1)
        (l1) edge[bend left =30] node {$\begin{aligned}t_{2}:& \\ \tau =& y > 0 \\
        \Land& w = 1\end{aligned}$} (l2)
        (l2) edge[bend left=30] node {$t_3: \eta(y) = y - 1$} (l1)
                % (l1) edge node {$t_4:x \leq 0$}      (l2)
                %      edge[loop above] node {$t_2:\begin{aligned} x &> 1 \\ x&:=
                %      x+1\end{aligned}$} ()
                %      edge[loop below] node  {$t_3:\begin{aligned} x &> 0 \\ x&:=
                %      x-1\end{aligned}$} ()
                    ;
\end{tikzpicture}