
\documentclass[a4paper]{article}

\setlength\textwidth{6.5in}
\setlength\oddsidemargin{0in}
\setlength\evensidemargin{0in}

%\setlength\headheight{0in}
%\setlength\headsep{0in}

%\setlength\topmargin{-0.5in}
%\addtolength{\textheight}{0.5in}


\newcommand{\SIG}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\Idiom}[1]{\textsl{#1}}
\newcommand{\IF}[0]{\textbf{if}}
\newcommand{\FI}[0]{\textbf{fi}}
\newcommand{\SKIP}[0]{\textbf{skip}}
\newcommand{\DO}[0]{\textbf{do}}
\newcommand{\OD}[0]{\textbf{od}}

\usepackage{latexsym}
\usepackage[spanish]{babel}

\title{Programaci\'on Concurrente \\ Parcial 1}
\author{J. Blanco, N. Wolovick}


\begin{document}
\maketitle

\begin{enumerate}

	
	%WF99-6	
	\item{Dado el siguiente multiprograma muestre:
		\newline
		\begin{center}
		\begin{tabular}{|l|l|}
			\hline
			\multicolumn{2}{|l|}{Pre: $x=0 \wedge y=0 \wedge \neg p \wedge \neg q$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				A:\ \=$p:=true;$ \\
				   \>$x:=x+1;$ \\
				   \>$\IF\ 1\leq y \rightarrow y:=y-1\ \FI$ \\
				   \>$\{q\}$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				B:\ \=$q:=true;$ \\
				   \>$y:=y+1;$ \\
				   \>$\IF\ 1\leq x \rightarrow x:=x-1\ \FI$ \\
				   \>$\{p\}$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}
		\begin{enumerate}
			 \item{Correcci\'on de la anotaci\'on.}
			 \item{Progreso.}
			 \item{Invariancia de $0\leq x\leq 1 \wedge 0\leq y\leq 1$.}
			 \item{La precondici\'on $x=0 \wedge y=0$, tambi\'en vale como postcondici\'on.}
			 \item{Si reemplazamos la sentecia guardada de la componente $A$ por
			 	la de menor grado de atomicidad
			 	$\IF\ 1\leq y \rightarrow \SKIP\ \FI; y:=y-1$, la correcci\'on se
			 	mantiene.
			 }
		\end{enumerate}
	}

	
	%rh 920312-0
	\item{ Se tiene un programa paralelo compuesto por 3 componentes
		\newline
		\begin{center}
		\begin{tabular}{|l|l|l|}
			\hline
			\multicolumn{3}{|l|}{Pre: $x=0 \wedge y=0 \wedge z=0$} \\
			\hline
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$ *[ x:=x+1 ]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$ *[ y:=x ]$
			\end{tabbing}
			\end{minipage}
			&
			\begin{minipage}[t]{1in}
			\begin{tabbing}
				$ *[ z:=z+1 ]$
			\end{tabbing}
			\end{minipage}
			\\
			\hline
		\end{tabular}
		\end{center}

		Agregar c\'odigo de sincronizaci\'on de manera de asegurar el siguiente invariante.
		\[ y\leq x \wedge x\leq z \wedge z\leq y+1 \]

		Sincronizar utilizando solamente skip guardados.

		Demostrar la correcci\'on parcial de la soluci\'on y dar un argumento informal pero claro del progreso de la soluci\'on. 
	}

\end{enumerate}

\end{document}
