\def\|#1|{{\bf #1}}
\newcommand{\Case}[2]{\>\> $\phi$ is $#1$ : \|return| $#2$\\}
\begin{tabbing}
XX\=XX\=XX\=XX\=\kill
\|function| {\tt SAT}\,($\phi$)\\
/*  determines the set of states satisfying $\phi$ */ \\
\|begin|\\
\>\|case|\\
\Case{\top}{S}
\Case{\bot}{\emptyset}
\>\> $\phi$ is atomic: \|return| $\{s\in S\mid \phi\in L(s)\}$\\
\Case{\neg\phi_1}{S - {\tt SAT}\,(\phi_1)}
\Case{\phi _1\land \phi _2}{{\tt SAT}\,(\phi _1)\cap {\tt SAT}\,(\phi _2)}
\Case{\phi _1\lor \phi _2}{{\tt SAT}\,(\phi _1)\cup {\tt SAT}\,(\phi _2)}
\Case{\phi _1\to\phi _2}{{\tt SAT}\,(\neg\phi \vee\phi _2)}
\Case{\AX\phi_1}{{\tt SAT}\,(\neg\EX\neg\phi_1)}
\Case{\EX\phi_1}{{\tt SAT_{EX}}(\phi_1)}
\Case{\A[\phi _1\U\, \phi _2]}{{\tt SAT}(\neg(\E [\neg \phi _2\U (\neg \phi
_1\wedge \neg\phi _2)]\vee \EG\neg\phi _2))}
\Case{\E[\phi _1\U \phi _2]}{{\tt SAT_{EU}}(\phi _1, \phi _2)}
\Case{\EF\phi_1}{{\tt SAT}\,(\E (\top \U \phi_1))}
\Case{\EG\phi_1}{{\tt SAT}(\neg\AF\neg\phi_1)}
\Case{\AF\phi_1}{{\tt SAT_{AF}}\,(\phi_1)}
\Case{\AG\phi_1}{{\tt SAT}\,(\neg \EF \neg \phi_1)}
\>\|end case|\\
\|end function|
\end{tabbing}