% TeX root = ../main.tex

\begin{tikzpicture}[program,initial above,font=\scriptsize, 
    every state/.append style={rectangle,rounded corners=10},
    ]
    \node[state,initial]    (l0t)  {$\langle \ell_0, \texttt{true} \rangle$};

    \node[state] (l1t) [below=2cm of l0t] {$\langle \ell_1, \texttt{true} \rangle$};

    \node[state] (l1p134) [below=2cm of l1t] {$\langle \ell_1, \lbrace \psi_1, \psi_3, \psi_4 \rbrace \rangle$};
    \node[state] (l1p124) [right=4cm of l1p134] {$\langle \ell_1, \lbrace \psi_1, \psi_2, \psi_4 \rbrace \rangle$};
    \node[state] (l2py) [left=4cm of l1p134] {$\langle \ell_2, y > 0 \rangle$};
    
    \node[state] (l2p134y) [below=2cm of l1p134] {$\langle \ell_2, \psi_1 \land \psi_3 \land \psi_4 \land y>0 \rangle$};
    \node[state] (l2p124y) [right=4cm of l2p134y] {$\langle \ell_2, \psi_1 \land \psi_2 \land \psi_4 \land y>0  \rangle$};
    \node[state] (l1p56) [left=4cm of l2p1345] {$\langle \ell_1, \lbrace \psi_5, \psi_6 \rbrace \rangle$};

    \node[state,] (l1p13456) [below=2cm of l2p1345] {$\langle \ell_1, \lbrace \psi_1, \psi_3, \psi_4, \psi_5, \psi_6 \rbrace \rangle$};
    \node[state,] (l1p12456) [right=4cm of l1p13456] {$\langle \ell_1, \lbrace \psi_1, \psi_2, \psi_4, \psi_5, \psi_6 \rbrace \rangle$};

    % Neu in Bild 2
    \node[state] (l2p13456y) [below=2.5cm of l1p13456] {$\left\langle\ell_2,\begin{aligned} \psi_1 &\land \psi_3 \land \psi_4 \land\\ \psi_5 &\land \psi_6 \land y > 0 \end{aligned}\right\rangle$};
    \node[state] (l2p56y) [below=3cm of l1p56] {$\langle \ell_2, \psi_5 \land \psi_6 \land y > 0 \rangle$};
    \node[state] (l2p12456y) [right=4cm of l2p13456y] {$\left\langle\ell_2, \begin{aligned}\psi_1 &\land \psi_2 \land \psi_4 \land \\ \psi_5 &\land \psi_6 \land y > 0 \end{aligned}\right\rangle$};

    % Transitions
    \path[->]   
        (l0t) edge[] node (t01) { $t_{0,1}$ } (l1t)
        (l1t) edge[] node[swap] (t21) { $t_{2,1}$ } (l2p5)
        (l1t) edge[bend right=20] node[swap] (t1a1) { $t_{1a,1}$ } (l1p134)
        (l1t) edge[] node (t1b1) { $t_{1b,1}$ } (l1p124) %FEHLT IN  DER SKIZZE
        (l2py) edge[] node[swap] (t31) { $t_{3,1}$ } (l1p56)
        (l1p134) edge[bend right=10] node[swap] (t1b2) { $t_{1b,2}$ } (l1p124)
        (l1p134) edge[loop above,transform canvas={xshift=5mm}] node[swap] (t1a2) { $t_{1a,2}$ } ()
        (l1p134) edge[] node (t22) { $t_{2,2}$ } (l2p134y)
        (l1p124) edge[bend right=10] node[swap] (t1a3) { $t_{1a,3}$ } (l1p134)
        (l1p124) edge[loop above] node (t1b3) { $t_{1b,3}$ } ()
        (l1p124) edge[] node (t23) { $t_{2,3}$ } (l2p124y)
        (l1p56) edge[bend right=30] node (t1a6) { $t_{1a,6}$ } (l1p13456)
        (l1p56) edge[out=290,in=205] node[swap,pos=.40] (t1b6) { $t_{1b,6}$ } (l1p12456)
        (l2p134y) edge[] node[swap] (t32) { $t_{3,2}$ } (l1p13456)
        (l2p124y) edge[] node[swap] (t33) { $t_{3,3}$ } (l1p12456)
        (l1p13456) edge[loop above,transform canvas={xshift=12mm}] node[swap] (t1a4) { $t_{1a,4}$ } ()
        (l1p12456) edge[loop above,transform canvas={xshift=12mm}] node[swap] (t1b5) { $t_{1b,5}$ } ()
        (l1p13456) edge[bend left=10] node (t1b4) { $t_{1b,4}$ } (l1p12456)
        (l1p12456) edge[bend left=10] node (t1a5) { $t_{1a,5}$ } (l1p13456)
        % (l1p56) edge[rot, bend right=20] node[swap] (t25) { $t_{2,5}$ } (l2p5)
        (l1p56) edge[bend left=15,transform canvas={xshift=-4mm}] node[] (t26) { $t_{2,6}$ } (l2p56y)
        (l2p56y) edge[bend left=15,transform canvas={xshift=-4mm}] node[] (t36) { $t_{3,6}$ } (l1p56)
        % (l1p13456) edge[bend right=20] node[swap] (t24) { $t_{2,4}$ } (l2p1345)
        (l1p13456) edge[bend left=20] node[pos=.55] (t26) { $t_{2,4}$ } (l2p13456y)
        (l2p13456y) edge[bend left=20] node[pos=.45] (t34) { $t_{3,4}$ } (l1p13456)
        % (l1p12456) edge[bend right=20] node[swap] (t26) { $t_{2,6}$ } (l2p1245)
        (l1p12456) edge[bend right=20] node[swap] (t25) { $t_{2,5}$ } (l2p12456y)
        (l2p12456y) edge[bend right=20] node[swap] (t35) { $t_{3,5}$ } (l1p12456)
        ;
\end{tikzpicture}