% TeX root = ../main.tex

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

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

    \node[state,rwth] (l1p134) [below=2cm of l1t] {$\langle \ell_1, \lbrace \psi_1, \psi_3, \psi_4 \rbrace \rangle$};
    \node[state,rwth] (l1p124) [right=4cm of l1p134] {$\langle \ell_1, \lbrace \psi_1, \psi_2, \psi_4 \rbrace \rangle$};
    \node[state,rwth] (l2p5) [left=4cm of l1p134] {$\langle \ell_2, \lbrace \psi_5 \rbrace \rangle$};
    
    \node[state,rot] (l2p1345) [below=2cm of l1p134] {$\langle \ell_2, \lbrace \psi_1, \psi_3, \psi_4, \psi_5 \rbrace \rangle$};
    \node[state,rot] (l2p1245) [right=4cm of l2p1345] {$\langle \ell_2, \lbrace \psi_1, \psi_2, \psi_4, \psi_5 \rbrace \rangle$};
    \node[state,rot] (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$};

    % Transitions
    \path[->]   
        (l0t) edge[grun] node (t01) { $t_{0,1}$ } (l1t)
        (l1t) edge[rwth] node[swap] (t21) { $t_{2,1}$ } (l2p5)
        (l1t) edge[rwth,bend right=20] node[swap] (t1a1) { $t_{1a,1}$ } (l1p134)
        (l1t) edge[rwth] node (t1b1) { $t_{1b,1}$ } (l1p124)
        (l2p5) edge[rot, bend right=20] node[swap] (t31) { $t_{3,1}$ } (l1p56)
        (l1p134) edge[rot] node (t22) { $t_{2,2}$ } (l2p1345)
        (l1p134) edge[rot, bend right=10] node[swap] (t1b2) { $t_{1b,2}$ } (l1p124)
        (l1p134) edge[rot,loop above,transform canvas={xshift=5mm}] node[swap] (t1a2) { $t_{1a,2}$ } ()
        (l1p134) edge[rot] node (t22) { $t_{2,2}$ } (l2p1345)
        (l1p124) edge[rot, bend right=10] node[swap] (t1a3) { $t_{1a,3}$ } (l1p134)
        (l1p124) edge[rot,loop above] node (t1b3) { $t_{1b,3}$ } ()
        (l1p124) edge[rot] node (t23) { $t_{2,3}$ } (l2p1245)
        (l1p56) edge[rot, bend right=20] node[swap] (t25) { $t_{2,5}$ } (l2p5)
        (l1p56) edge[bend right=30] node (t1a5) { $t_{1a,5}$ } (l1p13456)
        (l1p56) edge[out=270,in=210] node[swap] (t1b5) { $t_{1b,5}$ } (l1p12456)
        (l2p1345) edge[bend right=20] node[swap] (t32) { $t_{3,2}$ } (l1p13456)
        (l1p13456) edge[bend right=20] node[swap] (t24) { $t_{2,4}$ } (l2p1345)
        (l2p1245) edge[bend right=20] node[swap] (t33) { $t_{3,3}$ } (l1p12456)
        (l1p12456) edge[bend right=20] node[swap] (t26) { $t_{2,6}$ } (l2p1245)
        (l1p13456) edge[loop above,transform canvas={xshift=12mm}] node[swap] (t1a4) { $t_{1a,4}$ } ()
        (l1p12456) edge[loop above,transform canvas={xshift=12mm}] node[swap] (t1b6) { $t_{1b,6}$ } ()
        (l1p13456) edge[bend left=10] node (t1b4) { $t_{1b,4}$ } (l1p12456)
        (l1p12456) edge[bend left=10] node (t1a6) { $t_{1a,6}$ } (l1p13456)
        ;

    % General transitions
    \node[grun] [right=1cm of t01] {$G_1$};
    \node[rwth] [above right=1cm of t1b1] {$G_2$};
    \node[rot] [right=1cm of t23] {$G_3$};
\end{tikzpicture}