1.1 --- a/slides/src/slides.tex Tue Jul 19 21:29:46 2011 +0200
1.2 +++ b/slides/src/slides.tex Wed Jul 20 03:03:50 2011 +0200
1.3 @@ -1,6 +1,16 @@
1.4 \documentclass[9pt]{beamer}
1.5 \usetheme{Boadilla}
1.6 -\usecolortheme{seagull}
1.7 +\usecolortheme{dove}
1.8 +\usecolortheme{orchid}
1.9 +\usecolortheme{dolphin}
1.10 +%\usecolortheme{seagull}
1.11 +
1.12 +\usepackage{color}
1.13 +\usepackage{ulem}
1.14 +\usepackage{graphicx}
1.15 +\usepackage{tikz}
1.16 +\usetikzlibrary{automata}
1.17 +\usepackage{subfigure}
1.18
1.19 \newcommand{\M}{\mathcal{M}}
1.20 \newcommand{\N}{\mathbb{N}_0}
1.21 @@ -79,6 +89,162 @@
1.22
1.23 \begin{frame}
1.24 \frametitle{Automata}
1.25 +\framesubtitle{Example 1/3}
1.26 +\begin{figure}
1.27 +\centering
1.28 +\only<1>{
1.29 +\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
1.30 + %every state/.style={fill, draw=none, gray, text=white},
1.31 + ,accepting/.style={fill, gray!50!black, text=white}
1.32 + %initial/.style ={gray, text=white}]%, thick]
1.33 + ]
1.34 +\node[state,initial, initial text=] (q_0) {$q_0$};
1.35 +\node[state] (q_1) [above right of= q_0] {$q_1$};
1.36 +\node[state,accepting](q_2) [below right of= q_1] {$q_2$};
1.37 +\path[->]
1.38 +(q_0) edge node {$a$} (q_1)
1.39 + edge [loop above] node {$b$} ()
1.40 +(q_1) edge node {$b$} (q_2)
1.41 + edge [loop above] node {$a$} ()
1.42 +(q_2) %edge node {$a$} (q_1)
1.43 + edge node {$b$} (q_0);
1.44 +\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
1.45 +\end{tikzpicture}
1.46 +}
1.47 +
1.48 +\only<2>{
1.49 +\begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
1.50 + %every state/.style={fill, draw=none, gray, text=white},
1.51 + ,accepting/.style={fill, gray!50!black, text=white}
1.52 + %initial/.style ={gray, text=white}]%, thick]
1.53 + ]
1.54 +\node[state,initial, initial text=] (q_0) {$q_0$};
1.55 +\node[state] (q_1) [above right of= q_0] {$q_1$};
1.56 +\node[state,accepting](q_2) [below right of= q_1] {$q_2$};
1.57 +\path[->]
1.58 +(q_0)
1.59 + edge [loop above] node {$b$} ()
1.60 +(q_1)
1.61 + edge [loop above] node {$a$} ()
1.62 +(q_2) %edge node {$a$} (q_1)
1.63 + edge node {$b$} (q_0);
1.64 +\color{green}
1.65 +\path[->]
1.66 +(q_0) edge node {$a$} (q_1)
1.67 +(q_1) edge node {$b$} (q_2);
1.68 +\draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
1.69 +\end{tikzpicture}
1.70 +\color{black}
1.71 +}
1.72 +%Automaton $\A_1$
1.73 +\end{figure}
1.74 +\end{frame}
1.75 +
1.76 +\begin{frame}
1.77 +\frametitle{Automata}
1.78 +\framesubtitle{Example 2/3 (Complement)}
1.79 +\begin{figure}
1.80 +\centering
1.81 +\only<-1>{
1.82 + \subfigure
1.83 + {
1.84 + \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
1.85 + %every state/.style={fill, draw=none, gray, text=white},
1.86 + ,accepting/.style={fill, gray!50!black, text=white}
1.87 + %initial/.style ={gray, text=white}]%, thick]
1.88 + ]
1.89 + \node[state,initial, initial text=, accepting] (q_0) {$q_0$};
1.90 + \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
1.91 + \node[state](q_2) [below right of= q_1] {$q_2$};
1.92 + \path[->]
1.93 + (q_0) edge node {$a$} (q_1)
1.94 + edge [loop above] node {$b$} ()
1.95 + (q_1) edge node {$b$} (q_2)
1.96 + edge [loop above] node {$a$} ()
1.97 + (q_2) %edge node {$a$} (q_1)
1.98 + edge node {$b$} (q_0);
1.99 + \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
1.100 + \end{tikzpicture}
1.101 + }
1.102 +}
1.103 +\only<2>{
1.104 + \subfigure
1.105 + {
1.106 + \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
1.107 + %every state/.style={fill, draw=none, gray, text=white},
1.108 + ,accepting/.style={fill, gray!50!black, text=white}
1.109 + %initial/.style ={gray, text=white}]%, thick]
1.110 + ]
1.111 + \node[state,initial, initial text=, accepting] (q_0) {$q_0$};
1.112 + \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
1.113 + \node[state](q_2) [below right of= q_1] {$q_2$};
1.114 + \path[->]
1.115 + (q_0)
1.116 + edge [loop above] node {$b$} ()
1.117 + (q_1)
1.118 + edge [loop above] node {$a$} ();
1.119 + \color{red}
1.120 + \path[->]
1.121 + (q_0) edge node {$a$} (q_1)
1.122 + (q_1) edge node {$b$} (q_2)
1.123 + (q_2) edge node {$b$} (q_0);
1.124 + \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
1.125 + \end{tikzpicture} \color{red}
1.126 + }
1.127 + \color{black}
1.128 +}
1.129 +\only<3->{ \setcounter{subfigure}{0}
1.130 + \subfigure[\sout{Complement automaton}]
1.131 + {
1.132 + \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
1.133 + %every state/.style={fill, draw=none, gray, text=white},
1.134 + ,accepting/.style={fill, gray!50!black, text=white}
1.135 + %initial/.style ={gray, text=white}]%, thick]
1.136 + ]
1.137 + \node[state,initial, initial text=, accepting] (q_0) {$q_0$};
1.138 + \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
1.139 + \node[state](q_2) [below right of= q_1] {$q_2$};
1.140 + \path[->]
1.141 + (q_0)
1.142 + edge [loop above] node {$b$} ()
1.143 + (q_1)
1.144 + edge [loop above] node {$a$} ();
1.145 + \path[->]
1.146 + (q_0) edge node {$a$} (q_1)
1.147 + (q_1) edge node {$b$} (q_2)
1.148 + (q_2) edge node {$b$} (q_0);
1.149 + \draw[->] (q_2) .. controls +(up:1cm) and +(right:1cm) .. node[above] {$a$} (q_1);
1.150 + \end{tikzpicture} \color{red}
1.151 + }
1.152 + \color{black}
1.153 +}
1.154 +\hspace{10pt}
1.155 +\visible<3->{
1.156 + \subfigure[Complement automaton]
1.157 + {
1.158 + \label{fig:complement automaton}
1.159 + \begin{tikzpicture}[shorten >=1pt, node distance=2cm, auto, semithick, >=stealth
1.160 + ,accepting/.style={fill, gray!50!black, text=white}]
1.161 + \node[state, initial, initial text=] (q_0) {$q_0$};
1.162 + \node[state, accepting] (q_1) [above right of= q_0] {$q_1$};
1.163 + \node[state, accepting](q_2) [below right of= q_1] {$q_2$};
1.164 + \path[->]
1.165 + (q_0) edge node {$a$} (q_1)
1.166 + edge node {$b$} (q_2)
1.167 + edge [loop above] node {$a, b$} ()
1.168 + (q_1) edge [loop above] node {$a$} ()
1.169 + (q_2)
1.170 + edge [loop above] node {$b$} ();
1.171 + \end{tikzpicture}\color{green}
1.172 + }
1.173 +\color{black}
1.174 +}
1.175 +%\caption{Automata from Example \ref{ex:automaton}}
1.176 +\end{figure}
1.177 +\end{frame}
1.178 +
1.179 +\begin{frame}
1.180 +\frametitle{Automata}
1.181 \framesubtitle{Definition}
1.182 \begin{def:buechi automata}
1.183 A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$ with:
1.184 @@ -176,7 +342,7 @@
1.185
1.186 \begin{frame}
1.187 \frametitle{Linear Temporal Logic}
1.188 -\framesubtitle{A bit more information about this}
1.189 +\framesubtitle{Motivation}
1.190 \end{frame}
1.191
1.192 \begin{frame}