Mercurial Mercurial > hg > regexp / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tphols-2011/document/fig_star.tex
author zhang
Mon, 31 Jan 2011 14:51:47 +0000
changeset 55 d71424eb5d0c
permissions -rw-r--r--
Myhill.thy IsabelleMakefile modified

\begin{figure}[h!]
\centering
\subfigure[First split]{\label{first_split}
\scalebox{0.7}{
\begin{tikzpicture}
    \node[draw,minimum height=3.8ex] (xa) {$\hspace{2em}xa\hspace{2em}$};
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{5em}x - xa\hspace{5em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$x$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (z.north west) -- ($(z.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$z$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
               node[midway, above=0.6em]{$x @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$(x - xa) @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$xa \in L_1*$};
\end{tikzpicture}}}

\subfigure[Max split]{\label{max_split}
\scalebox{0.7}{
\begin{tikzpicture}
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$x$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (z.north west) -- ($(z.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$z$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
               node[midway, above=0.8em]{$x @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$xa \in L_1*$};
\end{tikzpicture}}}

\subfigure[Max split with $a$ and $b$ (the right situation)]{\label{ab_split}
\scalebox{0.7}{
\begin{tikzpicture}
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$x$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (z.north west) -- ($(z.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$z$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
               node[midway, above=0.8em]{$x @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$xa \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xxa.south east)+(6em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
               node[midway, below=0.5em]{$a \in L_1$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(6em,-5ex)$)
               node[midway, below=0.5em]{$b \in L_1*$};
\end{tikzpicture}}}


\subfigure[Max split with $a$ and $b$ (the wrong situation)]{\label{ab_split_wrong}
\scalebox{0.7}{
\begin{tikzpicture}
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{21em}$ };

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$x$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (z.north west) -- ($(z.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$z$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
               node[midway, above=0.8em]{$x @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$(x - xa\_max) @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$xa \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xxa.south east)+(-3em,-5ex)$) -- ($(xxa.south west)+(0em,-5ex)$)
               node[midway, below=0.5em]{$a \in L_1$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(z.south east)+(0em,-5ex)$) -- ($(xxa.south east)+(-3em,-5ex)$)
               node[midway, below=0.5em]{$b \in L_1*$};
\end{tikzpicture}}}


\subfigure[Last split]{\label{last_split}
\scalebox{0.7}{
\begin{tikzpicture}
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}xa\_max\hspace{4em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - xa\_max\hspace{0.5em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$x$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (za.north west) -- ($(zb.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$z$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
               node[midway, above=0.8em]{$x @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$(x - xa\_max) @ za \in L_1$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$xa\_max \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$zb \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
               node[midway, below=0.5em]{$(x - xa\_max)@z \in L_1*$};
\end{tikzpicture}}}


\subfigure[Structure transferred to $y$]{\label{trans_split}
\scalebox{0.7}{
\begin{tikzpicture}
    \node[draw,minimum height=3.8ex] (xa) { $\hspace{5em}ya\hspace{5em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{2em}y - ya\hspace{2em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}za\hspace{2em}$ };
    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}zb\hspace{7em}$ };

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$y$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           (za.north west) -- ($(zb.north east)+(0em,0em)$)
               node[midway, above=0.5em]{$z$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
               node[midway, above=0.8em]{$y @ z \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$(y - ya) @ za \in L_1$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$ya \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
               node[midway, below=0.5em]{$zb \in L_1*$};

    \draw[decoration={brace,transform={yscale=3}},decorate]
           ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
               node[midway, below=0.5em]{$(y - ya)@z \in L_1*$};
\end{tikzpicture}}}

\caption{The case for $STAR$}
\end{figure}
regexp