\batchmode
\documentclass[twoside,fleqn]{article}
\RequirePackage{ifthen}



\usepackage[spanish]{babel}
\usepackage{isolatin1}
\usepackage{latexsym}
\usepackage{html}
\usepackage{graphicx}
\usepackage{a4wide}
\usepackage{listings}
\usepackage{floatflt}

\lstset{mathescape=true,extendedchars=true,language=Modula-2,basicstyle=\sffamily ,keywordstyle=\rmfamily\bfseries ,morekeywords={TASK,BSEMAPHORE,SEMAPHORE,INIT,Wait,Signal,Continue,Delay,COBEGIN,COEND,MONITOR,CONDITION,PUBLIC,STATE,LOOP,CHANNEL,MODEL,Send,Receive,GetChannel,WHEN,SELECT,FORALL}}

%
\renewcommand{\floatpagefraction}{0.9}%
\renewcommand{\floatsep}{0.5cm}%
%
\renewcommand{\textfloatsep}{0.5cm}%

%
\providecommand{\en}{\ensuremath{\rightarrow}}%
\providecommand{\por}{\ensuremath{\times}}%
\providecommand{\nat}{\ensuremath{\mathcal{N}}}%
\providecommand{\bool}{\ensuremath{\mathcal{B}}}%
\providecommand{\real}{\ensuremath{\mathcal{R}}}%
\providecommand{\complex}{\ensuremath{\mathcal{C}}}%
\providecommand{\sal}{\ensuremath{^{sal}}}%
\providecommand{\ent}{\ensuremath{^{ent}}}%
\providecommand{\sep}{\ensuremath{\bullet}}
\topmargin -1cm
\evensidemargin -1cm
\oddsidemargin -1cm
\textwidth 17.5cm
\textheight 25cm

\itemsep -1em
\parsep -2em
\topsep 0pt
\partopsep 0pt
\baselineskip 0pt


\usepackage[dvips]{color}


\pagecolor[gray]{.7}

\usepackage[latin1]{inputenc}



\makeatletter

