Hi,

I hacked a quick-and-dirty LaTeX style file enabling me to pretty-print Alloy 4 code. As it may be useful to many users, I am releasing it hereby under public domain ;-)  

First issue these commands in the preamble of your document:

\usepackage{listings}

\lstdefinelanguage{Alloy}
{morekeywords={abstract, all, and, as, assert, but, check, disj, else,
  exactly, extends, fact, for, fun, iden, if, iff, implies, in, Int,
  int, let, lone, module, no, none, not, one, open, or, part, pred,
  run, seq, set, sig, some, sum, then, univ},
sensitive=true,
morecomment=[l][\small\itshape]{--},
morecomment=[l][\small\itshape]{//},
morecomment=[s][\small\itshape]{/*}{*/},
%basicstyle=\sffamily,
tabsize=2,
columns=fullflexible,
literate={->}{{$\to$}}1 {^}{{$\mspace{-3mu}\widehat{\quad}\mspace{-3mu}$}}1
 {<}{$<$ }2 {>}{$>$ }2 {>=}{$\geq$ }2 {=<}{$\leq$ }2
 {<:}{{$<\mspace{-3mu}:$}}2 {:>}{{$:\mspace{-3mu}>$}}2
 {=>}{{$\Rightarrow$ }}2 {+}{$+$ }2 {++}{{$+\mspace{-8mu}+$ }}2
 {\~}{{$\mspace{-3mu}\widetilde{\quad}\mspace{-3mu}$}}1
 {!=}{$\neq$ }2 {*}{${}^{\ast}$}1 {.}{$\cdot$}1
 {\#}{$\#$}1
}


Then don't forget to issue the following command after the \begin{document}:

\lstset{language=Alloy}

(the listings package can handle many languages, so every \lsset command is here to switch to a new pretty-printing style).

Now, every time you wish to show some Alloy code, just write:

\begin{lstlisting}[numbers=left, numberstyle={\tiny\oldstylenums}, name=aName]
sig A { x : some B }

sig B {}

sig C {
   y : one A,
   z : one B
}
\end{lstlisting}


The options numbers=left and numberstyle={\tiny\oldstylenums} command LaTeX to number lines with small old style numbers.

The name=aName gives the name aName to this enviromnent. Every other environemnt with the same name, appearing later in the LaTeX file, will continue the numbering instead of counting from 1. If you don't want this behaviour, just remove this option. If you want this option but don't want to continue a previous numbering, just use a new name.

Cheers

dc