1\documentclass{standalone} 2\usepackage{tikz} 3\usetikzlibrary{arrows} 4\usetikzlibrary{shadows} 5\usetikzlibrary{positioning} 6\usetikzlibrary{calc} 7\usetikzlibrary{shapes} 8\usetikzlibrary{backgrounds} 9\newcommand{\CF}{\ensuremath{\mathcal{F}}} 10 11\begin{document} 12\scalebox{1.2}{ 13\begin{tikzpicture}[shorten >=1pt,>=stealth',semithick,node distance=5.5mm] 14\tikzstyle{dstep}=[align=center,minimum height=3em] 15\tikzstyle{pstep}=[draw,dstep,drop shadow,fill=white] 16\tikzstyle{iostep}=[dstep,rounded corners=1mm] 17\tikzstyle{instep}=[iostep,fill=yellow!20] 18\tikzstyle{outstep}=[iostep,fill=green!20] 19\tikzstyle{errstep}=[iostep,fill=red!20] 20%\tikzset{callout/.style={ellipse callout, callout pointer arc=30, 21% callout absolute pointer={#1},fill=blue!30,draw}} 22%\tikzstyle{ 23 24\node[pstep] (trans) {translate\\to TGBA}; 25\node[pstep,right=of trans.0,xshift=-2mm] (wdba) {attempt\\WDBA\\minim.}; 26\draw[->] (trans) -- (wdba); 27\node[pstep,right=of wdba.0] (simp) {simplify\\TGBA}; 28\draw[->] (wdba) -- node[above]{fail} (simp); 29\node[instep,below=of trans,yshift=-4mm] (ltl1) {LTL\\formula}; 30\draw[->] (ltl1) -- (trans); 31 32\node[pstep,right=of simp,yshift=8mm,xshift=1mm] (degen) {degen\\to TBA}; 33\draw[->] (simp) -- ($(simp.east)+(2mm,0mm)$) |- node[above left,align=right,at end]{nondet. or\\$|\CF|>m=1$} (degen); 34\coordinate[pstep,right=of degen,yshift=-8mm,xshift=-1mm] (isdet); 35%\coordinate[pstep,right=of degen,yshift=-2em] (isdet2); 36\draw[->] (simp) -- ($(simp.east)+(2mm,0mm)$) -- node[below right,at start]{else} (isdet); 37\coordinate (degen2) at ($(degen.east)+(2mm,0mm)$); 38\draw[->] (degen) -- (degen2) -- ($(simp.east -| degen2)$); 39\node[pstep,right=of degen,xshift=2.5em] (tbadet) {attempt\\ powerset\\to DTBA}; 40\draw[->] (isdet) |- node[at end,above left]{nondet.} (tbadet); 41\coordinate (tbadet2) at ($(tbadet.east)+(2mm,0mm)$); 42\node[errstep,right=of tbadet.0,xshift=2mm,yshift=2mm] (nottcong) {not in\\$\mathsf{TCONG}$}; 43\draw[->] (tbadet) -- node[at end,above left,align=center]{fail} ($(nottcong.180 |- tbadet)$); 44\coordinate (turn) at ($(nottcong.-130 |- simp.0)$); 45\draw[->] (isdet) -- node[below right,at start]{det.} (turn); 46\draw[->] (tbadet2) -- node[right,pos=.6]{success} ($(tbadet2 |- turn)$); 47\node[pstep,below=of tbadet.-125,yshift=-5mm] (dtbasat) {DTBA SAT\\minimization}; 48\node[pstep,below=of dtbasat,yshift=5mm] (dtgbasat) {DTGBA SAT\\minimization}; 49\draw[->] (turn) |- node[above left]{$m=1$} (dtbasat); 50\draw[->] (turn) |- node[above left]{$m>1$} (dtgbasat); 51\node[outstep,left=of dtgbasat] (mindtgba) {minimal\\DTGBA}; 52\node[outstep] at ($(mindtgba |- dtbasat)$) (mindtba) {minimal\\DTBA}; 53\node[outstep,left=of mindtba,xshift=5mm] (wdbaok) {minimal\\WDBA}; 54\draw[->] (wdba) |- coordinate(c1) node[above right]{success} (wdbaok); 55 56\draw[->] (dtgbasat) -- (mindtgba); 57\draw[->] (dtbasat) -- (mindtba); 58\node[pstep,below=of ltl1,yshift=-3mm,xshift=1mm] (ltl2dstar) {\texttt{ltl2dstar}\\(DRA)}; 59\draw[->] (ltl1) -- ($(ltl1 |- ltl2dstar.90)$); 60\node[pstep,right=of ltl2dstar] (dra2dba) {attempt\\conversion\\to DBA}; 61\draw[->] (ltl2dstar) -- (dra2dba); 62\node[pstep,right=of dra2dba,xshift=3em] (wdba2) {attempt\\WDBA\\minim.}; 63\node[pstep,right=of wdba2,xshift=2em] (simp2) {simplify as\\DBA or DTBA}; 64\draw[->] (dra2dba) -- node[at start,below right]{success} (wdba2); 65\draw[->] (wdba2) -- node[at start,below right]{fail} (simp2); 66\coordinate (turn2) at ($(turn |- simp2)$); 67\draw[->] (simp2) -- (turn2); 68\draw[] (turn2) -- (turn); 69\node[errstep] (notrec) at ($(ltl1 -| dra2dba)$) {not a\\ recurrence}; 70\draw[->] (dra2dba) -- node[right]{fail} (notrec); 71\draw[->] (wdba2.160) -| node[below right,sloped]{success} (wdbaok); 72 73\begin{scope}[on background layer] 74\coordinate (pt1) at ($(tbadet.north east)+(3mm,3mm)$); 75\coordinate (pt2) at ($(mindtba.north east)+(3mm,1mm)$); 76\coordinate (pt3) at ($(mindtgba.south east)+(0mm,-2mm)$); 77\coordinate[xshift=1mm,yshift=1mm] (turn3) at (turn); 78\path[fill=blue!30,opacity=.3,rounded corners=1mm] ($(trans.west |- pt1)$) ++ (-1mm,0) |- (pt2) -- (pt3 -| pt2) -| (turn3) -| (pt1) -- cycle; 79\node[below right] at ($(trans.west |- pt1)$) {\texttt{ltl2tgba}}; 80 81 82\coordinate[yshift=1mm,xshift=1mm] (pt4) at ($(pt2 -| turn3)$); 83\coordinate[yshift=-4mm,xshift=-1mm] (pt5) at ($(dra2dba.south west)$); 84\coordinate[yshift=1mm,xshift=-1mm] (pt6) at ($(dra2dba.north west)$); 85\path[fill=blue!30!red!30,opacity=.3,rounded corners=1mm] (pt5) -| (pt4) -- ($(pt2) + (1mm,1mm)$) |- (pt6) -- cycle; 86\node[above left,yshift=-1mm] at ($(pt5 -| pt4)$) {\texttt{dstar2tgba}/\texttt{autfilt}}; 87\end{scope} 88%\draw[red] (current bounding box.north west) rectangle (current bounding box.south east); 89\end{tikzpicture}} 90\end{document} 91%%% Local Variables: 92%%% mode: latex 93%%% TeX-master: t 94%%% End: 95