\makeatletter
\count@=\the\catcode`\_ \catcode`\_=8 
\newenvironment{tex2html_wrap}{}{}%
\catcode`\<=12\catcode`\_=\count@
\newcommand{\providedcommand}[1]{\expandafter\providecommand\csname #1\endcsname}%
\newcommand{\renewedcommand}[1]{\expandafter\providecommand\csname #1\endcsname{}%
  \expandafter\renewcommand\csname #1\endcsname}%
\newcommand{\newedenvironment}[1]{\newenvironment{#1}{}{}\renewenvironment{#1}}%
\let\newedcommand\renewedcommand
\let\renewedenvironment\newedenvironment
\makeatother
\let\mathon=$
\let\mathoff=$
\ifx\AtBeginDocument\undefined \newcommand{\AtBeginDocument}[1]{}\fi
\newbox\sizebox
\setlength{\hoffset}{0pt}\setlength{\voffset}{0pt}
\addtolength{\textheight}{\footskip}\setlength{\footskip}{0pt}
\addtolength{\textheight}{\topmargin}\setlength{\topmargin}{0pt}
\addtolength{\textheight}{\headheight}\setlength{\headheight}{0pt}
\addtolength{\textheight}{\headsep}\setlength{\headsep}{0pt}
\setlength{\textwidth}{451pt}
\setlength{\textheight}{554pt}
\newwrite\lthtmlwrite
\makeatletter
\let\realnormalsize=\normalsize
\global\topskip=2sp
\def\preveqno{}\let\real@float=\@float \let\realend@float=\end@float
\def\@float{\let\@savefreelist\@freelist\real@float}
\def\liih@math{\ifmmode$\else\bad@math\fi}
\def\end@float{\realend@float\global\let\@freelist\@savefreelist}
\let\real@dbflt=\@dbflt \let\end@dblfloat=\end@float
\let\@largefloatcheck=\relax
\let\if@boxedmulticols=\iftrue
\def\@dbflt{\let\@savefreelist\@freelist\real@dbflt}
\def\adjustnormalsize{\def\normalsize{\mathsurround=0pt \realnormalsize
 \parindent=0pt\abovedisplayskip=0pt\belowdisplayskip=0pt}%
 \def\phantompar{\csname par\endcsname}\normalsize}%
\def\lthtmltypeout#1{{\let\protect\string \immediate\write\lthtmlwrite{#1}}}%
\newcommand\lthtmlhboxmathA{\adjustnormalsize\setbox\sizebox=\hbox\bgroup\kern.05em }%
\newcommand\lthtmlhboxmathB{\adjustnormalsize\setbox\sizebox=\hbox to\hsize\bgroup\hfill }%
\newcommand\lthtmlvboxmathA{\adjustnormalsize\setbox\sizebox=\vbox\bgroup %
 \let\ifinner=\iffalse \let\)\liih@math }%
\newcommand\lthtmlboxmathZ{\@next\next\@currlist{}{\def\next{\voidb@x}}%
 \expandafter\box\next\egroup}%
\newcommand\lthtmlmathtype[1]{\gdef\lthtmlmathenv{#1}}%
\newcommand\lthtmllogmath{\lthtmltypeout{l2hSize %
:\lthtmlmathenv:\the\ht\sizebox::\the\dp\sizebox::\the\wd\sizebox.\preveqno}}%
\newcommand\lthtmlfigureA[1]{\let\@savefreelist\@freelist
       \lthtmlmathtype{#1}\lthtmlvboxmathA}%
\newcommand\lthtmlpictureA{\bgroup\catcode`\_=8 \lthtmlpictureB}%
\newcommand\lthtmlpictureB[1]{\lthtmlmathtype{#1}\egroup
       \let\@savefreelist\@freelist \lthtmlhboxmathB}%
\newcommand\lthtmlpictureZ[1]{\hfill\lthtmlfigureZ}%
\newcommand\lthtmlfigureZ{\lthtmlboxmathZ\lthtmllogmath\copy\sizebox
       \global\let\@freelist\@savefreelist}%
\newcommand\lthtmldisplayA{\bgroup\catcode`\_=8 \lthtmldisplayAi}%
\newcommand\lthtmldisplayAi[1]{\lthtmlmathtype{#1}\egroup\lthtmlvboxmathA}%
\newcommand\lthtmldisplayB[1]{\edef\preveqno{(\theequation)}%
  \lthtmldisplayA{#1}\let\@eqnnum\relax}%
\newcommand\lthtmldisplayZ{\lthtmlboxmathZ\lthtmllogmath\lthtmlsetmath}%
\newcommand\lthtmlinlinemathA{\bgroup\catcode`\_=8 \lthtmlinlinemathB}
\newcommand\lthtmlinlinemathB[1]{\lthtmlmathtype{#1}\egroup\lthtmlhboxmathA
  \vrule height1.5ex width0pt }%
\newcommand\lthtmlinlineA{\bgroup\catcode`\_=8 \lthtmlinlineB}%
\newcommand\lthtmlinlineB[1]{\lthtmlmathtype{#1}\egroup\lthtmlhboxmathA}%
\newcommand\lthtmlinlineZ{\egroup\expandafter\ifdim\dp\sizebox>0pt %
  \expandafter\centerinlinemath\fi\lthtmllogmath\lthtmlsetinline}
\newcommand\lthtmlinlinemathZ{\egroup\expandafter\ifdim\dp\sizebox>0pt %
  \expandafter\centerinlinemath\fi\lthtmllogmath\lthtmlsetmath}
\newcommand\lthtmlindisplaymathZ{\egroup %
  \centerinlinemath\lthtmllogmath\lthtmlsetmath}
\def\lthtmlsetinline{\hbox{\vrule width.1em \vtop{\vbox{%
  \kern.1em\copy\sizebox}\ifdim\dp\sizebox>0pt\kern.1em\else\kern.3pt\fi
  \ifdim\hsize>\wd\sizebox \hrule depth1pt\fi}}}
\def\lthtmlsetmath{\hbox{\vrule width.1em\kern-.05em\vtop{\vbox{%
  \kern.1em\kern0.75 pt\hbox{\hglue.17em\copy\sizebox\hglue0.75 pt}}\kern.3pt%
  \ifdim\dp\sizebox>0pt\kern.1em\fi \kern0.75 pt%
  \ifdim\hsize>\wd\sizebox \hrule depth1pt\fi}}}
\def\centerinlinemath{%
  \dimen1=\ifdim\ht\sizebox<\dp\sizebox \dp\sizebox\else\ht\sizebox\fi
  \advance\dimen1by.5pt \vrule width0pt height\dimen1 depth\dimen1 
 \dp\sizebox=\dimen1\ht\sizebox=\dimen1\relax}

\def\lthtmlcheckvsize{\ifdim\ht\sizebox<\vsize 
  \ifdim\wd\sizebox<\hsize\expandafter\hfill\fi \expandafter\vfill
  \else\expandafter\vss\fi}%
\providecommand{\selectlanguage}[1]{}%
\makeatletter \tracingstats = 1 


\begin{document}
\pagestyle{empty}\thispagestyle{empty}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength hsize=\the\hsize}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength vsize=\the\vsize}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength hoffset=\the\hoffset}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength voffset=\the\voffset}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength topmargin=\the\topmargin}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength topskip=\the\topskip}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength headheight=\the\headheight}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength headsep=\the\headsep}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength parskip=\the\parskip}\lthtmltypeout{}%
\lthtmltypeout{latex2htmlLength oddsidemargin=\the\oddsidemargin}\lthtmltypeout{}%
\makeatletter
\if@twoside\lthtmltypeout{latex2htmlLength evensidemargin=\the\evensidemargin}%
\else\lthtmltypeout{latex2htmlLength evensidemargin=\the\oddsidemargin}\fi%
\lthtmltypeout{}%
\makeatother
\setcounter{page}{1}
\onecolumn

% !!! IMAGES START HERE !!!

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlineA{tex2html_nomath_inline933}%
\fbox{\parbox{0.98\textwidth}{\textbf{Nota importante:} el texto de
    descripción de este problema es \textbf{exactamente} el mismo que
    el dejado anteriormente en fotocopiadora y en WWW, al igual que la
    primera pregunta de este ejercicio.  La segunda pregunta es nueva,
    y debe realizarse durante este examen.}  }%
\lthtmlinlineZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline883}%
$TipoNumPlanta~=~\{1..P\}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap943}%
\includegraphics[width=0.3\textwidth]{im/ascensor}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline885}%
$p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
\stepcounter{paragraph}
{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap1037}%
\includegraphics[width=\textwidth]{im/adis}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting261}%
\begin{lstlisting}{}
TASK BotonCabina;
  VAR p: TipoNumPlanta;
