\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}
EXTENDS Integers, Sequences

Put(s) == Append(s, "widget")
Get(s) == Tail(s)

a (+) b == (a + b) % 2

(***************************************************************************
--algorithm Handshake {

    variable p = 0,  c = 0,  box = << >> ;

    process (Producer = 0) 
      { p1: while (TRUE)
              { await p = c ;
                box := Put(box) ;
                p := p (+) 1
              }
      }
      
    process (Consumer = 1)
      { c1: while (TRUE)
              { await p # c ;
                box := Get(box) ;
                c := c (+) 1
              }
      }
}
 ***************************************************************************)
\end{verbatim*}
\end{popup}
\makeasciipopup