% \documentclass[10pt,mathserif,dvipsnames,handout]{beamer}
\documentclass[10pt,mathserif,dvipsnames,display]{beamer}
% Compile with pdflatex or with latex+dvips+ps2pdf
\usepackage[pdflatex,recompilepics=true]{gastex}
\gasset{linewidth=0.21,AHdist=2.1,AHLength=2.25,AHlength=2.1} 
\gasset{ATdist=2.1,ATLength=2.25,ATlength=2.1} 
 
\beamersetleftmargin{3mm}
\beamersetrightmargin{3mm}
\abovedisplayskip=1ex
\belowdisplayskip=1ex
\parskip=.5ex
\parindent=0pt

\newcommand{\Auto}{\mathcal{A}}
\newcommand{\F}{\mathop{\mathsf{F}\vphantom{a}}\nolimits}
\newcommand{\G}{\mathop{\mathsf{G}\vphantom{a}}\nolimits}
\newcommand{\X}{\mathop{\mathsf{X}\vphantom{a}}\nolimits}
\newcommand{\True}{\top}
\newcommand{\False}{\bot}

\newcommand{\Blue}[1]{\textcolor{blue}{#1}}
\newcommand{\Red}[1]{\textcolor{red}{#1}}
\newcommand{\Green}[1]{\textcolor{PineGreen}{#1}}

\begin{document}

% WARNING: If a frame consists only of a gpicture with overlays, when compiling 
% with pdflatex you may get the first overlay only. I don't know why and guess 
% it is a problem either with auto-pst-pdf or with beamer.
% SOLUTION: add a command outside the gpicture which forces the generation of 
% all overlays, e.g., \pause[6]

%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
  \frametitle{Automaton $\Auto_\varphi$}
  \vspace{-7mm}
  \begin{center}\scalebox{0.9}{
  \begin{gpicture}(130,71)(-12,0)
%   The following (almost) invisible rectangle is necessary when compiling with 
%   pdflatex so that in each overlay the picture is always of the same size.
%   Otherwise, the picture of each overlay is cropped to its visible part.
    \put(-12,0){\drawrect[linegray=.99](0,0,130,71)}
    \gasset{Nadjust=w,Nadjustdist=2,Nh=8,fillcolor=White,Nfill=y,ilength=7}
    {\only<7-| handout:0>{\gasset{fillcolor=yellow}}
    \node[Nmarks=i](1)(10,45){$\varphi=\G(\neg p\vee\F q)$}}
    \node(2)(10,25){$\neg p\vee\F q, \X\varphi$}\drawedge(1,2){}
    \node(3)(10,05){$\neg p, \X\varphi$}\drawedge(2,3){}
    \node(4)(40,25){$\F q, \X\varphi$}\drawedge(2,4){}
    \node(5)(40,45){$q, \X\varphi$}\drawedge(4,5){}
    \node(6)(40,05){$\X\F q, \X\varphi$}\drawedge(4,6){\Blue{$\F q$}}

    \only<2->{
    \only<2| handout:0>{\gasset{linecolor=Red}}
    \drawedge[curvedepth=15](3,1){$\neg p$}
    \drawedge[ELside=r,ELpos=35](5,1){$q$}
    {\only<7-| handout:0>{\gasset{fillcolor=yellow}}
    \node(7)(70,05){$\F q, {\only<3| handout:0>{\color{red}}\varphi}$}}
    \drawedge(6,7){$\True$}
    }
    \only<3->{
    \only<3| handout:0>{\gasset{linecolor=Red}}
    \node(8)(70,25){$\F q, 
      {\only<3-4| handout:0>{\color{red}}\neg p\vee\F q},
      {\only<3| handout:0>{\color{red}}\X\varphi}$}
    \drawedge(7,8){}
    }
    \only<4->{
    \only<4| handout:0>{\gasset{linecolor=Red}}
    \node(9)(70,45){${\only<5| handout:0>{\color{red}}\F q}, 
      {\only<4| handout:0>{\color{red}}\neg p}, 
      \X\varphi$}
    \drawedge[ELpos=55](8,4){}
    \drawedge(8,9){}
    }
    \only<5->{
    \node(10)(105,25){${\only<5| handout:0>{\color{red}}\X\F q}, 
      \neg p, \X\varphi$}
    \node(11)(40,65){${\only<5| handout:0>{\color{red}}q}, 
      \neg p, \X\varphi$}
    \only<5| handout:0>{\gasset{linecolor=Red}}
    \drawedge(9,10){\Blue{$\F q$}}
    \drawedge(9,11){}
    }
    \only<6->{
    \only<6| handout:0>{\gasset{linecolor=Red}}
    \drawedge(10,7){$\neg p$}
    \drawedge[ELside=r](11,1){$\neg p\wedge q$}
    }
    \only<7->{\put(18,18){
%     \drawrect(58,33,100,53)
    \gasset{loopdiam=5,Nw=7,Nh=7}
    \gasset{fillcolor=yellow}
    \node[Nmarks=i,ilength=5](A)(72,40){1}
    \node(B)(92,40){2}
    \drawedge[curvedepth=2,linecolor=blue](A,B){$\True$}
    \drawedge[curvedepth=2](B,A){$q$}
    \only<7>{\drawedge[curvedepth=8](B,A){$\neg p\wedge q$}}
    \drawloop(A){$\neg p\vee q$}
    \drawloop[linecolor=blue](B){$\True$}
    \only<7>{\drawloop[ELpos=75,linecolor=blue,loopangle=0](B){$\neg p$}}
    }}
  \end{gpicture}}
  \end{center}

  \vspace{-2mm}
  \uncover<2->{{\only<2>{\color{red}}
  Transition = check litterals and move forward.}}

  \uncover<8->{{\only<8>{\color{red}}
  Simplification}}
\end{frame}

\end{document}