BEGIN
  LOOP
    BOTON.LeerCabina(p);
    GESTOR.PulsadoCabina(p);
  END
END BotonCabina;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting264}%
\begin{lstlisting}{}
TASK BotonPlanta(p: TipoNumPlanta);
BEGIN
  LOOP
    BOTON.LeerPlanta(p);
    GESTOR.PulsadoPlanta(p);
  END
END BotonPlanta;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting267}%
\begin{lstlisting}{}
TASK Temporizador;
  VAR t: CARDINAL;
BEGIN
  LOOP
    GESTOR.IniciarEspera(t);
    TIEMPO.Espera(t - TIEMPO.Ahora);
    GESTOR.TerminarEspera;
  END
END Temporizador;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting274}%
\begin{lstlisting}{}
TASK Ascensor;
  VAR p: TipoNumPlanta;
      movimiento: TipoMovimiento;
      parar: BOOLEAN;
BEGIN
  «inicializar el ascensor parado en alguna 
  planta 'p' y con las puertas abiertas»
  GESTOR.ParadoEnPlanta(p);
  LOOP
    GESTOR.ElegirMovimiento(movimiento);
    PUERTA.Cerrar;
    IF movimiento = SUBIR THEN
      MOTOR.Subir;
    ELSE
      MOTOR.Bajar;
    END;
    REPEAT
      SENSOR.DetectarPaso(p);
      GESTOR.HayPeticion(p, parar);
    UNTIL parar;
    MOTOR.Parar;
    PUERTA.Abrir;
    GESTOR.ParadoEnPlanta(p);
  END
