\documentclass[12pt]{article}

\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}
\usepackage{stmaryrd}
\usepackage[usenames,dvipsnames]{color}

\usepackage{amssymb}
\usepackage{amsxtra}
\usepackage{amsmath}
\usepackage{amstext}
\usepackage{amsthm}
\usepackage{amsbsy}
\usepackage{latexsym}
\usepackage{mathrsfs}
\usepackage{eucal}
\usepackage{alltt}
\usepackage{listings}



\theoremstyle{definition}
\newtheorem{definition}{Definici\'on}[section]
\newtheorem{proposition}{Proposici\'on}[section]
\newtheorem{lemma}{Lema}[section]
\newtheorem{theorem}{Teorema}[section]
\newtheorem{corollary}{Corolario}[section]
\newtheorem{example}{Ejemplo}[section]
\newtheorem{observation}{Observaci\'on}[section]
\newtheorem{problem}{Problema}[section]
\newtheorem{question}{Pregunta}[section]
\newtheorem{pml}{Código Promela}[section]

\def\proof{\noindent{\textbf{Demostraci\'on}}\\}
\def\endproof{\hfill{\ensuremath\square}}
\def\refname{Referencias}
\def\abstractname{Resumen}


\title{Código Promela \\
en \LaTeX \\
Métodos Formales \\
Otoño 2012 \\
Sección 101}
\author{José de Jesús Lavalle Martínez}

\begin{document}
\maketitle

\begin{abstract}
Este documento sirve para aprender a escribir código Promela en \LaTeX.
\end{abstract}

En general siempre hay al menos tres maneras de presentar en \LaTeX\, código de lenguajes de programación, la primera es usar el ambiente \verb+verbatim+, la segunda usando el ambiente \verb+alltt+, para la tercera se debe usar el ambiente \verb+lstlisting+.

\section{verbatim}
En la primera manera se escribe el código entre \verb+\begin{verbatim}+ y \verb+\end{verbatim}+, note que en este ambiente \LaTeX\ no interpreta los comandos, no se necesita incluir algún paquete, así obtendrá:

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+verbatim+.
\begin{verbatim}
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("%d divided by %d = %d, remainder = %d\n", 
             dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{verbatim}
\end{pml}

\section{alltt}
En la segunda manera se escribe el código entre \verb+\begin{alltt}+ y \verb+\end{alltt}+, note que en este ambiente \LaTeX\ sí interpreta los comandos, necesita poner en el preámbulo \verb+\usepackage{alltt}+, para obtener:

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \texttt{alltt}.
\begin{alltt}
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n ", 
             dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{alltt}
\end{pml}

\section{lstlisting}
La tercera forma es escribiendo el código entre \verb+\begin{lstlisting}+ y \verb+\end{lstlisting}+ con opción \verb+[language=Promela]+, en este ambiente tampoco se interpretan los comandos, lo único que hace el paquete es formatear el código de acuerdo al lenguaje seleccionado y poner en negras las palabras reservadas del lenguaje, ponga en el preámbulo \verb+\usepackage{listings}+. 

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+.
\begin{lstlisting}[language=Promela]
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("\% d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{lstlisting}
\end{pml}

Observe que las líneas largas se salen del margen derecho de la hoja. Ponga el código entre \verb+\begin{lstlisting}+ y \verb+\end{lstlisting}+ con opción \verb+[language=Promela,numbers=left,breaklines=true]+ si quiere que el paquete \verb+listings+ numere las líneas de código y parta automáticamente las líneas muy grandes, obtendrá:

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas y ruptura automática de líneas largas.
\begin{lstlisting}[language=Promela, numbers=left, breaklines=true]
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("% d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{lstlisting}
\end{pml}

Si además quiere encerrar el código en una caja sombreada agregue la opción \verb+frame=shadowbox+.

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura automática de líneas largas y caja sombreada.
\begin{lstlisting}[language=Promela, numbers=left, breaklines=true,frame=shadowbox]
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("% d divided by %d = %d, remainder = %d\n", dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{lstlisting}
\end{pml}

Como puede observar en la línea 27 se imprimen mal los carácteres de formato, para solucionarlo utilizamos la opción \verb+escapeinside=`'+ para que lo que encerremos entre estos dos carácteres sea interpretado por \LaTeX, es decir \verb+"`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'"+.

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura automática de líneas largas y carácteres interpretados por \LaTeX.
\begin{lstlisting}[language=Promela, numbers=left, breaklines=true,escapeinside=`']
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'", dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{lstlisting}
\end{pml}

Lo malo es que al habilitar a \LaTeX\, para que interprete el código, el paquete \verb+listings+ pierde el control, si ahora ponemos el código  en una caja el paquete se equivoca al pintarla, obtenemos:

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura automática de líneas largas, carácteres especiales interpretados por \LaTeX\, y caja sombreada.
\begin{lstlisting}[language=Promela, numbers=left, breaklines=true,escapeinside=`',frame=shadowbox]
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'", dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{lstlisting}
\end{pml}

Como no se puede tener todo, debemos tomar una decisión, es decir, si queremos la caja deshabilitamos la ruputura automática de líneas, nosotros partimos las líneas, para obtener:

\begin{pml} Programa para hallar el cociente y el residuo de dos números naturales, presentado usando el ambiente \verb+lstlisting+ con las líneas numeradas, ruptura manual de líneas largas, carácteres especiales interpretados por \LaTeX\, y caja sombreada.
\begin{lstlisting}[language=Promela, numbers=left, breaklines=false,escapeinside=`',frame=shadowbox]
/* Copyright 2007 by Moti Ben-Ari 
under the GNU GPL; see readme.txt */

active proctype P() {
   int dividend = 15, divisor  = 4;
   int quotient = 0, remainder = 0;
   int n = dividend;

   assert (dividend >= 0 && divisor > 0);

   do
      :: n != 0 ->
         assert(dividend == quotient * divisor + 
                remainder + n);
         assert(0 <= remainder && remainder < divisor);
      
         if
            :: remainder + 1 == divisor -> 
               quotient++; 
               remainder = 0
            :: else ->
               remainder++
         fi;
         n--
      :: else ->
         break
   od;
   printf("`\%d divided by \%d = \%d, remainder = \%d \textbackslash\!n'", 
          dividend, divisor, quotient, remainder);
   assert (dividend == quotient * divisor + remainder);
   assert (0 <= remainder && remainder < divisor);
}
\end{lstlisting}
\end{pml}

\end{document}