\def\|#1|{{\bf #1}}
\begin{tabbing}
XX\=XX\=XX\=XX\=\kill
\|function| {\tt SAT _{EU}}\,($\phi,\psi$)\\
/*  determines the set of states satisfying ${\rm E}[\phi{\rm U}\, \psi]$ */ \\
\|local var| $W,X,Y$\\
\|begin|\\
\> $W := {\tt SAT}\, (\phi);$\\
\> $X := S;$\\
\> $Y := {\tt SAT}\, (\psi);$\\
\> \|repeat until| $X=Y$\\
\> \|begin|\\
\> \> $X := Y$;\\
\> \> $Y := Y \cup (W \cap {\tt pre}_\exists (Y))$\\
\> \|end|\\
\> \|return| $Y$\\
\|end|\\
\end{tabbing}