END Ascensor;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline729}%
\ensuremath{\times}%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline737}%
\ensuremath{\mathcal{B}}%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline743}%
\ensuremath{\mathcal{N}}%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline887}%
$|$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline889}%
$\forall t \in\emph{TipoGestor}\ensuremath{\bullet}\textsf{Longitud}(t.peticion) = P$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline891}%
$g^{ent} = g^{sal} / g\ensuremath{^{sal}}.peticion_p \wedgeg\ensuremath{^{sal}}.pulsadaCabina$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline893}%
$g^{ent} = g^{sal} / g\ensuremath{^{sal}}.peticion_p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline895}%
$g^{ent} = g^{sal} \wedge hay^{sal} = peticion_p$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline897}%
$g^{ent} = g^{sal} / \neg g\ensuremath{^{sal}}.peticion_p \wedge                g\ensuremath{^{sal}}.posicion = p \wedge \neg g\ensuremath{^{sal}}.pulsadaCabina \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline899}%
$g\ensuremath{^{sal}}.abierto \wedge g\ensuremath{^{sal}}.tiempoActual = TIEMPO.Ahora \wedge   g\ensuremath{^{sal}}.tiempoLimite = g\ensuremath{^{sal}}.tiempoActual + T$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline787}%
\ensuremath{^{ent}}%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline901}%
$<$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline903}%
$g^{ent} = g^{sal} \wedge t^{sal} =$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline905}%
$g^{ent} = g^{sal} / \emph{g\ensuremath{^{sal}}.tiempoActual} =$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline907}%
$\exists p \in \emph{TipoNumPlanta}\ensuremath{\bullet}p \not=g\ensuremath{^{ent}}.posicion \wedge \emph{g\ensuremath{^{ent}}.peticion}_p \wedge p\not=g\ensuremath{^{ent}}.posicion \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline909}%
$(\emph{g\ensuremath{^{ent}}.pulsadaCabina} \vee \emph{g\ensuremath{^{ent}}.tiempoActual} <\emph{g\ensuremath{^{ent}}.tiempoLimite})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline911}%
$g^{ent} = g^{sal} / \emph{g\ensuremath{^{sal}}.sentido} = g\ensuremath{^{sal}}.mov\wedge \neg g\ensuremath{^{sal}}.abierto \wedge g\ensuremath{^{sal}}.peticion_p \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline913}%
$g\ensuremath{^{sal}}.mov = \left\{    \begin{array}{ll}      \mathrm{SUBIR} & \exists p \in TipoNumPlanta \ensuremath{\bullet}p >      \emph{g\ensuremath{^{ent}}.posicion} \wedge g\ensuremath{^{ent}}.\emph{peticion}_p \wedge \\& (\emph{sentido} = SUBIR \vee \neg\exists k \in                     TipoNumPlanta \ensuremath{\bullet}k <                     \emph{posicion} \wedge \emph{peticion}_k) \\\mathrm{BAJAR} &   e.o.c.    \end{array}\right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting421}%
\begin{lstlisting}{}
TASK BotonCabina(a: TipoNumAscensor);
  VAR p: TipoNumPlanta;
BEGIN
  LOOP
    BOTON.LeerCabina(a, p);
    GESTOR.PulsadoCabina(a, p);
  END
END BotonCabina;
\par TASK BotonPlanta;
BEGIN
  LOOP
    BOTON.LeerPlanta(p);
    GESTOR.PulsadoPlanta(p);
  END
END BotonPlanta;
\par TASK Temporizador;
  VAR t: CARDINAL;
BEGIN
  LOOP
    GESTOR.IniciarEspera(t);
    TIEMPO.Espera(t - TIEMPO.Ahora);
    GESTOR.TerminarEspera;
  END
END Temporizador;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting427}%
\begin{lstlisting}{}
TASK Ascensor(a: TipoNumAscensor);
  VAR p: TipoNumPlanta;
      movimiento: TipoMovimiento;
      parar: BOOLEAN;
