\tikzset{program/.style={
    shorten >=1pt,
    >={Stealth[round]},
    node distance=1.5cm,
    every state/.style={minimum size=0.7cm,inner sep=2pt},
    semithick,
    on grid,
    auto,
    initial text=,
    initial above
}}
\tikzset{tree/.style={
    program,
    every state/.style={draw=none,rectangle,minimum size=0pt,inner sep=2pt},
    node distance=1.8cm
    }}

% TeX root = ../main.tex
\begin{tikzpicture}[tree]
    \node[state,initial]    (l0)                           {$\langle l_0, \textit{true}\rangle$};
    \node[state]            (l1)    [below=1.2cm of l0]          {$\langle l_1, \textit{true}\rangle$};
    \node[state]            (l2)    [below right=of l1]    {$\langle l_1, x > 1 \rangle$};
    \node[state]            (l2')   [below left=of l1]     {$\langle l_2, x \leq 0\rangle$};
    \node[state]            (l3)    [below right=of l2]    {$\langle l_1, x > 2 \rangle$};
    \node[state]            (l3')   [below left=of l2]     {$\langle l_2, \textit{false}\rangle$};
    \node[state]            (l4)    [below right=of l3]    {};
    \node[state]            (l4')   [below left=of l3]     {};
    \path[->]   (l0)      edge      node      {$\textit{true}$}       (l1)
                (l1)      edge      node[swap]{$x \leq 0$}            (l2')
                          edge      node      {$x > 0, x := x+1$ } (l2) 
                (l2)      edge      node[swap]{$x \leq 0$}            (l3')
                          edge      node[]    {$x > 0, x := x+1$ } (l3)
                              ;
    \path[dotted,->]
                (l3)      edge      (l4')
                          edge      (l4) 
                              ;
\end{tikzpicture}

% TeX root = ../main.tex
\begin{tikzpicture}[program]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state]            (l1)    [below = of l0]    {$l_1$};
    \node[state]            (l2)    [right= 3cm of l1]    {$l_2$};
    \node[state]            (l3)    [below = of l1]    {$l_3$};
    \path[->]   (l0)      edge node[swap]      {$\textit{true}$}       (l1)
                (l1)      edge node            {$x > 0$}               (l2)
                          edge node[swap]      {$x \leq 0$}            (l3)
                (l2)      edge[bend left=45]
                          node[anchor=north west] {$\begin{aligned}y &> 0\\ y&:= y-1\end{aligned}$}      (l1)
                          edge[bend right=45]
                          node[anchor=south west] {$\begin{aligned}y &\leq 0\\ x&:=x-1\end{aligned}$}    (l1)
                              ;
\end{tikzpicture}

% TeX root = ../main.tex
\begin{tikzpicture}[tree]
    \node[state,initial]    (l0)                           {$\langle l_0, \textit{true}\rangle$};
    \node[state]            (l1)    [below=1.2cm of l0]          {$\langle l_1, \textit{true}\rangle$};
    \node[state]            (l2)    [below right=of l1]    {$\langle l_1, x > 1 \rangle$};
    \node[state]            (l2')   [below left=of l1]     {$\langle l_2, x \leq 0\rangle$};
    \node[state]            (l3)    [below right=of l2]    {$\langle l_1, x > 2 \rangle$};
    \node[state]            (l3')   [below left=of l2]     {$\langle l_2, \textit{false}\rangle$};
    \node[state]            (l4)    [below right=of l3]    {};
    \node[state]            (l4')   [below left=of l3]     {};
    \path[->]   (l0)      edge      node      {$\textit{true}$}       (l1)
                (l1)      edge      node[swap]{$x \leq 0$}            (l2')
                          edge      node      {$x > 0, x := x+1$ } (l2) 
                (l2)      edge      node[swap]{$x \leq 0$}            (l3')
                          edge      node[]    {$x > 0, x := x+1$ } (l3)
                              ;
    \path[dotted,->]
                (l3)      edge      (l4')
                          edge      (l4) 
                              ;
\end{tikzpicture}

% TeX root = ../main.tex
\begin{tikzpicture}[program]
    \node[state,initial]    (l0)                       {$l_0$};
    \node[state]            (l1)    [below = of l0]    {$l_1$};
    \node[state]            (l2)    [below = of l1]    {$l_2$};
    \path[->]   (l0)      edge                  node[swap]      {$\textit{true}$}       (l1)
                (l1)      edge                  node[swap]      {$x \leq 0$}            (l2)
                          edge [loop right]     node      {%
                              $\begin{aligned}
                                  x &> 0 \\ x &:= x+1
                              \end{aligned}$ } () 
                              ;
\end{tikzpicture}

            \input{figures/ch3_example_program.tex}

            \input{figures/ch3_example1_program.tex}
        }
        \subbottom[Extract of the evaluation tree]{
            \input{figures/ch3_example1_tree.tex}
        }
        \caption{Foo}
    \end{figure} \todo{ref}
    \begin{figure}
        \centering
        \subbottom[Program]{
            \input{figures/ch3_example2_program.tex}

            \input{figures/ch3_example_tree.tex}

            \input{figures/ch3_example2_tree.tex}