% TeX root = ../main.tex

\begin{tikzpicture}[tree,
    font=\scriptsize,
    every state/.append style={rectangle,rounded corners=10}]
    \node[state,initial]    (l0)                           {$\langle \ell_0, \texttt{true}\rangle$};
    \node[state]            (l1)    [below=1.2cm of l0]          {$\langle l_1, \texttt{true}\rangle$};
    \node[state]            (l2)    [below right=of l1]    {$\langle \ell_1, x > 1 \rangle$};
    \node[state]            (l2')   [below left=of l1]     {$\langle \ell_2, x \leq 0\rangle$};
    \node[state]            (l3)    [below right=of l2]    {$\langle \ell_1, x > 2 \rangle$};
    \node[state]            (l3')   [below left=of l2,gray]{$\langle \ell_2, \texttt{false}\rangle$};
    \node[]            (l4)    [below right=of l3]    {};
    \node[]            (l4')   [below left=of l3]     {};


    \path[->]   (l0)      edge      node      {$\tau = \texttt{true}$}    (l1)
                (l1)      edge      node[swap]{$\tau = x \leq 0$}         (l2')
                          edge      node      {$\tau = x > 0; \eta(x) = x+1$ } (l2) 
                (l2)      edge[gray]node[gray,swap]{$x \leq 0$}    (l3')
                          edge      node[]    {$\tau = x > 0; \eta(x) = x+1$ } (l3)
                              ;
    \path[dotted,->]
                (l3)      edge[gray]      (l4')
                          edge      (l4) 
                              ;
\end{tikzpicture}