BEGIN
  «inicializar el ascensor parado en alguna
   planta 'p' y con las puertas abiertas»
  GESTOR.ParadoEnPlanta(a, p);
  LOOP
    GESTOR.ElegirMovimiento(a, movimiento);
    PUERTA.Cerrar;
    IF movimiento = SUBIR THEN
      MOTOR.Subir(a);
    ELSE
      MOTOR.Bajar(a);
    END;
    REPEAT
      SENSOR.DetectarPaso(a, p);
      GESTOR.HayPeticion(a, p, parar);
    UNTIL parar;
    MOTOR.Parar(a);
    PUERTA.Abrir(a);
    GESTOR.ParadoEnPlanta(a, p);
  END
END Ascensor;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlpictureA{tex2html_wrap1093}%
\includegraphics[width=\textwidth]{im/adis-2}%
\lthtmlpictureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline917}%
$\forall g \inTipoGestor\ensuremath{\bullet}\textsf{Longitud}(p.petPlanta) = P  \wedge \textsf{Longitud}(g.sentido) = NumAscensores \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline919}%
$\textsf{Longitud}(g.asignada) = NumAscensores \wedge \textsf{Longitud}(g.posicion) = NumAscensores \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline921}%
$\textsf{Longitud}(g.pulsadaCabina) = NumAscensores \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline923}%
$\textsf{Longitud}(g.tiempoActual) = NumAscensores \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline925}%
$\textsf{Longitud}(g.tiempoLimite) = NumAscensores \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline927}%
$\forall i\in\{1..NumAscensores\}\ensuremath{\bullet}\mathsf{Longitud}(g.peticion_i) = P$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline929}%
$\exists a \in \emph{TipoNumAscensor}\ensuremath{\bullet}\emph{g.tiempoActual} < \emph{g.tiempoLimite}_a$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2398}%
$\forall a \in\emph{TipoAlm}\ensuremath{\bullet}(\mathsf{Longitud}(a) = \emph{NumSalas})$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2400}%
$\forall i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{sal}}_i.nvacas = 0)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2402}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas = 0\vee (alm\ensuremath{^{ent}}_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}_i.tipo = loca))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2404}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas = 0\vee (alm\ensuremath{^{ent}}_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}_i.tipo = loca) \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2406}%
$ sala\ensuremath{^{sal}}= i \wedge alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslashalm\ensuremath{^{sal}}_i.nvacas= alm\ensuremath{^{ent}}_i.nvacas + 1 \wedge alm\ensuremath{^{sal}}_i.tipo = loca)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2408}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas > 0 \wedgealm_i.tipo = loca)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2410}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas > 0 \wedgealm\ensuremath{^{ent}}_i.tipo = loca \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2412}%
$sala\ensuremath{^{sal}}= i \wedge alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslashalm\ensuremath{^{sal}}_i.nvacas = alm\ensuremath{^{ent}}_i.nvacas - 1) $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2414}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas = 0\vee (alm\ensuremath{^{ent}}_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}_i.tipo = normal))$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2416}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas = 0\vee (alm\ensuremath{^{ent}}_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}_i.tipo = normal) \wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2418}%
$ sala\ensuremath{^{sal}}= i \wedge alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslashalm\ensuremath{^{sal}}_i.nvacas= alm\ensuremath{^{ent}}_i.nvacas + 1 \wedge alm\ensuremath{^{sal}}_i.tipo = normal)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2420}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas > 0 \wedgealm\ensuremath{^{ent}}_i.tipo = normal)$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2422}%
$\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas > 0 \wedgealm\ensuremath{^{ent}}_i.tipo = normal \wedge $%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}


%
\providecommand{\mpat}[1]{
  \begin{minipage}[t]{0.2\textwidth}
    #1
  \end{minipage}
}%


%
\providecommand{\mpae}[1]{
  \begin{minipage}[t]{0.2\textwidth}
    #1
  \end{minipage}
}%

\stepcounter{paragraph}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2108}%
\(\exists i \in TipoNumSala\ensuremath{\bullet}(alm\ensuremath{^{ent}}_i.nvacas > 0 \wedge
alm\ensuremath{^{ent}}_i.tipo = normal)\)%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}


