1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
% \documentclass[10pt,mathserif,handout]{beamer}
\documentclass[10pt,mathserif,display]{beamer}
\usepackage{gastex}
\gasset{linewidth=0.21,AHdist=2.1,AHLength=2.25,AHlength=2.1}
\gasset{ATdist=2.1,ATLength=2.25,ATlength=2.1}
% \usepackage{beamerthemeEPIT}
\usepackage{beamerthemeplain}
\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}
%%%%%%%%%%%%%%%%%%%%%%
\frame{
\frametitle{Automaton $\Auto_\varphi$}
\vspace{-7mm}
\begin{center}\scalebox{0.9}{
\begin{picture}(130,71)(-12,0)\nullfont
% \put(-12,0){\framebox(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{picture}}
\end{center}
\vspace{-2mm}
\uncover<2->{{\only<2>{\color{red}}
Transition = check litterals and move forward.}}
\uncover<8->{{\only<8>{\color{red}}
Simplification}}
}
\end{document}
|
