You will write your algorithms in
ascii
text, but people unfamiliar
with PlusCal or TLA+ will find them easier to read if you pretty-print
them. There is a pretty-printer that replaces TLA+
ascii
symbols by their mathematical equivalents — for example, printing
\in as ∈. It also does a pretty good job of
formatting the algorithm and the rest of the specification that
contains the algorithm. You can also use the pretty-printer to
format an algorithm or parts of an algorithm in a LaTeX document.