\begin{frame}
  \frametitle{Where is Modal Logic Applied?}

  \begin{goal}{How does it work? The verifier\ldots}
    \begin{itemize}
      \item translates program execution into a graph (state space), 
      \item checks the validity of the modal formulas.
    \end{itemize}
  \end{goal}
  
  \begin{center}{\small
  \scalebox{.8}{
    \begin{tikzpicture}[default]
      \node (p) at (17.5mm,2.5mm) {$P$};
      \node (l) at (0mm,0mm) [anchor=north west,shift={(1mm,-1mm)}] {loop forever};
      \node (p1) [b=l,xshift=-4mm] {p1:}; \node [r=p1] {wait for \textit{free} = 1};
      \node (p2) [b=p1] {p2:}; \node [r=p2] {\textit{free} = 0};
      \node (p3) [b=p2] {$C_P$:}; \node [r=p3] {\emph{critical section}};
      \node (p4) [b=p3] {p4:}; \node [r=p4] {\textit{free} = 1};
      \begin{pgfonlayer}{background}
         \draw [fill=black!10,drop shadow] (0mm,5mm) rectangle (38mm,-22mm);
         \draw [fill=black!5] (0mm,0mm) rectangle (38mm,-22mm);
         \light{1,5-9}{p1}
         \light{2,10-12}{p2}
         \light{3,13-}{p3}
         \light{4}{p4}
      \end{pgfonlayer}
    \end{tikzpicture}\quad
    \begin{tikzpicture}[default]
      \node (q) at (17.5mm,2.5mm) {$Q$};
      \node (l) at (0mm,0mm) [anchor=north west,shift={(1mm,-1mm)}] {loop forever};
      \node (q1) [b=l,xshift=-4mm] {q1:}; \node [r=q1] {wait for \textit{free} = 1};
      \node (q2) [b=q1] {q2:}; \node [r=q2] {\textit{free} = 0};
      \node (q3) [b=q2] {$C_Q$:}; \node [r=q3] {\emph{critical section}};
      \node (q4) [b=q3] {q4:}; \node [r=q4] {\textit{free} = 1};
      \begin{pgfonlayer}{background}
         \draw [fill=black!10,drop shadow] (0mm,5mm) rectangle (38mm,-22mm);
         \draw [fill=black!5] (0mm,0mm) rectangle (38mm,-22mm);
         \light{1-5,9-10}{q1}
         \light{6,11}{q2}
         \light{7,12-}{q3}
         \light{8}{q4}
      \end{pgfonlayer}
    \end{tikzpicture}
  }}\end{center}
  \begin{center}
  \scalebox{.8}{
  \begin{tikzpicture}[every node/.style={ellipse,inner sep=.3mm,thick,fill=yellow!75!orange,drop shadow},
    node distance=25mm,->, thick,outer sep=1mm]
    \node (111) {p1,q1,1};
    \pause
    \node (211) [right of=111] {p2,q1,1}; \draw (111) -- (211);
    \pause
    \node (310) [right of=211] {$C_P$,q1,0}; \draw (211) -- (310);
    \pause
    \node (410) [right of=310] {p4,q1,0}; \draw (310) -- (410);
    \pause
    \draw (410) to[bend left=-10] (111);
   
    \begin{scope}[node distance=10mm]
    \pause
    \node (121) [below of=111] {p1,q2,1}; \draw (111) -- (121);
    \pause
    \node (130) [below of=121] {p1,$C_Q$,0}; \draw (121) -- (130);
    \pause
    \node (140) [below of=130] {p1,q4,0}; \draw (130) -- (140);
    \pause
    \draw (140) to[bend left=60] (111);

    \pause\pause
    \node (221) [below of=211] {p2,q2,1}; \draw (211) -- (221);
    \pause
    \node (230) [below of=221] {p2,$C_Q$,0}; \draw (221) -- (230);
    \pause
    \node (330) [right of=230,node distance=25mm,fill=red!80] {$C_P$,$C_Q$,0}; \draw (230) -- (330);

    \pause
    \draw (121) -- (221);
    \node (320) [below of=310] {$C_P$,q2,0}; \draw (221) -- (320);
    \draw (320) -- (330);
    
    \pause
    \node (240) [below of=230] {p2,q4,0}; \draw (230) -- (240);
    \node (420) [right of=320,node distance=25mm] {p4,q2,0}; \draw (320) -- (420);

    \draw (240) to[bend left=60] (211);
    \draw (420) to[bend left=-10] (121);
    
    \node (340) [below of=330] {$C_P$,q4,0}; \draw (330) -- (340);
    \node (311) [below of=340] {};%{$C_P$,q1,1}; 
    \draw [gray,dashed] (340) -- (311);

    \node (430) [right of=330,node distance=25mm] {p4,$C_Q$,0}; \draw (330) -- (430);
    \node (131) [right of=430,node distance=25mm] {};%{p1,$C_Q$,1}; 
    \draw [gray,dashed] (430) -- (131);

    \node (440) [below of=430] {p4,q4,0}; 
    \draw (420) -- (430);
    \draw (430) -- (440);
    \draw (240) -- (340);
    \draw (340) -- (440);
    \end{scope}
  \end{tikzpicture}
  }  
  \end{center}
  \vspace{10cm}
\end{frame}