| author | Christian Urban <urbanc@in.tum.de> | 
| Thu, 03 Aug 2017 01:21:19 +0100 | |
| changeset 498 | cd2d192775a4 | 
| parent 445 | e7d0157f0471 | 
| child 500 | 91b888c91d73 | 
| permissions | -rw-r--r-- | 
| 25 | 1  | 
\documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
2  | 
\usepackage{../slides}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
3  | 
\usepackage{../graphics}
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
4  | 
\usepackage{../langs}
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
5  | 
\usepackage{../data}
 | 
| 25 | 6  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
7  | 
\hfuzz=220pt  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
8  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
9  | 
\pgfplotsset{compat=1.11}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
10  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
11  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}  
 | 
| 25 | 12  | 
|
13  | 
% beamer stuff  | 
|
| 445 | 14  | 
\renewcommand{\slidecaption}{CFL 03, King's College London}
 | 
| 25 | 15  | 
|
16  | 
\begin{document}
 | 
|
17  | 
||
18  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
19  | 
\begin{frame}[t]
 | 
| 25 | 20  | 
\frametitle{%
 | 
21  | 
  \begin{tabular}{@ {}c@ {}}
 | 
|
22  | 
\\[-3mm]  | 
|
| 445 | 23  | 
\LARGE Compilers and \\[-2mm]  | 
| 25 | 24  | 
\LARGE Formal Languages (3)\\[3mm]  | 
25  | 
  \end{tabular}}
 | 
|
26  | 
||
27  | 
\normalsize  | 
|
28  | 
  \begin{center}
 | 
|
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
29  | 
  \begin{tabular}{lp{8cm}}
 | 
| 25 | 30  | 
Email: & christian.urban at kcl.ac.uk\\  | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
31  | 
Office: & S1.27 (1st floor Strand Building)\\  | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
32  | 
Slides: & KEATS (also home work and coursework is there)\\  | 
| 25 | 33  | 
  \end{tabular}
 | 
34  | 
  \end{center}
 | 
|
35  | 
||
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
36  | 
\end{frame}
 | 
| 445 | 37  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
38  | 
||
39  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
40  | 
\begin{frame}[c]
 | 
|
41  | 
\frametitle{Scala Book, Exams}
 | 
|
42  | 
||
43  | 
\begin{itemize}
 | 
|
44  | 
\item www.inf.kcl.ac.uk/~urbanc/ProgInScala2ed.pdf  | 
|
45  | 
\item homeworks (exam 80\%)  | 
|
46  | 
\item coursework (20\%)  | 
|
47  | 
\end{itemize}
 | 
|
48  | 
||
49  | 
\end{frame}
 | 
|
50  | 
%%%%%%%%%%%  | 
|
| 25 | 51  | 
|
52  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
53  | 
\begin{frame}[c]
 | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
54  | 
\frametitle{Regular Expressions}
 | 
| 25 | 55  | 
|
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
56  | 
In programming languages they are often used to recognise:\medskip  | 
| 25 | 57  | 
|
58  | 
\begin{itemize}
 | 
|
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
59  | 
\item symbols, digits  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
60  | 
\item identifiers  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
61  | 
\item numbers (non-leading zeros)  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
62  | 
\item keywords  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
63  | 
\item comments  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
64  | 
\end{itemize}\bigskip
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
65  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
66  | 
\mbox{}\hfill\bl{\url{http://www.regexper.com}}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
67  | 
\end{frame}
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
68  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
69  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
70  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
71  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
72  | 
\begin{frame}[c]
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
73  | 
\frametitle{Last Week}
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
74  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
75  | 
Last week I showed you a regular expression matcher  | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
76  | 
that works provably correct in all cases (we only  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
77  | 
started with the proving part though)  | 
| 25 | 78  | 
|
79  | 
\begin{center}
 | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
80  | 
\bl{$matches\,s\,r$} \;\;if and only if \;\; \bl{$s \in L(r)$}
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
81  | 
\end{center}\bigskip\bigskip 
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
82  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
83  | 
\small  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
84  | 
\textcolor{gray}{\mbox{}\hfill{}by Janusz Brzozowski (1964)}
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
85  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
86  | 
\end{frame}
 | 
| 25 | 87  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
88  | 
||
89  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
90  | 
\begin{frame}[c]
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
91  | 
\frametitle{The Derivative of a Rexp}
 | 
| 25 | 92  | 
|
93  | 
\begin{center}
 | 
|
94  | 
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
 | 
|
| 445 | 95  | 
  \bl{$der\, c\, (\ZERO)$}      & \bl{$\dn$} & \bl{$\ZERO$} & \\
 | 
96  | 
  \bl{$der\, c\, (\ONE)$}           & \bl{$\dn$} & \bl{$\ZERO$} & \\
 | 
|
97  | 
  \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\ONE$ else $\ZERO$} & \\
 | 
|
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
98  | 
  \bl{$der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
99  | 
  \bl{$der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
100  | 
  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
101  | 
  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
102  | 
  \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\medskip\\
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
103  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
104  | 
  \bl{$\textit{ders}\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
105  | 
  \bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\
 | 
| 25 | 106  | 
  \end{tabular}
 | 
107  | 
\end{center}
 | 
|
108  | 
||
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
109  | 
\end{frame}
 | 
| 25 | 110  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
111  | 
||
112  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
113  | 
\begin{frame}[c]
 | 
|
114  | 
||
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
115  | 
Input: string \bl{$abc$} and regular expression \bl{$r$} 
 | 
| 25 | 116  | 
|
117  | 
\begin{enumerate}
 | 
|
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
118  | 
\item \bl{$der\,a\,r$}
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
119  | 
\item \bl{$der\,b\,(der\,a\,r)$}
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
120  | 
\item \bl{$der\,c\,(der\,b\,(der\,a\,r))$}\bigskip\pause
 | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
121  | 
\item finally check whether the last regular expression can match the empty string  | 
| 25 | 122  | 
\end{enumerate}
 | 
123  | 
||
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
124  | 
\end{frame}
 | 
| 25 | 125  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
126  | 
||
127  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
128  | 
\begin{frame}[c]
 | 
|
129  | 
||
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
130  | 
We proved already  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
131  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
132  | 
\begin{center}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
133  | 
\bl{$nullable(r)$} \;if and only if\;  \bl{$[] \in L(r)$}
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
134  | 
\end{center}
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
135  | 
|
| 445 | 136  | 
by induction on the regular expression \bl{$r$}.\bigskip\pause
 | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
137  | 
|
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
138  | 
\begin{center}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
139  | 
{\huge\bf\alert{Any Questions?}}
 | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
140  | 
\end{center}
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
141  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
142  | 
\end{frame}
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
143  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
144  | 
|
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
145  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
146  | 
\begin{frame}[c]
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
147  | 
|
| 25 | 148  | 
We need to prove  | 
149  | 
||
150  | 
\begin{center}
 | 
|
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
151  | 
\bl{$L(der\,c\,r) = Der\,c\,(L(r))$}
 | 
| 25 | 152  | 
\end{center}
 | 
153  | 
||
| 445 | 154  | 
also by induction on the regular expression \bl{$r$}.
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
155  | 
\end{frame}
 | 
| 25 | 156  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
157  | 
||
158  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
159  | 
\begin{frame}[c]
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
160  | 
\frametitle{Proofs about Rexps}
 | 
| 25 | 161  | 
|
162  | 
\begin{itemize}
 | 
|
| 445 | 163  | 
\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
164  | 
\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
165  | 
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
166  | 
\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
167  | 
holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
168  | 
\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
169  | 
holds for \bl{$r$}.
 | 
| 25 | 170  | 
\end{itemize}
 | 
171  | 
||
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
172  | 
\end{frame}
 | 
| 25 | 173  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
174  | 
||
175  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
176  | 
\begin{frame}[c]
 | 
|
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
177  | 
\frametitle{\begin{tabular}{c}Proofs about Natural\\[-1mm] Numbers and Strings\end{tabular}}
 | 
| 25 | 178  | 
|
179  | 
\begin{itemize}
 | 
|
180  | 
\item \bl{$P$} holds for \bl{$0$} and
 | 
|
181  | 
\item \bl{$P$} holds for \bl{$n + 1$} under the assumption that \bl{$P$} already
 | 
|
182  | 
holds for \bl{$n$}
 | 
|
183  | 
\end{itemize}\bigskip
 | 
|
184  | 
||
185  | 
\begin{itemize}
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
186  | 
\item \bl{$P$} holds for \bl{$[]$} and
 | 
| 25 | 187  | 
\item \bl{$P$} holds for \bl{$c\!::\!s$} under the assumption that \bl{$P$} already
 | 
188  | 
holds for \bl{$s$}
 | 
|
189  | 
\end{itemize}
 | 
|
190  | 
||
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
191  | 
\end{frame}
 | 
| 25 | 192  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
193  | 
||
194  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
195  | 
\begin{frame}[t]
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
196  | 
\frametitle{Regular Expressions}
 | 
| 25 | 197  | 
|
198  | 
\begin{center}
 | 
|
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
199  | 
   \begin{tabular}{@ {}rrl@ {\hspace{13mm}}l}
 | 
| 445 | 200  | 
  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}  & null\\
 | 
201  | 
         & \bl{$\mid$} & \bl{$\ONE$}        & empty string / "" / $[]$\\
 | 
|
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
202  | 
         & \bl{$\mid$} & \bl{$c$}                         & character\\
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
203  | 
         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
204  | 
         & \bl{$\mid$} & \bl{$r_1 + r_2$}  & alternative / choice\\
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
205  | 
         & \bl{$\mid$} & \bl{$r^*$}                   & star (zero or more)\\
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
206  | 
  \end{tabular}
 | 
| 25 | 207  | 
  \end{center}
 | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
208  | 
|
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
209  | 
How about ranges \bl{$[a\mbox{-}z]$}, \bl{$r^+$} and \bl{$\sim{}r$}? Do they increase the
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
210  | 
set of languages we can recognise?  | 
| 25 | 211  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
212  | 
\end{frame}
 | 
| 25 | 213  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
214  | 
||
215  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
216  | 
\begin{frame}[c]
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
217  | 
\frametitle{Negation of Regular Expr's}
 | 
| 25 | 218  | 
|
219  | 
\begin{itemize}
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
220  | 
\item \bl{$\sim{}r$}  \hspace{6mm} (everything that \bl{$r$} cannot recognise)\medskip
 | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
221  | 
\item \bl{$L(\sim{}r) \dn UNIV - L(r)$}\medskip
 | 
| 
136
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
222  | 
\item \bl{$nullable (\sim{}r) \dn not\, (nullable(r))$}\medskip
 | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
223  | 
\item \bl{$der\,c\,(\sim{}r) \dn \;\sim{}(der\,c\,r)$}
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
224  | 
\end{itemize}\bigskip\pause
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
225  | 
|
| 
136
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
226  | 
Used often for recognising comments:  | 
| 
134
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
227  | 
|
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
228  | 
\[  | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
229  | 
\bl{/ \cdot * \cdot (\sim{}([a\mbox{-}z]^* \cdot * \cdot / \cdot [a\mbox{-}z]^*)) \cdot * \cdot /}
 | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
230  | 
\]  | 
| 
 
e3a8cf96f570
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
133 
diff
changeset
 | 
231  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
232  | 
\end{frame}
 | 
| 25 | 233  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
234  | 
||
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
235  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
236  | 
\begin{frame}[c]
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
237  | 
\frametitle{Negation}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
238  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
239  | 
Assume you have an alphabet consisting of the letters \bl{$a$}, \bl{$b$} and \bl{$c$} only.
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
240  | 
Find a (basic!) regular expression that matches all strings \emph{\alert{except}} 
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
241  | 
\bl{$ab$} and \bl{$ac$}!
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
242  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
243  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
244  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
245  | 
|
| 25 | 246  | 
|
247  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
248  | 
%\mode<presentation>{
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
249  | 
%\begin{frame}[c]
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
250  | 
%\frametitle{\begin{tabular}{c}Regular Exp's for Lexing\end{tabular}}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
251  | 
%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
252  | 
%Lexing separates strings into ``words'' / components.  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
253  | 
%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
254  | 
%\begin{itemize}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
255  | 
%\item Identifiers (non-empty strings of letters or digits, starting with a letter)  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
256  | 
%\item Numbers (non-empty sequences of digits omitting leading zeros)  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
257  | 
%\item Keywords (else, if, while, \ldots)  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
258  | 
%\item White space (a non-empty sequence of blanks, newlines and tabs)  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
259  | 
%\item Comments  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
260  | 
%\end{itemize}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
261  | 
%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
262  | 
%\end{frame}}
 | 
| 25 | 263  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
264  | 
||
265  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
266  | 
\begin{frame}[c]
 | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
267  | 
\frametitle{Automata}
 | 
| 25 | 268  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
269  | 
A \alert{\bf deterministic finite automaton}, DFA, consists of:
 | 
| 25 | 270  | 
|
271  | 
\begin{itemize}
 | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
272  | 
\item a set of states \bl{$Q$}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
273  | 
\item one of these states is the start state \bl{$q_0$}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
274  | 
\item some states are accepting states \bl{$F$}, and
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
275  | 
\item there is transition function \bl{$\delta$}\bigskip 
 | 
| 25 | 276  | 
|
277  | 
\small  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
278  | 
which takes a state as argument and a character and produces a  | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
279  | 
new state; this function might not be everywhere defined  | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
280  | 
\end{itemize}
 | 
| 
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
281  | 
|
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
282  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
283  | 
\bl{$A(Q, q_0, F, \delta)$}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
284  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
285  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
286  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
287  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
288  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
289  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
290  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
291  | 
\begin{frame}[c]
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
292  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
293  | 
\begin{center}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
294  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
295  | 
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
296  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
297  | 
\node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
298  | 
\node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
299  | 
\node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
300  | 
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
301  | 
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
302  | 
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
303  | 
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
304  | 
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
305  | 
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
306  | 
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
307  | 
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
308  | 
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
309  | 
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
310  | 
\end{tikzpicture}
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
311  | 
\end{center}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
312  | 
|
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
313  | 
|
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
314  | 
\begin{itemize}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
315  | 
\item the start state can be an accepting state  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
316  | 
\item it is possible that there is no accepting state  | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
317  | 
\item all states might be accepting (but this does not necessarily mean all strings are accepted)  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
318  | 
\end{itemize}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
319  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
320  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
321  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
322  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
323  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
324  | 
\begin{frame}[c]
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
325  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
326  | 
\begin{center}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
327  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
328  | 
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
329  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
330  | 
\node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
331  | 
\node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
332  | 
\node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
333  | 
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
334  | 
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
335  | 
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
336  | 
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
337  | 
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
338  | 
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
339  | 
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
340  | 
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
341  | 
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
342  | 
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
343  | 
\end{tikzpicture}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
344  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
345  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
346  | 
for this automaton \bl{$\delta$} is the function\\
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
347  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
348  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
349  | 
\begin{tabular}{lll}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
350  | 
\bl{$(q_0, a) \rightarrow q_1$} & \bl{$(q_1, a) \rightarrow q_4$} & \bl{$(q_4, a) \rightarrow q_4$}\\
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
351  | 
\bl{$(q_0, b) \rightarrow q_2$} & \bl{$(q_1, b) \rightarrow q_2$} & \bl{$(q_4, b) \rightarrow q_4$}\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
352  | 
\end{tabular}\ldots
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
353  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
354  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
355  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
356  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
357  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
358  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
359  | 
\begin{frame}[t]
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
360  | 
\frametitle{Accepting a String}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
361  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
362  | 
Given  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
363  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
364  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
365  | 
\bl{$A(Q, q_0, F, \delta)$}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
366  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
367  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
368  | 
you can define  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
369  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
370  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
371  | 
\begin{tabular}{l}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
372  | 
\bl{$\hat{\delta}(q, []) \dn q$}\\
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
373  | 
\bl{$\hat{\delta}(q, c::s) \dn \hat{\delta}(\delta(q, c), s)$}\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
374  | 
\end{tabular}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
375  | 
\end{center}\pause
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
376  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
377  | 
Whether a string \bl{$s$} is accepted by \bl{$A$}?
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
378  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
379  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
380  | 
\hspace{5mm}\bl{$\hat{\delta}(q_0, s) \in F$}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
381  | 
\end{center}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
382  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
383  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
384  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
385  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
386  | 
\begin{frame}[c]
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
387  | 
\frametitle{Regular Languages}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
388  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
389  | 
A \alert{\bf language} is a set of strings.\bigskip
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
390  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
391  | 
A \alert{\bf regular expression} specifies a language.\bigskip
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
392  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
393  | 
A language is \alert{\bf regular} iff there exists
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
394  | 
a regular expression that recognises all its strings.\bigskip\bigskip\pause  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
395  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
396  | 
not all languages are regular, e.g.~\bl{$a^nb^n$} is not
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
397  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
398  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
399  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
400  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
401  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
402  | 
\frametitle{Regular Languages (2)}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
403  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
404  | 
A language is \alert{\bf regular} iff there exists a regular
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
405  | 
expression that recognises all its strings.\bigskip\medskip  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
406  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
407  | 
or {\bf equivalently}\bigskip\medskip
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
408  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
409  | 
A language is \alert{\bf regular} iff there exists a
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
410  | 
deterministic finite automaton that recognises all its  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
411  | 
strings.  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
412  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
413  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
414  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
415  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
416  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
417  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
418  | 
\begin{frame}[c]
 | 
| 
348
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
419  | 
\frametitle{\begin{tabular}{c}
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
420  | 
Non-Deterministic\\[-1mm]  | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
421  | 
              Finite Automata\end{tabular}}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
422  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
423  | 
A non-deterministic finite automaton consists again of:  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
424  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
425  | 
\begin{itemize}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
426  | 
\item a finite set of states  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
427  | 
\item one of these states is the start state  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
428  | 
\item some states are accepting states, and  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
429  | 
\item there is transition \alert{relation}\medskip 
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
430  | 
\end{itemize}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
431  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
432  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
433  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
434  | 
\begin{tabular}{c}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
435  | 
\bl{$(q_1, a) \rightarrow q_2$}\\
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
436  | 
\bl{$(q_1, a) \rightarrow q_3$}\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
437  | 
\end{tabular}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
438  | 
\hspace{10mm}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
439  | 
\begin{tabular}{c}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
440  | 
\bl{$(q_1, \epsilon) \rightarrow q_2$}\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
441  | 
\end{tabular}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
442  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
443  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
444  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
445  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
446  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
447  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
448  | 
\begin{frame}[c]
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
449  | 
\frametitle{Two NFA Examples}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
450  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
451  | 
\small  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
452  | 
\begin{center}
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
453  | 
\begin{tabular}[t]{c@{\hspace{9mm}}c}
 | 
| 
136
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
454  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
455  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
456  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
457  | 
\node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
458  | 
\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
459  | 
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
460  | 
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
461  | 
\path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
462  | 
\path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
463  | 
\path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
464  | 
\end{tikzpicture} &
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
465  | 
|
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
466  | 
\raisebox{20mm}{
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
467  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
468  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
469  | 
\node[state,initial]  (r_1)  {$r_1$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
470  | 
\node[state] (r_2) [above=of r_1] {$r_2$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
471  | 
\node[state, accepting] (r_3) [right=of r_1] {$r_3$};
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
472  | 
\path[->] (r_1) edge node [below]  {\alert{$b$}} (r_3);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
473  | 
\path[->] (r_2) edge [bend left] node [above]  {\alert{$a$}} (r_3);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
474  | 
\path[->] (r_1) edge [bend left] node  [left] {\alert{$\epsilon$}} (r_2);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
475  | 
\path[->] (r_2) edge [bend left] node  [right] {\alert{$a$}} (r_1);
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
476  | 
\end{tikzpicture}}
 | 
| 
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
477  | 
\end{tabular}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
478  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
479  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
480  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
481  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
482  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
483  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
484  | 
\begin{frame}[c]
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
485  | 
\frametitle{Rexp to NFA}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
486  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
487  | 
\begin{center}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
488  | 
\begin{tabular}[t]{l@{\hspace{10mm}}l}
 | 
| 445 | 489  | 
\raisebox{1mm}{\bl{$\ZERO$}} & 
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
490  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
491  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
492  | 
\end{tikzpicture}\\\\
 | 
| 445 | 493  | 
\raisebox{1mm}{\bl{$\ONE$}} & 
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
494  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
495  | 
\node[state, initial, accepting]  (q_0)  {$\mbox{}$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
496  | 
\end{tikzpicture}\\\\
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
497  | 
\raisebox{2mm}{\bl{$c$}} & 
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
498  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
499  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
500  | 
\node[state, accepting]  (q_1)  [right=of q_0] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
501  | 
\path[->] (q_0) edge node [below]  {\alert{$c$}} (q_1);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
502  | 
\end{tikzpicture}\\\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
503  | 
\end{tabular}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
504  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
505  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
506  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
507  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
508  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
509  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
510  | 
\begin{frame}[t]
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
511  | 
\frametitle{Case $r_1\cdot r_2$}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
512  | 
|
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
513  | 
\mbox{}\bigskip
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
514  | 
\onslide<1>{By recursion we are given two automata:\bigskip}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
515  | 
|
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
516  | 
{\centering\begin{tikzpicture}[node distance=3mm,
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
517  | 
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
518  | 
\node[state, initial]  (q_0)  {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
519  | 
\node (r_1)  [right=of q_0] {$\ldots$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
520  | 
\only<1>{
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
521  | 
\node[state, accepting]  (t_1)  [right=of r_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
522  | 
\node[state, accepting]  (t_2)  [above=of t_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
523  | 
\node[state, accepting]  (t_3)  [below=of t_1] {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
524  | 
\only<2>{
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
525  | 
\node[state]  (t_1)  [right=of r_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
526  | 
\node[state]  (t_2)  [above=of t_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
527  | 
\node[state]  (t_3)  [below=of t_1] {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
528  | 
\only<1>{\node[state, initial]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
529  | 
\only<2>{\node[state]  (a_0)  [right=2.5cm of t_1] {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
530  | 
\node (b_1)  [right=of a_0] {$\ldots$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
531  | 
\node[state, accepting]  (c_1)  [right=of b_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
532  | 
\node[state, accepting]  (c_2)  [above=of c_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
533  | 
\node[state, accepting]  (c_3)  [below=of c_1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
534  | 
\only<2>{
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
535  | 
\path[->] (t_1) edge node [above, pos=0.3]  {\alert{$\epsilon$}} (a_0);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
536  | 
\path[->] (t_2) edge node [above]  {\alert{$\epsilon$}} (a_0);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
537  | 
\path[->] (t_3) edge node [below]  {\alert{$\epsilon$}} (a_0);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
538  | 
}  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
539  | 
\begin{pgfonlayer}{background}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
540  | 
\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (r_1) (t_1) (t_2) (t_3)] {};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
541  | 
\only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (a_0) (b_1) (c_1) (c_2) (c_3)] {};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
542  | 
\only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (q_0) (c_1) (c_2) (c_3)] {};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
543  | 
\only<1>{\node [yshift=2mm] at (1.north) {\bl{$r_1$}};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
544  | 
\only<1>{\node [yshift=2mm] at (2.north) {\bl{$r_2$}};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
545  | 
\only<2>{\node [yshift=2mm] at (3.north) {\bl{$r_1\cdot r_2$}};}
 | 
| 
143
 
e3fd4c5995ef
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
139 
diff
changeset
 | 
546  | 
\end{pgfonlayer}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
547  | 
\end{tikzpicture}}\bigskip\bigskip
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
548  | 
|
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
549  | 
\small  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
550  | 
We need to (1) change the accepting nodes of the first automaton into non-accepting nodes, and (2) connect them  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
551  | 
via $\epsilon$-transitions to the starting state of the second automaton.  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
552  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
553  | 
\end{frame}
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
554  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
555  | 
|
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
556  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
557  | 
\begin{frame}[t]
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
558  | 
\frametitle{Case $r_1+ r_2$}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
559  | 
\mbox{}\\[-10mm]
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
560  | 
|
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
561  | 
\onslide<1>{By recursion we are given two automata:\smallskip}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
562  | 
|
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
563  | 
\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
564  | 
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
565  | 
\onslide<1>{\node at (0,0)  (1)  {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
566  | 
\onslide<2>{\node at (0,0) [state, initial]  (1)  {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
567  | 
\only<1>{
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
568  | 
\node[state, initial]  (2)  [above right=16mm of 1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
569  | 
\node[state, initial]  (3)  [below right=16mm of 1] {$\mbox{}$};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
570  | 
\only<2>{
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
571  | 
\node[state]  (2)  [above right=16mm of 1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
572  | 
\node[state]  (3)  [below right=16mm of 1] {$\mbox{}$};}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
573  | 
|
| 
137
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
574  | 
\node (a)  [right=of 2] {$\ldots$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
575  | 
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
576  | 
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
577  | 
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
578  | 
|
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
579  | 
\node (b)  [right=of 3] {$\ldots$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
580  | 
\node[state, accepting]  (b1)  [right=of b] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
581  | 
\node[state, accepting]  (b2)  [above=of b1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
582  | 
\node[state, accepting]  (b3)  [below=of b1] {$\mbox{}$};
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
583  | 
\only<2>{
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
584  | 
\path[->] (1) edge node [above]  {\alert{$\epsilon$}} (2);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
585  | 
\path[->] (1) edge node [below]  {\alert{$\epsilon$}} (3);
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
586  | 
}  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
587  | 
\begin{pgfonlayer}{background}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
588  | 
\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
589  | 
\only<1>{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (3) (b1) (b2) (b3)] {};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
590  | 
\only<2>{\node (3) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3) (b2) (b3)] {};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
591  | 
\only<1>{\node [yshift=3mm] at (1.north) {\bl{$r_1$}};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
592  | 
\only<1>{\node [yshift=3mm] at (2.north) {\bl{$r_2$}};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
593  | 
\only<2>{\node [yshift=3mm] at (3.north) {\bl{$r_1+ r_2$}};}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
594  | 
\end{pgfonlayer}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
595  | 
\end{tikzpicture}
 | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
596  | 
|
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
597  | 
\small  | 
| 
 
69cec773736b
added pictures
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
136 
diff
changeset
 | 
598  | 
We (1) need to introduce a new starting state and (2) connect it to the original two starting states.  | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
599  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
600  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
601  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
602  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
603  | 
\begin{frame}[c]
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
604  | 
\frametitle{Case $r^*$}
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
605  | 
|
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
606  | 
\onslide<1>{By recursion we are given an automaton for $r$:\smallskip}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
607  | 
|
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
608  | 
\hspace{2cm}\begin{tikzpicture}[node distance=3mm,
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
609  | 
                             >=stealth',very thick, every state/.style={minimum size=3pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
610  | 
\onslide<1>{\node at (0,0)  (1)  {$\mbox{}$};}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
611  | 
\onslide<2->{\node at (0,0) [state, initial,accepting]  (1)  {$\mbox{}$};}
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
612  | 
\only<1>{\node[state, initial]  (2)  [right=16mm of 1] {$\mbox{}$};}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
613  | 
\only<2->{\node[state]  (2)  [right=16mm of 1] {$\mbox{}$};}
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
614  | 
\node (a)  [right=of 2] {$\ldots$};
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
615  | 
\only<1>{
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
616  | 
\node[state, accepting]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
617  | 
\node[state, accepting]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
618  | 
\node[state, accepting]  (a3)  [below=of a1] {$\mbox{}$};}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
619  | 
\only<2->{
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
620  | 
\node[state]  (a1)  [right=of a] {$\mbox{}$};
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
621  | 
\node[state]  (a2)  [above=of a1] {$\mbox{}$};
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
622  | 
\node[state]  (a3)  [below=of a1] {$\mbox{}$};}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
623  | 
\only<2->{
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
624  | 
\path[->] (1) edge node [above]  {\alert{$\epsilon$}} (2);
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
625  | 
\path[->] (a1) edge [bend left=45] node [above]  {\alert{$\epsilon$}} (1);
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
626  | 
\path[->] (a2) edge [bend right] node [below]  {\alert{$\epsilon$}} (1);
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
627  | 
\path[->] (a3) edge [bend left=45] node [below]  {\alert{$\epsilon$}} (1);
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
628  | 
|
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
629  | 
}  | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
630  | 
\begin{pgfonlayer}{background}
 | 
| 
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
631  | 
\only<1>{\node (1) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (2) (a1) (a2) (a3)] {};}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
632  | 
\only<2->{\node (2) [rounded corners, inner sep=1mm, thick, draw=black!60, fill=black!20, fit= (1) (a2) (a3)] {};}
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
633  | 
\only<1>{\node [yshift=3mm] at (1.north) {\bl{$r$}};}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
634  | 
\only<2->{\node [yshift=3mm] at (2.north) {\bl{$r^*$}};}
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
635  | 
\end{pgfonlayer}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
636  | 
\end{tikzpicture}\bigskip
 | 
| 
138
 
b98a0a49c432
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
137 
diff
changeset
 | 
637  | 
|
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
638  | 
\onslide<3->{
 | 
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
639  | 
Why can't we just have an epsilon transition from the accepting states to the starting state?}  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
640  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
641  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
642  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
643  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
644  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
645  | 
\begin{frame}[c]
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
646  | 
\frametitle{Subset Construction}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
647  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
648  | 
|
| 
136
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
649  | 
\begin{textblock}{5}(1,1)
 | 
| 
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
650  | 
\begin{center}
 | 
| 
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
651  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
652  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
653  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
654  | 
\node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
655  | 
\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
656  | 
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
657  | 
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
658  | 
\path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
659  | 
\path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
143 
diff
changeset
 | 
660  | 
\path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
136
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
661  | 
\end{tikzpicture}
 | 
| 
 
cc19e6cbcb68
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
135 
diff
changeset
 | 
662  | 
\end{center}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
663  | 
\end{textblock}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
664  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
665  | 
\begin{textblock}{11}(6.5,4.5)
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
666  | 
\begin{tabular}{r|cl}
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
667  | 
nodes \textcolor{white}{*} & $a$ & $b$\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
668  | 
\hline  | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
669  | 
$\{\}$ \textcolor{white}{*} & \onslide<2->{$\{\}$} & \onslide<2->{$\{\}$}\\
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
670  | 
$\{0\}$ \textcolor{white}{*} & \onslide<3->{$\{0,1,2\}$} & \onslide<3->{$\{2\}$}\\
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
671  | 
$\{1\}$ \textcolor{white}{*} & \onslide<3->{$\{1\}$} & \onslide<3->{$\{\}$}\\
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
672  | 
$\{2\}$ \onslide<5->{*} & \onslide<3->{$\{\}$} & \onslide<3->{$\{2\}$}\\
 | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
673  | 
$\{0,1\}$ \textcolor{white}{*} &\onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
674  | 
$\{0,2\}$ \onslide<5->{*} &\onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
675  | 
$\{1,2\}$ \onslide<5->{*} & \onslide<4->{$\{1\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
676  | 
\onslide<5->{s:} $\{0,1,2\}$ \onslide<5->{*}& \onslide<4->{$\{0,1,2\}$} & \onslide<4->{$\{2\}$}\\
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
677  | 
\end{tabular}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
678  | 
\end{textblock}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
679  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
680  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
681  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
682  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
683  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
684  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
685  | 
\frametitle{The Result}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
686  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
687  | 
\footnotesize  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
688  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
689  | 
\begin{tikzpicture}[scale=0.5,>=stealth',very thick,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
690  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
691  | 
draw=blue!50,very thick,fill=blue!20},  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
692  | 
baseline=0mm]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
693  | 
\node[state,initial,accepting]  (q012)  {$\{0,1,2\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
694  | 
\node[state,accepting] (q02) [right=of q012] {$\{0,2\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
695  | 
\node[state] (q01) [above=of q02] {$\{0,1\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
696  | 
\node[state,accepting] (q12) [below=of q02] {$\{1,2\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
697  | 
\node[state] (q0) [right=2cm of q01] {$\{0\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
698  | 
\node[state] (q1) [right=2.5cm of q02] {$\{1\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
699  | 
\node[state,accepting] (q2) [right=1.5cm of q12] {$\{2\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
700  | 
\node[state] (qn) [right=of q1] {$\{\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
701  | 
|
| 
348
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
702  | 
\path[->] (q012) edge [loop below] node  {\alert{$a$}} ();
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
703  | 
\path[->] (q012) edge node [above]  {\alert{$b$}} (q2);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
704  | 
\path[->] (q12) edge [bend left] node [below,pos=0.4]  {\alert{$a$}} (q1);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
705  | 
\path[->] (q12) edge node [below]  {\alert{$b$}} (q2);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
706  | 
\path[->] (q02) edge node [above]  {\alert{$a$}} (q012);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
707  | 
\path[->] (q02) edge [bend left] node [above, pos=0.8]  {\alert{$b$}} (q2);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
708  | 
\path[->] (q01) edge node [below]  {\alert{$a$}} (q012);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
709  | 
\path[->] (q01) edge [bend left] node [above]  {\alert{$b$}} (q2);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
710  | 
\path[->] (q0) edge node [below]  {\alert{$a$}} (q012);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
711  | 
\path[->] (q0) edge node [right, pos=0.2]  {\alert{$b$}} (q2);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
712  | 
\path[->] (q1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
713  | 
\path[->] (q1) edge node [above]  {\alert{$b$}} (qn);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
714  | 
\path[->] (q2) edge [loop right] node  {\alert{$b$}} ();
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
715  | 
\path[->] (q2) edge node [below]  {\alert{$a$}} (qn);
 | 
| 
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
716  | 
\path[->] (qn) edge [loop above] node  {$\alert{a},\alert{b}$} ();
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
717  | 
\end{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
718  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
719  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
720  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
721  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
722  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
723  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
724  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
725  | 
\begin{frame}[c]
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
726  | 
\frametitle{Removing Dead States}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
727  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
728  | 
\footnotesize  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
729  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
730  | 
\begin{tabular}{ll}
 | 
| 445 | 731  | 
DFA: & (original) NFA:\\  | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
732  | 
\raisebox{10mm}{%
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
733  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
734  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
735  | 
draw=blue!50,very thick,fill=blue!20}]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
736  | 
\node[state,initial,accepting]  (q012)  {$\{0,1,2\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
737  | 
\node[state,accepting] (q2) [right=of q012] {$\{2\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
738  | 
\node[state] (qn) [right=of q2] {$\{\}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
739  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
740  | 
\path[->] (q012) edge [loop below] node  {\alert{$a$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
741  | 
\path[->] (q012) edge node [above]  {\alert{$b$}} (q2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
742  | 
\path[->] (q2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
743  | 
\path[->] (q2) edge node [below]  {\alert{$a$}} (qn);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
744  | 
\path[->] (qn) edge [loop above] node  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
745  | 
   {$\alert{a},\alert{b}$} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
746  | 
\end{tikzpicture}}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
747  | 
&  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
748  | 
\begin{tikzpicture}[scale=0.7,>=stealth',very thick,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
749  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
750  | 
draw=blue!50,very thick,fill=blue!20},]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
751  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
752  | 
\node[state] (q_1) [above=of q_0] {$q_1$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
753  | 
\node[state, accepting] (q_2) [below=of q_0] {$q_2$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
754  | 
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_1);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
755  | 
\path[->] (q_0) edge node [left]  {\alert{$\epsilon$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
756  | 
\path[->] (q_0) edge [loop right] node  {\alert{$a$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
757  | 
\path[->] (q_1) edge [loop above] node  {\alert{$a$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
758  | 
\path[->] (q_2) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
759  | 
\end{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
760  | 
\end{tabular}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
761  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
762  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
763  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
764  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
765  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
766  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
767  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
768  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
769  | 
\begin{frame}[c]
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
770  | 
\frametitle{Regexps and Automata}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
771  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
772  | 
\begin{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
773  | 
\begin{tikzpicture}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
774  | 
\node (rexp)  {\bl{\bf Regexps}};
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
775  | 
\node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
776  | 
\node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
777  | 
\onslide<2->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
778  | 
\path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
779  | 
\path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
780  | 
\onslide<2->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
781  | 
\end{tikzpicture}\\
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
782  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
783  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
784  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
785  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
786  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
787  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
788  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
789  | 
\frametitle{DFA Minimisation}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
790  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
791  | 
\begin{enumerate}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
792  | 
\item Take all pairs \bl{$(q, p)$} with \bl{$q \not= p$}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
793  | 
\item Mark all pairs that accepting and non-accepting states  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
794  | 
\item For  all unmarked pairs \bl{$(q, p)$} and all characters \bl{$c$} test whether
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
795  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
796  | 
\bl{$(\delta(q, c), \delta(p,c))$}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
797  | 
\end{center} 
 | 
| 
348
 
31e89128ccd2
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
346 
diff
changeset
 | 
798  | 
are marked. If yes in at least one case, then also mark \bl{$(q, p)$}.
 | 
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
799  | 
\item Repeat last step until no change.  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
800  | 
\item All unmarked pairs can be merged.  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
801  | 
\end{enumerate}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
802  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
803  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
804  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
805  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
806  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
807  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
808  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
809  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
810  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
811  | 
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
812  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
813  | 
\node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
814  | 
\node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
815  | 
\node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
816  | 
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
817  | 
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
818  | 
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
819  | 
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
820  | 
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
821  | 
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
822  | 
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
823  | 
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
824  | 
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
825  | 
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
826  | 
\end{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
827  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
828  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
829  | 
\mbox{}\\[-20mm]\mbox{}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
830  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
831  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
832  | 
\begin{tikzpicture}[scale=0.8,line width=0.8mm]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
833  | 
\draw (0,0) -- (4,0);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
834  | 
\draw (0,1) -- (4,1);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
835  | 
\draw (0,2) -- (3,2);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
836  | 
\draw (0,3) -- (2,3);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
837  | 
\draw (0,4) -- (1,4);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
838  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
839  | 
\draw (0,0) -- (0, 4);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
840  | 
\draw (1,0) -- (1, 4);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
841  | 
\draw (2,0) -- (2, 3);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
842  | 
\draw (3,0) -- (3, 2);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
843  | 
\draw (4,0) -- (4, 1);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
844  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
845  | 
\draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
846  | 
\draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
847  | 
\draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
848  | 
\draw (3.5,-0.5) node {$q_3$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
849  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
850  | 
\draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
851  | 
\draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
852  | 
\draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
853  | 
\draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
854  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
855  | 
\draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
856  | 
\draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
857  | 
\draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
858  | 
\draw (3.5,0.5) node {\large$\star$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
859  | 
\end{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
860  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
861  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
862  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
863  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
864  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
865  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
866  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
867  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
868  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
869  | 
\begin{tabular}{@{\hspace{-8mm}}cc@{}}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
870  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
871  | 
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
872  | 
\node[state,initial]  (q_0)  {$q_0$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
873  | 
\node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
874  | 
\node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
875  | 
\node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
876  | 
\node[state, accepting] (q_4) [right=of q_1] {$q_4$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
877  | 
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
878  | 
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
879  | 
\path[->] (q_4) edge [loop right] node  {\alert{$a, b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
880  | 
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
881  | 
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
882  | 
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
883  | 
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
884  | 
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
885  | 
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
886  | 
\end{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
887  | 
&  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
888  | 
\raisebox{9mm}{\begin{tikzpicture}[scale=0.6,line width=0.8mm]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
889  | 
\draw (0,0) -- (4,0);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
890  | 
\draw (0,1) -- (4,1);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
891  | 
\draw (0,2) -- (3,2);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
892  | 
\draw (0,3) -- (2,3);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
893  | 
\draw (0,4) -- (1,4);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
894  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
895  | 
\draw (0,0) -- (0, 4);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
896  | 
\draw (1,0) -- (1, 4);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
897  | 
\draw (2,0) -- (2, 3);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
898  | 
\draw (3,0) -- (3, 2);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
899  | 
\draw (4,0) -- (4, 1);  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
900  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
901  | 
\draw (0.5,-0.5) node {$q_0$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
902  | 
\draw (1.5,-0.5) node {$q_1$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
903  | 
\draw (2.5,-0.5) node {$q_2$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
904  | 
\draw (3.5,-0.5) node {$q_3$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
905  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
906  | 
\draw (-0.5, 3.5) node {$q_1$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
907  | 
\draw (-0.5, 2.5) node {$q_2$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
908  | 
\draw (-0.5, 1.5) node {$q_3$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
909  | 
\draw (-0.5, 0.5) node {$q_4$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
910  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
911  | 
\draw (0.5,0.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
912  | 
\draw (1.5,0.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
913  | 
\draw (2.5,0.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
914  | 
\draw (3.5,0.5) node {\large$\star$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
915  | 
\draw (0.5,1.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
916  | 
\draw (2.5,1.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
917  | 
\draw (0.5,3.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
918  | 
\draw (1.5,2.5) node {\large$\star$}; 
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
919  | 
\end{tikzpicture}}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
920  | 
\end{tabular}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
921  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
922  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
923  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
924  | 
\mbox{}\\[-20mm]\mbox{}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
925  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
926  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
927  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
928  | 
                             every state/.style={minimum size=0pt,inner sep=2pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
929  | 
\node[state,initial]  (q_02)  {$q_{0, 2}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
930  | 
\node[state] (q_13) [right=of q_02] {$q_{1, 3}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
931  | 
\node[state, accepting] (q_4) [right=of q_13] {$q_{4\phantom{,0}}$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
932  | 
\path[->] (q_02) edge [bend left] node [above]  {\alert{$a$}} (q_13);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
933  | 
\path[->] (q_13) edge [bend left] node [below]  {\alert{$b$}} (q_02);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
934  | 
\path[->] (q_02) edge [loop below] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
935  | 
\path[->] (q_13) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
936  | 
\path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
937  | 
\end{tikzpicture}\\
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
938  | 
minimal automaton  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
939  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
940  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
941  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
942  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
943  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
944  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
945  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
946  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
947  | 
\frametitle{Alternatives}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
948  | 
\mbox{}\\[-17mm]\mbox{}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
949  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
950  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
951  | 
\begin{tikzpicture}[>=stealth',very thick,auto,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
952  | 
                    every state/.style={minimum size=0pt,
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
953  | 
inner sep=2pt,draw=blue!50,very thick,fill=blue!20}]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
954  | 
\only<1>{\node[state,initial]  (q_0)  {$q_0$};}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
955  | 
\only<2->{\node[state,accepting]  (q_0)  {$q_0$};}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
956  | 
\node[state] (q_1) [right=of q_0] {$q_1$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
957  | 
\node[state] (q_2) [below right=of q_0] {$q_2$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
958  | 
\node[state] (q_3) [right=of q_2] {$q_3$};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
959  | 
\only<1>{\node[state, accepting] (q_4) [right=of q_1] {$q_4$};}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
960  | 
\only<2->{\node[state, initial right] (q_4) [right=of q_1] {$q_4$};}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
961  | 
\only<1-2>{
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
962  | 
\path[->] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
963  | 
\path[->] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
964  | 
\path[->] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
965  | 
\path[->] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
966  | 
\path[->] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
967  | 
\path[->] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
968  | 
\path[->] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
969  | 
\path[->] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
970  | 
\path[->] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
971  | 
\only<3->{
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
972  | 
\path[<-] (q_0) edge node [above]  {\alert{$a$}} (q_1);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
973  | 
\path[<-] (q_1) edge node [above]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
974  | 
\path[<-] (q_4) edge [loop above] node  {\alert{$a, b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
975  | 
\path[<-] (q_3) edge node [right]  {\alert{$a$}} (q_4);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
976  | 
\path[<-] (q_2) edge node [above]  {\alert{$a$}} (q_3);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
977  | 
\path[<-] (q_1) edge node [right]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
978  | 
\path[<-] (q_0) edge node [above]  {\alert{$b$}} (q_2);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
979  | 
\path[<-] (q_2) edge [loop left] node  {\alert{$b$}} ();
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
980  | 
\path[<-] (q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (q_0);}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
981  | 
\end{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
982  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
983  | 
\mbox{}\\[-18mm]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
984  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
985  | 
\small  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
986  | 
\begin{itemize}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
987  | 
\item<2-> exchange initial / accepting states\\[-2mm]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
988  | 
\item<3-> reverse all edges\\[-2mm]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
989  | 
\item<4-> subset construction $\Rightarrow$ DFA\\[-2mm]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
990  | 
\item<5-> remove dead states\\[-2mm]  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
991  | 
\item<6-> repeat once more  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
992  | 
          \onslide<6->{$\Rightarrow$ minimal DFA}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
993  | 
\end{itemize}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
994  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
995  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
996  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
997  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
998  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
999  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1000  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1001  | 
\frametitle{Regexps and Automata}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1002  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1003  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1004  | 
\begin{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1005  | 
\node (rexp)  {\bl{\bf Regexps}};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1006  | 
\node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1007  | 
\node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1008  | 
\onslide<1->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1009  | 
\path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1010  | 
\path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1011  | 
\onslide<1->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1012  | 
\onslide<2->{\path[->, red, line width=2mm] (dfa) edge [bend left=45] (rexp);}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1013  | 
\end{tikzpicture}\\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1014  | 
\end{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1015  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1016  | 
\end{frame}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1017  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1018  | 
|
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1019  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1020  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1021  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1022  | 
\begin{frame}<2>[c]
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1023  | 
\frametitle{DFA to Rexp}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1024  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1025  | 
\begin{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1026  | 
\begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1027  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1028  | 
  \only<1>{\node[state, initial]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1029  | 
  \only<2->{\node[state, initial,accepting]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1030  | 
  \only<1>{\node[state]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1031  | 
  \only<2->{\node[state,accepting]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1032  | 
  \only<1>{\node[state, accepting] (q2) at ( 2,1) {$q_2$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1033  | 
  \only<2->{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1034  | 
  \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1035  | 
                  (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1036  | 
                  (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1037  | 
                  (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1038  | 
                  (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1039  | 
                  (q0) edge [loop below] node {\alert{$b$}} ()
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1040  | 
;  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1041  | 
\end{tikzpicture}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1042  | 
\end{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1043  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1044  | 
\onslide<3>{How to get from a DFA to a regular expression?}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1045  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1046  | 
\end{frame}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1047  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1048  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1049  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1050  | 
\begin{frame}[c]
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1051  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1052  | 
\begin{center}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1053  | 
\begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1054  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1055  | 
  \only<1->{\node[state, initial]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1056  | 
  \only<1->{\node[state]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1057  | 
  \only<1->{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1058  | 
  \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1059  | 
                  (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1060  | 
                  (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1061  | 
                  (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1062  | 
                  (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1063  | 
                  (q0) edge [loop below] node {\alert{$b$}} ()
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1064  | 
;  | 
| 
139
 
6e7c3db9023d
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
138 
diff
changeset
 | 
1065  | 
\end{tikzpicture}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1066  | 
\end{center}\pause\bigskip
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1067  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1068  | 
\onslide<2->{
 | 
| 445 | 1069  | 
You know how to solve since school days, no?  | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1070  | 
\begin{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1071  | 
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1072  | 
\bl{$q_0$} & \bl{$=$} & \bl{$2\, q_0 + 3 \,q_1 +  4\, q_2$}\\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1073  | 
\bl{$q_1$} & \bl{$=$} & \bl{$2 \,q_0 + 3\, q_1 + 1\, q_2$}\\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1074  | 
\bl{$q_2$} & \bl{$=$} & \bl{$1\, q_0 + 5\, q_1 + 2\, q_2$}\\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1075  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1076  | 
\end{tabular}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1077  | 
\end{center}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1078  | 
}  | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1079  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1080  | 
\end{frame}
 | 
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1081  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1082  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1083  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1084  | 
\begin{frame}[c]
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1085  | 
|
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1086  | 
\begin{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1087  | 
\begin{tikzpicture}[scale=2,>=stealth',very thick,
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1088  | 
                             every state/.style={minimum size=0pt,draw=blue!50,very thick,fill=blue!20},]
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1089  | 
  \only<1->{\node[state, initial]        (q0) at ( 0,1) {$q_0$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1090  | 
  \only<1->{\node[state]                    (q1) at ( 1,1) {$q_1$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1091  | 
  \only<1->{\node[state] (q2) at ( 2,1) {$q_2$};}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1092  | 
  \path[->] (q0) edge[bend left] node[above] {\alert{$a$}} (q1)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1093  | 
                  (q1) edge[bend left] node[above] {\alert{$b$}} (q0)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1094  | 
                  (q2) edge[bend left=50] node[below] {\alert{$b$}} (q0)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1095  | 
                  (q1) edge node[above] {\alert{$a$}} (q2)
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1096  | 
                  (q2) edge [loop right] node {\alert{$a$}} ()
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1097  | 
                  (q0) edge [loop below] node {\alert{$b$}} ()
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1098  | 
;  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1099  | 
\end{tikzpicture}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1100  | 
\end{center}\bigskip
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1101  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1102  | 
\onslide<2->{
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1103  | 
\begin{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1104  | 
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 | 
| 445 | 1105  | 
\bl{$q_0$} & \bl{$=$} & \bl{$\ONE + q_0\,b + q_1\,b +  q_2\,b$}\\
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1106  | 
\bl{$q_1$} & \bl{$=$} & \bl{$q_0\,a$}\\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1107  | 
\bl{$q_2$} & \bl{$=$} & \bl{$q_1\,a + q_2\,a$}\\
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1108  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1109  | 
\end{tabular}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1110  | 
\end{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1111  | 
}  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1112  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1113  | 
\onslide<3->{
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1114  | 
Arden's Lemma:  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1115  | 
\begin{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1116  | 
If \bl{$q = q\,r + s$}\; then\; \bl{$q = s\, r^*$}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1117  | 
\end{center}
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1118  | 
}  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1119  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1120  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1121  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1122  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1123  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1124  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1125  | 
\frametitle{Regexps and Automata}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1126  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1127  | 
\begin{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1128  | 
\begin{tikzpicture}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1129  | 
\node (rexp)  {\bl{\bf Regexps}};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1130  | 
\node (nfa) [right=of rexp] {\bl{\bf NFAs}};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1131  | 
\node (dfa) [right=of nfa] {\bl{\bf DFAs}};
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1132  | 
\onslide<1->{\node (mdfa) [right=of dfa] {\bl{\bf \begin{tabular}{c}minimal\\ DFAs\end{tabular}}};}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1133  | 
\path[->, red, line width=2mm] (rexp) edge node [above=4mm, black] {\begin{tabular}{c@{\hspace{9mm}}}Thompson's\\[-1mm] construction\end{tabular}} (nfa);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1134  | 
\path[->, red, line width=2mm] (nfa) edge node [above=4mm, black] {\begin{tabular}{c}subset\\[-1mm] construction\end{tabular}}(dfa);
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1135  | 
\onslide<1->{\path[->, red, line width=2mm] (dfa) edge node [below=9mm, black] {minimisation} (mdfa);}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1136  | 
\onslide<1->{\path[->, red, line width=2mm] (dfa) edge [bend left=45] (rexp);}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1137  | 
\end{tikzpicture}\\
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1138  | 
\end{center}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1139  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1140  | 
\end{frame}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1141  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1142  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1143  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1144  | 
\begin{frame}[c]
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1145  | 
\frametitle{Regular Languages (3)}
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1146  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1147  | 
A language is \alert{\bf regular} iff there exists a regular
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1148  | 
expression that recognises all its strings.\bigskip\medskip  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1149  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1150  | 
or {\bf equivalently}\bigskip\medskip
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1151  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1152  | 
A language is \alert{\bf regular} iff there exists a
 | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1153  | 
deterministic finite automaton that recognises all its  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1154  | 
strings.\bigskip\medskip\pause  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1155  | 
|
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1156  | 
Why is every finite set of strings a regular language?  | 
| 
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1157  | 
\end{frame}
 | 
| 
265
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1158  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1159  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1160  | 
|
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1161  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1162  | 
\begin{frame}[c]
 | 
| 
 
332fbe9c91ab
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
1163  | 
|
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1164  | 
Given the function  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1165  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1166  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1167  | 
\bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
 | 
| 445 | 1168  | 
$rev(\ZERO)$ & $\dn$ & $\ZERO$\\  | 
1169  | 
$rev(\ONE)$ & $\dn$ & $\ONE$\\  | 
|
| 
135
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1170  | 
$rev(c)$ & $\dn$ & $c$\\  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1171  | 
$rev(r_1 + r_2)$ & $\dn$ & $rev(r_1) + rev(r_2)$\\  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1172  | 
$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1173  | 
$rev(r^*)$ & $\dn$ & $rev(r)^*$\\  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1174  | 
\end{tabular}}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1175  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1176  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1177  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1178  | 
and the set  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1179  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1180  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1181  | 
\bl{$Rev\,A \dn \{s^{-1} \;|\; s \in A\}$}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1182  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1183  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1184  | 
prove whether  | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1185  | 
|
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1186  | 
\begin{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1187  | 
\bl{$L(rev(r)) = Rev (L(r))$}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1188  | 
\end{center}
 | 
| 
 
72b686e1c974
added slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
134 
diff
changeset
 | 
1189  | 
|
| 
346
 
a98794b11ac4
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
265 
diff
changeset
 | 
1190  | 
\end{frame}
 | 
| 
133
 
09efdf5cf07c
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
93 
diff
changeset
 | 
1191  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 25 | 1192  | 
|
1193  | 
||
1194  | 
\end{document}
 | 
|
1195  | 
||
1196  | 
%%% Local Variables:  | 
|
1197  | 
%%% mode: latex  | 
|
1198  | 
%%% TeX-master: t  | 
|
1199  | 
%%% End:  | 
|
1200  |