%
\providecommand{\mpbl}[1]{
  \begin{minipage}[t]{0.18\textheight}
    #1
  \end{minipage}
}%


%
\providecommand{\rotlatex}[1]{
\par
#1
\par
}%

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2432}%
$alm\ensuremath{^{sal}}_{sala\ensuremath{^{sal}}} < TamSala$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2436}%
$alm\ensuremath{^{sal}}_{sala\ensuremath{^{sal}}} = 0$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1332}%
\begin{displaymath}
  TipoAlm = (salas: Secuencia(TipoSala) \ensuremath{\times}nosalaslocas: \ensuremath{\mathcal{N}}\ensuremath{\times}nosalasnormales: \ensuremath{\mathcal{N}})
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1338}%
\begin{displaymath}
  \begin{array}{ll}
\exists i \in TipoNumSala \ensuremath{\bullet}& ((alm\ensuremath{^{ent}}.salas_i.nvacas = 0 
\mathbf{\wedge alm\ensuremath{^{ent}}.nosalaslocas \leq NumSalas - 2)}
\vee 
\\& (alm\ensuremath{^{ent}}.salas_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}.salas_i.tipo =
loca)) 
  \end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1345}%
\begin{displaymath}
  \begin{array}{ll}
    \exists i \in  TipoNumSala \ensuremath{\bullet}& ((alm\ensuremath{^{ent}}.salas_i.nvacas = 0 
    \mathbf{\wedge alm\ensuremath{^{ent}}.nosalasnormales \leq NumSalas - 2}) \vee \\
    & (alm\ensuremath{^{ent}}.salas_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}.salas_i.tipo =
    normal)) 
  \end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1354}%
\begin{displaymath}
  \begin{array}{ll}
\exists i \in  TipoNumSala \ensuremath{\bullet}& ((alm\ensuremath{^{ent}}.salas_i.nvacas = 0 \wedge
alm\ensuremath{^{ent}}.nosalaslocas \leq NumSalas - 2) \vee \\
& (alm\ensuremath{^{ent}}.salas_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}.salas_i.tipo = loca))
\wedge sala\ensuremath{^{sal}}= i \wedge \\
& alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslash alm\ensuremath{^{sal}}.salas_i.nvacas = alm\ensuremath{^{ent}}.salas_i.nvacas
+ 1 \\
& \wedge alm\ensuremath{^{sal}}.salas_i.tipo = loca   \wedge (
\mathbf{alm\ensuremath{^{ent}}.salas_i.nvacas = 0 
\rightarrow} \\
&  \mathbf{alm\ensuremath{^{sal}}.nosalaslocas = alm\ensuremath{^{ent}}.nosalaslocas + 1) }
  \end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1362}%
\begin{displaymath}
  \begin{array}{ll}
    \exists i \in TipoNumSala \ensuremath{\bullet}& 
    ((alm\ensuremath{^{ent}}.salas_i.nvacas = 0 \wedge alm\ensuremath{^{ent}}.nosalasnormales \leq
    NumSalas - 2) \vee \\
    & (alm\ensuremath{^{ent}}.salas_i.nvacas < TamSala \wedge alm\ensuremath{^{ent}}.salas_i.tipo =
    normal) \wedge sala\ensuremath{^{sal}}= i \wedge \\
    & alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslash alm\ensuremath{^{sal}}.salas_i.nvacas =
    alm\ensuremath{^{ent}}.salas_i.nvacas + 1 \wedge \\
    &  alm\ensuremath{^{sal}}.salas_i.tipo = normal \mathbf{ \wedge (alm\ensuremath{^{ent}}.salas_i.nvacas =
    0 \rightarrow} \\
    &  \mathbf{alm\ensuremath{^{sal}}.nosalasnormales =
      alm\ensuremath{^{ent}}.nosalasnormales  + 1))}
  \end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1372}%
