% 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] (l1a) at ($(l1) - (3,1.5)$) {$l_{1a}$};
    \node[state] (l2) [below=3cm of l1] {$l_2$};

    \path[->]   
        (l0) edge node { $t_0: \eta(x) = u $ } (l1)
        (l1) edge [out=140,in=120,looseness=2,draw=rot-75]
        node[below=0.3cm,pos=0.35] {$t_{1a}:\begin{aligned} \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1) edge [out=130,in=130,looseness=2,draw=rot-75] node[above,pos=0.4] {$t_{1b}:\begin{aligned} \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1a) edge [out=150,in=210,looseness=10] node[swap]{$\begin{aligned}
            t_{1b}:& \\ \tau = &1 \leq x \leq 3
        \\ &\Land w = 0 \\ \eta(x) &= x + 1\end{aligned}$} (l1a)
        (l1a) edge [bend right=15] node[swap] {$t_{2b}: \begin{aligned}\tau &= y > 0 \\
        &\Land w = 1\end{aligned}$} (l2)
        (l1) edge[bend left =20] node {$\begin{aligned}t_{2a}:& \\ \tau =& y > 0 \\
        \Land& w = 1\end{aligned}$} (l2)
        (l2) edge[bend left=20] node {$\begin{aligned}&t_3:\\ &\eta(y) = y - 1\end{aligned}$} (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}