\usepackage{amssymb,amsmath}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{semantic}
\usepackage{graphicx}
\usepackage{eurosym}
\usepackage{hyperref}
\usepackage{array}
\usepackage{multirow}
\usepackage{tikz}
\usepackage{pgfplots}

\usepackage{listings}
\usepackage{enumerate}

\newcommand\putAt[3]{\vbox to 0pt{\kern #2\hbox{\kern #1{#3}\hss}\vss}}

\lstdefinelanguage{multicubes}{
  keywords={rollup,rollup*,recrollup,drilldown,drilldown*,recdrilldown,privot,sort,
  ASC,DESC,BASC,BDESC,dice,rename,drillacross,addmeasure,dropmeasure,max,min,sum,avg,
  toppercent,order,by,over,cells,preceding,union},
  alsoletter={*},
  sensitive={false},
  comment=[l]//,
  morecomment=[s]{/*}{*/}
}
\lstdefinelanguage{MDX}[]{SQL}{
  escapechar=@,
  morekeywords={columns,PAGES, CHAPTER, SECTIONS,
               SELF,AFTER,BEFORE,BEFORE_AND_AFTER,SELF_AND_AFTER,SELF_AND_BEFORE,
               SELF_BEFORE_AFTER,LEAVES,
               descendants, ascendants,
               CURRENTMEMBER, PREVMEMBER, NEXTMEMBER,
               PARENT, FIRSTCHILD, LASTCHILD,
               generate,  PARALLELPERIOD,  OPENINGPERIOD,
               CLOSINGPERIOD,
               periodstodate, ytd, qtd, mtd, wtd,
               lag,filter, with, member,order,
               ASC,DESC,BASC, BDESC, name,
               head,tail,topcount,
               toppercent, topsum,
               bottom, bottomsum,
               SUM, AVG, MEDIAN, MAX, MIN, VAR, STDDEV,
               count, excludeempty
  },
  string=[bd]",
  deletekeywords={year},
}

\lstdefinelanguage{JavaScript}{
  keywords={typeof, new, true, false, catch, function, return, null, catch, switch, var, if, in, while, do, else, case, break},
  keywordstyle=\color{blue}\bfseries,
  ndkeywords={class, export, boolean, throw, implements, import, this},
  ndkeywordstyle=\color{darkgray}\bfseries,
  identifierstyle=\color{black},
  sensitive=false,
  comment=[l]{//},
  morecomment=[s]{/*}{*/},
  commentstyle=\color{purple}\ttfamily,
  stringstyle=\color{red}\ttfamily,
  morestring=[b]',
  morestring=[b]"
}


\newenvironment{nohandout}[1]{
  \begin{list}{}{}
  \item<#1|handount:0>
}{\end{list}}
\newenvironment{handout}[1]{
  \begin{list}{}{}
  \item<#1|handount:1>
}{\end{list}}

\lstset{language=Python,
  basicstyle=\fontsize{8}{9}\selectfont\ttfamily,
  keywordstyle=\color{brown},
  emphstyle=\color{blue}
}


\let\oldlstinline\lstinline
\def\lstinline{\oldlstinline[basicstyle=\normalsize\ttfamily]}

\newcommand{\tolevel}{->}

\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\makeatletter
\def\qed{%
     \ifhmode%
        \unskip\nobreak\hfil%
        \penalty50\hskip1em\null\nobreak\hfil\squareforqed%
        \parfillskip=0pt\finalhyphendemerits=0\endgraf%
     \else%
       % \nopagebreak[4]%
       % \leavevmode\nobreak\hfill\squareforqed%
       \kern-1em\samepage\leavevmode\hfill\squareforqed%
   \fi}
\makeatother

% \newtheorem{mytheorem}{Theorem}
% \newtheorem{mydefinition}{Definition}
% \newtheorem{myexample}{Example}
% \newtheorem{mylemma}{Lemma}
% \newtheorem{myproposition}{Proposition}
% \newtheorem{mycorollary}{Corollary}
%\newenvironment{proof}{\par\textit{Proof.}\ }{}

%\newenvironment{theorem}{\begin{mytheorem}\upshape}{\qed\end{mytheorem}}
%\newenvironment{definition}{\begin{mydefinition}\upshape}{\qed\end{mydefinition}}
%\newenvironment{lemma}{\begin{mylemma}\upshape}{\qed\end{mylemma}}
%\newenvironment{proposition}{\begin{myproposition}\upshape}{\qed\end{myproposition}}
%\newenvironment{corollary}{\begin{mycorollary}\upshape}{\qed\end{mycorollary}}
%\newenvironment{example}{\begin{myexample}\upshape}{\qed\end{myexample}}
\makeatother


\DeclareMathSymbol\gusano{\mathrel}{lasy}{"3A}

\newbox\arriba
\newbox\abajo
\newbox\CaracterInterno
\newbox\CaracterDerecha
\newdimen\anchura
\def\MacrosTranGeneral#1#2#3#4#5#6{%
  \setbox\CaracterInterno=\hbox{\mathsurround=0pt$\mathord#4$}
  \setbox\CaracterDerecha=\hbox{\mathsurround=0pt$\mathord#3$}
  \setbox\arriba=\hbox{$#1#2$}
  \setbox\abajo=\hbox{\mathsurround=0pt%
                      \anchura=\wd\arriba%
                      \advance \anchura by 0.5em%
                      \divide \anchura by \wd\CaracterInterno%
                      \multiply \anchura by \wd\CaracterInterno%
                      \copy\CaracterInterno\kern\SeparacionInternaFlecha
                      \hbox to \anchura{%
                          $\cleaders%
                            \hbox{\kern\SeparacionInternaFlecha\copy\CaracterInterno}
                            \hfill$}%
                      \kern\SeparacionExternaFlecha\copy\CaracterDerecha}
  \mathrel{{\buildrel\vbox{\copy\arriba \kern\SeparacionFlechaArriba} %
    \over{\copy\abajo^{#6}}}_{#5}}
  }
\def\MacrosTranGeneralProp#1#2#3#4#5{\mathchoice%
  {\MacrosTranGeneral{\scriptstyle}{#1}{#2}{#3}{#4}{#5}}
  {\MacrosTranGeneral{\scriptstyle}{#1}{#2}{#3}{#4}{#5}}
  {\MacrosTranGeneral{\scriptscriptstyle}{#1}{#2}{#3}{#4}{#5}}
  {\MacrosTranGeneral{\scriptscriptstyle}{#1}{#2}{#3}{#4}{#5}}}

\def\MacrosTran#1{%
  \def\SeparacionInternaFlecha{-0.3em}%
  \def\SeparacionExternaFlecha{-0.5em}%
  \def\SeparacionFlechaArriba{-3pt}%
  \MacrosTranGeneralProp{#1}{{\rightarrow}}{{-}}{}{}}
\def\MacrosNoTran#1{%
  \def\SeparacionInternaFlecha{-0.3em}
  \def\SeparacionExternaFlecha{-0.5em}
  \def\SeparacionFlechaArriba{-3pt}
  \MacrosTranGeneralProp{#1\kern 0.5em}{{\not\rightarrow}}{{-}}{}{}}
\def\MacrosVTran#1{%
  \def\SeparacionInternaFlecha{-0.2em}
  \def\SeparacionExternaFlecha{-0.5em}
  \def\SeparacionFlechaArriba{0pt}
  \MacrosTranGeneralProp{#1}{{\Rightarrow}}{{=}}{}{}}
\def\MacrosNoVTran#1{%
  \def\SeparacionInternaFlecha{-0.2em}
  \def\SeparacionExternaFlecha{-0.5em}
  \def\SeparacionFlechaArriba{-3pt}
  \MacrosNoTranGeneralProp{#1}{{\not\Rightarrow}}{{=}}{}{}}
\def\MacrosTiTran#1{%
  \def\SeparacionInternaFlecha{-0.0pt}
        \def\SeparacionExternaFlecha{-0.0pt}
        \def\SeparacionFlechaArriba{0pt}
  \kern 1pt\MacrosTranGeneralProp{#1}{{\leadsto}}{{\gusano}}{}{}}
\def\MacrosTiTranRe#1{%
  \def\SeparacionInternaFlecha{-0pt}
        \def\SeparacionExternaFlecha{-0.0pt}
        \def\SeparacionFlechaArriba{-3pt}
  \kern 1pt \MacrosTranGeneralProp{#1}{{\leadsto}}{{\gusano}}{}{*}}
\def\MacrosNoTiTranRe#1{%
  \def\SeparacionInternaFlecha{-0pt}
        \def\SeparacionExternaFlecha{-0.0pt}
        \def\SeparacionFlechaArriba{-3pt}
  \kern 1pt \MacrosTranGeneralProp{#1}{{\not\leadsto}}{{\gusano}}{}{*}}
\def\MacrosNoTiTran#1{%
  \def\SeparacionInternaFlecha{-0pt}
        \def\SeparacionExternaFlecha{-0.0pt}
        \def\SeparacionFlechaArriba{-3pt}
  \kern 1pt \MacrosTranGeneralProp{#1}{{\not\leadsto}}{{\gusano}}{}{}}



%\def\tran#1{\ensuremath\mathbin{\MacrosTran{#1}}}
\def\vtran#1{\ensuremath\mathbin{\MacrosVTran{#1}}}
\def\notran#1{\ensuremath\mathbin{\MacrosNoTran{#1}}}
\def\novtran#1{\ensuremath\mathbin{\MacrosNoVTran{#1}}}
\newcommand{\tran}[1]{\MacrosTran{#1}}
\newcommand{\tranti}[1]{\ensuremath\mathbin{\MacrosTiTran{#1}}}
\newcommand{\trantire}[1]{\MacrosTiTranRe{#1}}
\newcommand{\notranti}[1]{\MacrosNoTiTran{#1}}
\newcommand{\notrantire}[1]{\MacrosNoTiTranRe{#1}}


%% For iocos stuff.
\newcommand{\mIUT}{\ensuremath{\mathrm{IUT}_m}}
\newcommand{\Onodelta}{\ensuremath{O_{\not\delta}}}

\newcommand{\tranp}[2]{\MacrosTran{#1}_{\!\!#2}\;}
\newcommand{\tranap}[2]{\MacrosVTran{#1}_{\!\!#2}\;}
\newcommand{\tranb}[2]{\stackrel{#1}{\Longrightarrow}_{#2}}
\newcommand{\transi}[2]{\MacrosTran{#1}_{\!\!#2}\;}
\newcommand{\iocos}{\ensuremath{\mathbin{\mathsf{ioco\underline{s} }}}}
\newcommand{\giocos}{\ensuremath{\mathbin{\mathsf{g\mbox{-}ioco\underline{s} }}}}
\newcommand{\niocos}{\ensuremath{\mathbin{\kern 1em\hbox to 0pt{/\hss}\kern-1em \mathsf{ioco\underline{s}}}}}
%\newcommand{\iocoqs}{\mathbin{\mathbf{iocoqs}}}
\newcommand{\ioco}{\ensuremath{\mathbin{\mathsf{ioco}}}}
\newcommand{\nioco}{\ensuremath{\mathbin{\kern 1em\hbox to 0pt{/\hss}\kern-1em \mathsf{ioco}}}}
\newcommand{\IOTS}{\ensuremath{\mathit{IOTS}}}
\newcommand{\LTS}{\ensuremath{\mathit{LTS}}}
\newcommand{\LTSs}{\ensuremath{\mathit{LTSs}}}
\newcommand{\Lts}{\ensuremath{{\cal L}}}
\newcommand{\after}{\mathbin{\mathsf{after}}}
\newcommand{\partes}{\ensuremath{{\cal P}}}
% \newcommand{\success}{\hbox{\blacksmiley}}
% \newcommand{\fail}{\hbox{\frownie}}
% \newcommand{\success}{\hbox{\Checkmark}}
% \newcommand{\fail}{\hbox{\XSolidBrush}}
% \newcommand{\success}{\checkmark}
% \newcommand{\fail}{\hbox{X}}
\newcommand{\success}{\hbox{\fontsize{8}{10}\selectfont\Checkmark}}
\newcommand{\fail}{\lower2pt\hbox{\fontsize{8}{10}\selectfont\XSolidBrush}}

\newcommand{\pass}{\mathbin{\mathsf{pass}}}
\newcommand{\nopass}{\mathbin{\kern1em\hbox to 0pt{/\hss}\kern-1em \mathsf{pass}}}
\newcommand{\vacio}{\varnothing}

%\renewcommand{\after}{\mathbin{~\mathsf{after}~}}
\newcommand{\traces}{\mathsf{traces}}
\newcommand{\Straces}{\mathit{Straces}}
\newcommand{\outs}{\mathsf{outs}}
\newcommand{\ins}{\mathsf{ins}}
\newcommand{\init}{\mathsf{init}}

%% General commands

\newcommand{\comen}[1]{}
%\newcommand{\nota}[1]{\textbf{#1}}


\newcommand{\tests}{\ensuremath{\mathit{{\cal T}}}}
\newcommand{\vtests}{\ensuremath{\mathit{{\cal T}}_v}}
\newcommand{\ltest}{\ensuremath{\mathbin{\sqsubseteq_T}}}
\newcommand{\noltest}{\ensuremath{\mathbin{\kern0.5em/\kern-1em \sqsubseteq_T}}}
\newcommand{\testfrom}[1]{{\cal T}(#1)}
\newcommand{\partini}{\Omega}
\newcommand{\relini}{\preccurlyeq}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\calS}{\cal S}
\newcommand{\recup}{\vartriangleright}
\newcommand{\fin}{\;\mathsf{in}\;}
\newcommand{\nil}{\mathsf{nil}}
\newcommand{\pdiv}{\mathsf{div}}
\newcommand{\ok}{\mathsf{ok}}
\newcommand{\ic}{\mathsf{ic}}
\newcommand{\paral}{\mathbin{\|}}
\newcommand{\partest}{\mathbin{|}}
%\newcommand{\choice}{\mathbin{\square}}
\newcommand{\choice}{\mathbin{+}}
%\newcommand{\ichoice}{\mathbin{\sqcap}}
\newcommand{\ichoice}{\mathbin{\oplus}}
\newcommand{\rec}{\mathsf{rec\;}}
\newcommand{\ocul}{\mathbin{\backslash}}
\newcommand{\may}{\mathbin{\mathsf{may}}}
\newcommand{\must}{\mathbin{\mathsf{must}}}
\newcommand{\nomust}{\hbox to 0em{\null\hskip 1em /\hss}\mathbin{\mathsf{must}}}
\newcommand{\nomay}{\hbox to 0em{\null\hskip 1em /\hss}\mathbin{\mathsf{may}}}
\newcommand{\ltmust}{\mathbin{\sqsubseteq_{\mathsf{must}}}}
\newcommand{\llmust}{\mathbin{\ll_{\mathsf{must}}}}
\newcommand{\noltmust}{\hbox to 0em{\null\hskip 0.5em /\hss}\mathbin{\sqsubseteq_{\mathsf{must}}}}
\newcommand{\nollmust}{\hbox to 0em{\null\hskip 0.5em /\hss}\mathbin{\ll_{\mathsf{must}}}}
\newcommand{\eqmust}{\mathbin{\equiv_{\mathsf{must}}}}
\newcommand{\ltmay}{\mathbin{\sqsubseteq_{\mathsf{may}}}}
\newcommand{\llmay}{\mathbin{\ll_{\mathsf{may}}}}
\newcommand{\noltmay}{\hbox to 0em{\null\hskip 0.5em /\hss}\mathbin{\sqsubseteq_{\mathsf{may}}}}
\newcommand{\nollmay}{\hbox to 0em{\null\hskip 0.5em /\hss}\mathbin{\ll_{\mathsf{may}}}}
\newcommand{\eqmay}{\mathbin{\equiv_{\mathsf{may}}}}
\newcommand{\llset}{\mathbin{\subset\subset}}
\newcommand{\appr}{\mathsf{appr}}
\newcommand{\trdiv}[1]{\nearrow_{#1}}
\newcommand{\trconv}[1]{\searrow_{#1}}
%\newcommand{\dotminus}{\mathbin{\vbox{\hbox{.}\kern-0.8em\hbox{-}}}}
\newcommand{\dotminus}{\mathbin{\vbox{\hbox to 1em{\hfill$.$\hfill}\kern-0.8em\hbox to 1em{\hfill$-$\hfill}}}}
\newcommand{\act}{\mathsf{Act}}
\newcommand{\acttau}{\act_\tau}
\newcommand{\timedomain}{{\cal T}}
\newcommand{\agentset}{\ensuremath{{\cal AG}}}
\newcommand{\lsim}{\lesssim}
\newcommand{\cent}{c}
\newcommand{\pr}{\mathsf{P_r}}
\newcommand{\ob}{\mathsf{O_b}}
\newcommand{\fb}{\mathsf{F_b}}
\newcommand{\regla}[1]{\ensuremath{\textsf{#1}}}
\newcommand{\var}{\mathsf{Var}}
\newcommand{\wait}{\mathsf{Wait}}
\newcommand{\sync}[1]{\overline{#1}}
\makeatletter
\def\@inferenceFrontName[#1]{%
  \setbox3=\hbox{\textsf{\footnotesize #1}}%
  \ifdim \wd3 > \z@
    \unhbox3%
    \hskip\@@nSpace
  \fi
  \@inferenceMiddle
}
\def\calR{{\cal R}}
\def\calA{{\cal A}}
\def\calB{{\cal B}}
\def\calP{{\cal P}}
\def\calO{{\cal O}}

\usetikzlibrary{shapes,arrows,automata,trees,positioning,decorations.pathmorphing,backgrounds,fit,petri}
\tikzset{%
  div/.style={circle,draw=black,fill=white},
  %every node/.style={fill,circle,minimum size=5pt, inner sep=0pt},
  edge from parent/.style={->,>=stealth', shorten >=1pt,semithick,draw},
  every loop/.style={right, out=30, in=-15,->,>=stealth'},
  level distance=3.5em, level/.style={sibling distance=5em},
  nosyntax/.style={fill,circle,minimum size=5pt, inner sep=0pt,color=black},
  normal/.style={color=black},
  emph/.style={color=red},
  arbol/.style={shape=isosceles triangle,draw=black, fill=none, inner sep=0.5em, shape border rotate=90},
  place/.style={circle,draw=blue!50,fill=blue!20, thick, inner sep=0pt,minimum size=4mm},
  transition/.style={rectangle,draw=black!50,fill=black!20,thick, inner sep=0pt,minimum height=2mm, minimum width=6mm}
}
\pgfplotsset{compat=1.17}



\def\gtree#1{\lower2.5ex\hbox{\begin{tikzpicture}
    %\node[shape=isosceles triangle,draw=black, fill=none, inner sep=0.5em, shape border rotate=90] {#1};
    \node[arbol] {#1};
  \end{tikzpicture}}
}

\tikzset{onslide/.code args={<#1>#2}{%
  \only<#1>{\pgfkeysalso{#2}} % \pgfkeysalso doesn't change the path
}}
\tikzset{temporal/.code args={<#1>#2#3#4}{%
  \temporal<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}{\pgfkeysalso{#4}} % \pgfkeysalso doesn't change the path
}}

\let\oldemph\emph
\renewcommand{\emph}[1]{\oldemph{\color{red}#1}}
\def\transf#1{\hspace{0.5cm}$\tranti{\hspace{#1}}$\hspace{0.5cm}}
\newcounter{query}
\newcounter{queryant}
\setcounter{query}{0}
\def\query#1{\stepcounter{query} \textbf{Query \arabic{query}. #1}}
\newenvironment{itquery}{
  \begin{list}{\textbf{Query \arabic{query}.}}{%
      \usecounter{query}\setcounter{query}{\arabic{queryant}}
      \setlength{\leftmargin}{0pt}
    }
}{\setcounter{queryant}{\arabic{query}}\end{list}}
\def\acr#1{{\color{red}#1}}

\makeatother
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main.tex"
%%% End: