summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2017-10-29 16:25:25 (GMT)
committerDavid A. Madore <david+git@madore.org>2017-10-29 16:25:25 (GMT)
commit086b4847f212f6d120ef59b659ed97c71d8fb897 (patch)
tree3bcc259c69e870f977fe4df270375228ccbff348
parentfdf0777a7cbba7fea7969d71aa128c5eb60a265d (diff)
downloadinf105-086b4847f212f6d120ef59b659ed97c71d8fb897.zip
inf105-086b4847f212f6d120ef59b659ed97c71d8fb897.tar.gz
inf105-086b4847f212f6d120ef59b659ed97c71d8fb897.tar.bz2
Describe the Thompson automaton of a regular expression.
-rw-r--r--figs/example9.dot27
-rw-r--r--figs/example9b.dot19
-rw-r--r--notes-inf105.tex255
3 files changed, 293 insertions, 8 deletions
diff --git a/figs/example9.dot b/figs/example9.dot
new file mode 100644
index 0000000..cd3526c
--- /dev/null
+++ b/figs/example9.dot
@@ -0,0 +1,27 @@
+digraph example9 {
+ rankdir="LR";
+ node [texmode="math",shape="circle",style="state"];
+ q0 [style="state,initial",label="0"];
+ q1 [style="state",label="1"];
+ q2 [style="state",label="2"];
+ q3 [style="state",label="3"];
+ q4 [style="state",label="4"];
+ q5 [style="state",label="5"];
+ q6 [style="state",label="6"];
+ q7 [style="state",label="7"];
+ q8 [style="state",label="8"];
+ q9 [style="state,final",label="9"];
+ edge [texmode="math",lblstyle="auto"];
+ q0 -> q1 [label="e",texlbl="$\varepsilon$"];
+ q1 -> q2 [label="e",texlbl="$\varepsilon$"];
+ q2 -> q3 [label="a"];
+ q3 -> q6 [label="e",texlbl="$\varepsilon$"];
+ q1 -> q4 [label="e",texlbl="$\varepsilon$"];
+ q4 -> q5 [label="b"];
+ q5 -> q6 [label="e",texlbl="$\varepsilon$"];
+ q6 -> q1 [label="e",texlbl="$\varepsilon$"];
+ q6 -> q7 [label="e",texlbl="$\varepsilon$"];
+ q0 -> q7 [label="e",texlbl="$\varepsilon$"];
+ q7 -> q8 [label="e",texlbl="$\varepsilon$"];
+ q8 -> q9 [label="b"];
+}
diff --git a/figs/example9b.dot b/figs/example9b.dot
new file mode 100644
index 0000000..78137c9
--- /dev/null
+++ b/figs/example9b.dot
@@ -0,0 +1,19 @@
+digraph example9b {
+ rankdir="LR";
+ node [texmode="math",shape="circle",style="state"];
+ q0 [style="state,initial",label="0"];
+ q5 [style="state",label="5"];
+ q3 [style="state",label="3"];
+ q9 [style="state,final",label="9"];
+ edge [texmode="math",lblstyle="auto"];
+ q0 -> q3 [label="a"];
+ q0 -> q5 [label="b"];
+ { rank="same"; q3; q5; }
+ q3 -> q3 [label="a",topath="loop above"];
+ q5 -> q5 [label="b",topath="loop below"];
+ q3 -> q5 [label="b",lblstyle="auto,swap,near end"];
+ q5 -> q3 [label="a",lblstyle="auto,swap,pos=-0.2"];
+ q0 -> q9 [label="b"];
+ q3 -> q9 [label="b"];
+ q5 -> q9 [label="b"];
+}
diff --git a/notes-inf105.tex b/notes-inf105.tex
index 3806498..a946e4a 100644
--- a/notes-inf105.tex
+++ b/notes-inf105.tex
@@ -2289,10 +2289,11 @@ $q_0$ vers chacun des états initiaux de $A$, puis en éliminant les
résultat que ce qui vient d'être dit.)
\end{proof}
-\thingy On a vu en \ref{dfa-union-and-intersection} une preuve, à base
-de NFA, que $L_1 \cup L_2$ est reconnaissable lorsque $L_1$ et $L_2$
-le sont. Donnons maintenant une autre preuve de ce fait, à base de
-εNFA :
+\medbreak
+
+On a vu en \ref{dfa-union-and-intersection} une preuve, à base de DFA,
+que $L_1 \cup L_2$ est reconnaissable lorsque $L_1$ et $L_2$ le sont.
+Donnons maintenant une autre preuve de ce fait, à base de NFA :
\begin{prop}\label{nfa-union}
Si $L_1,L_2$ sont des langages reconnaissables (sur un même
@@ -2579,20 +2580,23 @@ triviaux $\varnothing$, $\{\varepsilon\}$ et $\{x\}$ (pour
chaque $x\in\Sigma$). On prendra les suivants :
\begin{center}
+\begin{tabular}{ll}
\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(q0.base)]
\node (q0) at (0bp,0bp) [draw,circle,state,initial] {$q_0$};
\end{tikzpicture}
-pour le langage $\varnothing$\\
+&pour le langage $\varnothing$ (i.e., pour l'expression rationnelle $\bot$),\\[1.75ex]
\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(q0.base)]
\node (q0) at (0bp,0bp) [draw,circle,state,initial,final] {$q_0$};
\end{tikzpicture}
-pour le langage $\{\varepsilon\}$\\
+&pour le langage $\{\varepsilon\}$ (i.e., pour l'expression
+rationnelle $\underline{\varepsilon}$), et\\[1.75ex]
\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(q0.base)]
\node (q0) at (0bp,0bp) [draw,circle,state,initial] {$q_0$};
\node (q1) at (60bp,0bp) [draw,circle,state,final] {$q_1$};
\draw [->] (q0) to node[auto,swap] {$x$} (q1);
\end{tikzpicture}
-pour le langage $\{x\}$.
+&pour le langage $\{x\}$ (i.e., pour l'expression rationnelle $x$).
+\end{tabular}
\end{center}
\begin{cor}\label{rational-languages-are-recognizable}
@@ -2618,7 +2622,7 @@ automate en DFA quitte déterminiser
si l'automate accepte le mot.
\end{proof}
-\thingy Les constructions que nous avons décrites dans cette section
+\thingy\label{glushkov-construction} Les constructions que nous avons décrites dans cette section
associent naturellement un NFA standard à chaque expression
rationnelle : il s'obtient en partant des automates de base décrits
en \ref{trivial-standard-automata} et en appliquant les constructions
@@ -2760,6 +2764,241 @@ toutes celles aboutissant à l'état $2$ sont étiquetées $b$, et toutes
celles aboutissant à $3$ sont étiquetées $c$.
+\subsection{L'automate de Thompson (alternative à l'automate de Glushkov)}
+
+\thingy La construction de Glushkov (exposée
+en \ref{glushkov-construction}) d'un automate reconnaissant le langage
+dénoté par expression rationnelle $r$ fabrique un NFA. Cette
+constrution produit un automate raisonnablement compact (en nombre
+d'états), mais il peut être intéressant de disposer d'une autre
+construction, plus transparente mais moins efficace : la
+\defin[Thompson (construction d'automate de)]{construction de
+ Thompson} fournit un autre moyen d'associer à une expression
+rationnelle $r$ un automate reconnaissant le langage qu'elle dénote.
+Elle possède pour sa part les propriétés suivantes :
+\begin{itemize}
+\item c'est un εNFA reconnaissant le langage $L_r$ dénoté par
+ l'expression rationnelle $r$ dont on est parti,
+\item il possède un unique état initial auquel n'aboutit aucune
+ transition, et un unique état final duquel ne part aucune
+ transition,
+\item son nombre d'états est égal au double du nombre de symboles
+ autres que les parenthèses constituant l'expression $r$ (en comptant
+ aussi bien les lettres de $\Sigma$ que les métacaractères $\bot$,
+ $\underline{\varepsilon}$, $|$ et $*$ ; mais sans compter la
+ concaténation implicite).
+\end{itemize}
+
+Dans les dessins qui suivent, on symbolisera de la manière suivante un
+automate de Thompson $A$ quelconque :
+\begin{center}
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (A) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+\end{center}
+
+\thingy\label{trivial-thompson-automata} Les automates de Thompson des
+langages de base triviaux $\varnothing$, $\{\varepsilon\}$ et $\{x\}$
+(pour chaque $x\in\Sigma$) seront les suivants :
+
+\begin{center}
+\begin{tabular}{ll}
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(qi.base)]
+\node (qi) at (0bp,0bp) [draw,circle,state,initial] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+&pour le langage $\varnothing$ (i.e., pour l'expression rationnelle $\bot$),\\
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(qi.base)]
+\node (qi) at (0bp,0bp) [draw,circle,state,initial] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\draw [->] (qi) to node[auto] {$\varepsilon$} (qf);
+\end{tikzpicture}
+&pour le langage $\{\varepsilon\}$ (i.e., pour l'expression
+rationnelle $\underline{\varepsilon}$), et\\
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(qi.base)]
+\node (qi) at (0bp,0bp) [draw,circle,state,initial] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\draw [->] (qi) to node[auto,swap] {$x$} (qf);
+\end{tikzpicture}
+&pour le langage $\{x\}$ (i.e., pour l'expression rationnelle $x$).
+\end{tabular}
+\end{center}
+
+\thingy\label{thompson-union} Si $A_1$ et $A_2$ sont les automates de
+Thompson pour les expressions rationnelles $r_1$ et $r_2$, celui de
+$r_1|r_2$ sera construit de la manière suivante :
+\begin{center}
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (A) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A_1$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+et
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (A) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A_2$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+\\deviennent\\
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(qi.base)]
+\node (qi) at (-35bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (95bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\node (A1) at (30bp,35bp) [draw,dotted,circle,minimum size=50bp] {$A_1$};
+\node (qi1) at (0bp,35bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\node (qf1) at (60bp,35bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\node (A2) at (30bp,-35bp) [draw,dotted,circle,minimum size=50bp] {$A_2$};
+\node (qi2) at (0bp,-35bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\node (qf2) at (60bp,-35bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\draw[->] (qi) to node[auto] {$\varepsilon$} (qi1); \draw[->] (qi) to node[auto] {$\varepsilon$} (qi2);
+\draw[->] (qf1) to node[auto] {$\varepsilon$} (qf); \draw[->] (qf2) to node[auto] {$\varepsilon$} (qf);
+\end{tikzpicture}
+\end{center}
+
+\thingy\label{thompson-concatenation} Si $A_1$ et $A_2$ sont les
+automates de Thompson pour les expressions rationnelles $r_1$ et
+$r_2$, celui de $r_1 r_2$ sera construit de la manière suivante :
+\begin{center}
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (A) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A_1$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+et
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (A) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A_2$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+\\deviennent\\
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(qi.base)]
+\node (A1) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A_1$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (ql) at (60bp,0bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\node (A2) at (150bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A_2$};
+\node (qr) at (120bp,0bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\node (qf) at (180bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\draw[->] (ql) to node[auto] {$\varepsilon$} (qr);
+\end{tikzpicture}
+\end{center}
+
+\thingy\label{thompson-star} Si $A$ est l'automate de Thompson pour
+l'expression rationnelle $r$, celui de $r{*}$ sera construit de la
+manière suivante :
+\begin{center}
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (A) at (30bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A$};
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (60bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\end{tikzpicture}
+devient
+\begin{tikzpicture}[>=latex,line join=bevel,automaton,baseline=(A.base)]
+\node (qi) at (0bp,0bp) [draw,circle,state,initial,fill=white] {$q_0$};
+\node (qf) at (180bp,0bp) [draw,circle,state,final,fill=white] {\vbox to0pt{\vss\hbox to0pt{$q_\infty$\hss}}\phantom{$q_0$}};
+\node (A) at (90bp,0bp) [draw,dotted,circle,minimum size=50bp] {$A$};
+\node (qai) at (60bp,0bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\node (qaf) at (120bp,0bp) [draw,circle,state,fill=white] {\phantom{$q_0$}};
+\draw[->] (qi) to node[auto] {$\varepsilon$} (qai);
+\draw[->] (qaf) to node[auto] {$\varepsilon$} (qf);
+\draw[->] (qi) ..controls (60bp,-60bp) and (120bp,-60bp) .. node[auto] {$\varepsilon$} (qf);
+\draw[->] (qaf) ..controls (120bp,60bp) and (60bp,60bp) .. node[auto,above] {$\varepsilon$} (qai);
+\end{tikzpicture}
+\end{center}
+
+\thingy Comme on le voit ci-dessus, la construction de Thompson est
+très simple à appliquer ; mais elle conduit à des automates rapidement
+énormes, comportant un nombre considérable d'états et de transitions
+spontanées « stupides ».
+
+À titre d'exemple, voici l'automate de Thompson, déjà gros, de
+l'expression rationnelle $(a|b){*}b$ :
+
+\begin{center}
+\scalebox{0.75}{%
+%%% begin example9 %%%
+
+\begin{tikzpicture}[>=latex,line join=bevel,automaton]
+%%
+\node (q1) at (97bp,61bp) [draw,circle,state] {$1$};
+ \node (q0) at (18bp,23bp) [draw,circle,state,initial] {$0$};
+ \node (q3) at (255bp,138bp) [draw,circle,state] {$3$};
+ \node (q2) at (176bp,138bp) [draw,circle,state] {$2$};
+ \node (q5) at (255bp,84bp) [draw,circle,state] {$5$};
+ \node (q4) at (176bp,84bp) [draw,circle,state] {$4$};
+ \node (q7) at (413bp,23bp) [draw,circle,state] {$7$};
+ \node (q6) at (334bp,61bp) [draw,circle,state] {$6$};
+ \node (q9) at (571bp,23bp) [draw,circle,state,final] {$9$};
+ \node (q8) at (492bp,23bp) [draw,circle,state] {$8$};
+ \draw [->] (q3) ..controls (280.5bp,113.5bp) and (299.16bp,94.836bp) .. node[auto] {$\varepsilon$} (q6);
+ \draw [->] (q2) ..controls (203.66bp,138bp) and (215.82bp,138bp) .. node[auto] {$a$} (q3);
+ \draw [->] (q6) ..controls (303.95bp,58.621bp) and (287.5bp,57.483bp) .. (273bp,57bp) .. controls (221.92bp,55.299bp) and (209.08bp,55.299bp) .. (158bp,57bp) .. controls (147.24bp,57.358bp) and (135.4bp,58.078bp) .. node[auto] {$\varepsilon$} (q1);
+ \draw [->] (q8) ..controls (519.66bp,23bp) and (531.82bp,23bp) .. node[auto] {$b$} (q9);
+ \draw [->] (q7) ..controls (440.66bp,23bp) and (452.82bp,23bp) .. node[auto] {$\varepsilon$} (q8);
+ \draw [->] (q5) ..controls (282.27bp,76.154bp) and (295.19bp,72.293bp) .. node[auto] {$\varepsilon$} (q6);
+ \draw [->] (q6) ..controls (361.12bp,48.108bp) and (375.27bp,41.127bp) .. node[auto] {$\varepsilon$} (q7);
+ \draw [->] (q4) ..controls (203.66bp,84bp) and (215.82bp,84bp) .. node[auto] {$b$} (q5);
+ \draw [->] (q1) ..controls (124.27bp,68.846bp) and (137.19bp,72.707bp) .. node[auto] {$\varepsilon$} (q4);
+ \draw [->] (q0) ..controls (49.792bp,8.7612bp) and (73.956bp,0bp) .. (96bp,0bp) .. controls (96bp,0bp) and (96bp,0bp) .. (335bp,0bp) .. controls (352.91bp,0bp) and (372.22bp,5.7837bp) .. node[auto] {$\varepsilon$} (q7);
+ \draw [->] (q0) ..controls (45.123bp,35.892bp) and (59.268bp,42.873bp) .. node[auto] {$\varepsilon$} (q1);
+ \draw [->] (q1) ..controls (122.5bp,85.495bp) and (141.16bp,104.16bp) .. node[auto] {$\varepsilon$} (q2);
+%
+\end{tikzpicture}
+
+%%% end example9 %%%
+}
+\end{center}
+
+(Il a $10$ états puisqu'il y a $5$ autres que les parenthèses
+dans $(a|b){*}b$.)
+
+Pour comparaison, voici son automate de Glushkov :
+
+\begin{center}
+%%% begin example9b %%%
+
+\begin{tikzpicture}[>=latex,line join=bevel,automaton]
+%%
+\begin{scope}
+ \pgfsetstrokecolor{black}
+ \definecolor{strokecol}{rgb}{1.0,1.0,1.0};
+ \pgfsetstrokecolor{strokecol}
+ \definecolor{fillcol}{rgb}{1.0,1.0,1.0};
+ \pgfsetfillcolor{fillcol}
+\end{scope}
+ \node (q9) at (176bp,45.608bp) [draw,circle,state,final] {$9$};
+ \node (q0) at (18bp,45.608bp) [draw,circle,state,initial] {$0$};
+ \node (q3) at (97bp,150.61bp) [draw,circle,state] {$3$};
+ \node (q5) at (97bp,45.608bp) [draw,circle,state] {$5$};
+ \draw [->] (q0) ..controls (42.244bp,77.303bp) and (64.303bp,107.38bp) .. node[auto] {$a$} (q3);
+ \draw [->] (q5) ..controls (124.66bp,45.608bp) and (136.82bp,45.608bp) .. node[auto] {$b$} (q9);
+ \draw [->] (q3) ..controls (121.24bp,118.91bp) and (143.3bp,88.83bp) .. node[auto] {$b$} (q9);
+ \draw [->] (q5) to[loop below] node[auto] {$b$} (q5);
+ \draw [->] (q0) ..controls (45.659bp,45.608bp) and (57.817bp,45.608bp) .. node[auto] {$b$} (q5);
+ \draw [->] (q0) ..controls (42.871bp,23.135bp) and (60.567bp,9.4181bp) .. (79bp,3.6077bp) .. controls (94.26bp,-1.2026bp) and (99.74bp,-1.2026bp) .. (115bp,3.6077bp) .. controls (129.69bp,8.2379bp) and (143.91bp,17.889bp) .. node[auto] {$b$} (q9);
+ \draw [->] (q3) to[loop above] node[auto] {$a$} (q3);
+ \draw [->] (q5) ..controls (112.04bp,72.544bp) and (117.47bp,87.733bp) .. (115bp,101.61bp) .. controls (113.63bp,109.34bp) and (111.12bp,117.45bp) .. node[auto,swap,pos=-0.2] {$a$} (q3);
+ \draw [->] (q3) ..controls (97bp,116.41bp) and (97bp,92.55bp) .. node[auto,swap,near end] {$b$} (q5);
+%
+\end{tikzpicture}
+
+%%% end example9b %%%
+\end{center}
+
+Il a $4$ états puisqu'il y a $3$ lettres dans $(a|b){*}b$. Ces états
+ont été étiquetés de manière à illustrer la proposition suivante, qui
+fait le lien entre les deux constructions :
+
+\begin{prop}
+L'élimination des transitions spontanées (au sens
+de \ref{removal-of-epsilon-transitions}, suivie de la suppression des
+états devenus inutiles) dans l'automate de Thompson d'une expression
+rationnelle conduit à l'automate de Glushkov de cette même expression.
+\end{prop}
+
+
+
+
\subsection{Automates à transitions étiquetées par des expressions rationnelles (=RNFA)}
\thingy\label{definition-rnfa} Un \defin[automate fini à transitions