%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Model: Computations}}
\vspace{0.6in}
\begin{center}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig1-computations.eps}}
	\end{figure*}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>\Red{event}\\
\>\Red{computation} $\langle E, \ra \rangle$\\
\>\Red{cut}\\
\>$G$ and $K$ are \Red{consistent} cuts\\
\>$H$ is an \Red{inconsistent} cut\\ 
\>\Red{predicate} \ \ example: mutual exclusion\\ \ \\
\>Assumptions: asynchronous, reliable message-passing
\end{tabbing}
\end{center}

%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{\Brown{Model: Controlling Computations}}

\vspace{0.6in}
\begin{center}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig3-contr-computations.eps}}
	\end{figure*}
\vspace{0.6in}
\begin{tabbing}
xxxxxx\= xxxxx\= xxxxxxxxxxxxxxxxxxxxxxxxxx\= \kill
\>$\langle E, \cra \rangle$ is a \Red{controlling computation} of B in 
$\langle E, \ra \rangle$, if:\\ \ \\
\>	\>(1) $\cra$ is stricter than $\ra$, and\\
\>\>(2) all consistent cuts in $\langle E, \cra \rangle$ satisfy $B$
\end{tabbing}
\end{center}
%-------------------------------------------------------------------------------
