\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}