\begin{displaymath}
  \begin{array}{ll}
  \exists \in TipoNumSala \ensuremath{\bullet}& (alm\ensuremath{^{ent}}.salas_i.nvacas > 0 \wedge
  alm\ensuremath{^{ent}}.salas_i.tipo = loca \wedge \\
  & sala\ensuremath{^{sal}}= i \wedge alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslash
  alm\ensuremath{^{sal}}.salas_i.nvacas = alm\ensuremath{^{ent}}.salas_i.nvacas - 1 \mathbf{\wedge}\\
  & \mathbf{(alm\ensuremath{^{sal}}.salas_i.nvacas = 0 \rightarrow}  \mathbf{alm\ensuremath{^{sal}}.nosalaslocas =
  alm\ensuremath{^{ent}}.nosalaslocas - 1))}
  \end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmldisplayA{displaymath1381}%
\begin{displaymath}
  \begin{array}{ll}
  \exists \in TipoNumSala \ensuremath{\bullet}& (alm\ensuremath{^{ent}}.salas_i.nvacas > 0 \wedge
  alm\ensuremath{^{ent}}.salas_i.tipo = normal \wedge sala\ensuremath{^{sal}}= i \wedge \\
  & alm\ensuremath{^{sal}}= alm\ensuremath{^{ent}}\backslash alm\ensuremath{^{sal}}.salas_i.nvacas =
  alm\ensuremath{^{ent}}.salas_i.nvacas - 1 \mathbf{\wedge} \\
  & \mathbf{(alm\ensuremath{^{sal}}.salas_i.nvacas = 0 \rightarrow}\mathbf{ alm\ensuremath{^{sal}}.nosalasnormales =
    alm\ensuremath{^{ent}}.nosalasnormales - 1))}
  \end{array}
\end{displaymath}%
\lthtmldisplayZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2440}%
$\mathbf{alm\ensuremath{^{ent}}.nosalastipo \leq
  NumSalas - 2}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{paragraph}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2442}%
$\leq$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2468}%
$\left\{\begin{array}{ll}0     & (\forall i \in \mbox{TipoNumSala}\cdot \\[-0.4ex]     & \mbox{\hspace{2em}             almacen(i).tipo = tipo $\rightarrow$\  almacen(i).npiezas             $\not=$\  TAMSALA) $\wedge$} \\[0.4ex]    & (\exists i \in \mbox{TipoNumSala}\cdot\\[-0.4ex]    &  \mbox{\hspace{2em} almacen(i).tipo = tipo $\rightarrow$nosalas(tipo) = NUMSALAS -1)}\\i & \exists i \in \mbox{TipoNumSala} \cdot\\[-0.4ex]            & \mbox{\hspace{3em} almacen(i).npiezas = 0 $\wedge$} \\[-0.4ex]            & \mbox{\hspace{3em} $\forall j \in$\  TipoNumSala}\cdot \\[-0.4ex]            & \mbox{\hspace{6em} almacen(j).tipo = tipo                             $\rightarrow$\  almacen(j).npiezas = TAMSALA} \\\multicolumn{2}{l}{\mbox{{\it maxim} $i \in$\  TipoNumSala$|$}}\\[-0.4ex]          \multicolumn{2}{l}{\mbox{\hspace{3em}almacen(i).tipo = tipo $\wedge$almacen(i).npiezas $<$\  TAMSALA $\cdot$\  }}\\[-0.4ex]          \multicolumn{2}{r}{\mbox{ almacen(i).npiezas}} \\[-0.4ex]          & \mbox{e.o.c.}         \end{array}\right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2484}%
$\left\{\begin{array}{ll}          0  & \forall i \in \mbox{TipoNumSala$\cdot$almacen(i).npiezas $\neq$\  0 $\rightarrow$almacen(i).tipo $\neq$\  tipo} \\[-0.4ex]          \multicolumn{2}{l}{\mbox{{\it minim} $i \in$\  TipoNumSala$|$almacen(i).tipo = tipo                                                                  $\cdot$\  almacen(i).npiezas}} \\[-0.4ex]          & \mbox{e.o.c.}         \end{array}\right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2486}%
$\left\{\begin{array}{ll}          \mbox{normal}  & \mbox{tipo = loca} \\[-0.4ex]          \mbox{loca}    & \mbox{tipo = normal}          \end{array}\right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2490}%
$\forall i \in \mbox{TipoNumSala} \cdot$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2492}%
$^{sal}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2498}%
$\left\{\begin{array}{ll}  \mbox{almacen$^{ent}$(sala) + 1} & \mbox{i = sala} \\[-0.4ex]  \mbox{almacen$^{ent}$(i)} & \mbox{e.o.c.} \end{array}\right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2500}%
$\wedge$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2502}%
$^{ent}$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2504}%
$\rightarrow$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2514}%
$>$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2522}%
$\forall i \in TipoNumSala.\mbox{              almacen$^{sal}$(i) =}\left\{\begin{array}{ll}  \mbox{almacen$^{ent}$(sala) - 1} & \mbox{i = sala} \\[-0.4ex]  \mbox{almacen$^{ent}$(i)} & \mbox{e.o.c.} \end{array}\right.$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

\stepcounter{section}
{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2876}%
$A$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2878}%
$B$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2880}%
$C$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2884}%
$\Box$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2898}%
$\surd$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}


