%% BAD ASCII
\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}
TypeOK == /\ pc \in [{0,1} -> {"r", "e1", "e2", "cs"}]
          /\ x \in [{0,1} -> BOOLEAN]
          
InCS(i) == pc[i] = "cs"

MutualExclusion == ~(InCS(0) /\ InCS(1))

Inv == /\ TypeOK
       /\ MutualExclusion
       /\ \A i \in {0,1} : InCS(i) \/ (pc[i] = "e2") => x[i]
\end{verbatim*}
\end{popup}
\makeasciipopup