%
\providecommand{\pregresp}[1]{
  \begin{minipage}[t]{0.45\textwidth}
    #1
  \end{minipage}
}%

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2904}%
$<<$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2906}%
$>>$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlinemathA{tex2html_wrap_inline2908}%
$v1, v2, v3, v4$%
\lthtmlinlinemathZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting2740}%
\begin{lstlisting}{}
MODULE Programa; 
TYPE T = [1..3]; 
VAR c1, c2 : CHANNEL (* OF T *);
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting2751}%
\begin{lstlisting}{}
TASK P1; 
VAR a : T; 
BEGIN 
    a := $v1$; 
    IF NOT ODD (a) THEN DEC (a) END; 
    IF a > 2 THEN 
        Send (c1, a) 
    END; 
END P1; 
  \end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting2757}%
\begin{lstlisting}{}
TASK P2; 
VAR a : T; 
BEGIN 
    a:= $v2$; 
    Send (c2, a); 
END P2; 
  \end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting2769}%
\begin{lstlisting}{}
TASK G_R; 
VAR a, b : T;  
VAR i, c : INTEGER; 
BEGIN 
    GetChannel(c1);
    GetChannel(c2);
    a := $v3$; 
    c := 0; 
    FOR i := 1 TO 2 DO 
        SELECT 
            WHEN a < 2, Receive (c1, b) DO
                c := c + b;
            WHEN a > 2, Receive (c2, b) DO
                c := c + b;
            ELSE
                c := b;
        END;
        a := $v4$;
    END 
END G_R; 
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlfigureA{lstlisting2779}%
\begin{lstlisting}{}
BEGIN 
    COBEGIN
        P1; P2; G_R
    COEND;
END Programa;
\end{lstlisting}%
\lthtmlfigureZ
\lthtmlcheckvsize\clearpage}

{\newpage\clearpage
\lthtmlinlineA{tex2html_nomath_inline2992}%
\fbox{
  \begin{minipage}[t]{0.98\textwidth}
    \textbf{Valores admisibles:} \hfill \\
\par
\begin{tabular}{p{20em}l}
      $v_i \in \{1..3\} \wedge$\  & 
         \emph{por declaración de tipos} \\
      $((v_1 = 3 \wedge (v_3,v_4) \in \{(1,3), (3,1)\}) \vee$\  & 
         \emph{cuando \textsf{P1} envía dato}\\
      $(v_1 \not= 3 \wedge (v_3,v_4) \in \{(2,3), (3,2)\}))$\  & 
         \emph{cuando \textsf{P1} no envía ningún dato}\\
    \end{tabular} \\
\par
Si se considera que puede haber un error de ejecución en el caso
    de que se realice la asignación \texttt{c := b} en el proceso
    gestor antes de la inicialización de \texttt{b}, la última línea
    debe ser \\
\par
\begin{tabular}{l}
      $v_1 \not= 3 \wedge v_3 = 3 \wedge v_4 = 2$    \end{tabular} \\
\par
que fuerza a que se ejecute la recepción por el canal \textsf{c2}
    antes que la rama \textbf{ELSE} de la \textbf{SELECT}.
\par
\end{minipage}
}%
\lthtmlinlineZ
\lthtmlcheckvsize\clearpage}


\end{document}
